重写规则解决数独谜题的理论计算机科学电子笔记

理论计算机科学电子笔记176（2007）79-93www.elsevier.com/locate/entcs用重写规则解决数独谜题*GustavoSantoos-Garc′sala1萨拉曼卡大学米格尔·帕洛米诺2D pto o。deSist emanforicosyProgram acionn，Uiv ersidadCom plutense摘要数独游戏（英语：Sudoku Puzzle）的目的是在一个网格的每个单元格中输入一个从1到9的数字，最常见的是由3× 3子网格组成的9×每一行、每一列和每一区域只能包含每个数字的一个实例。 在本文中，我们展示了如何数独难题可以解决重写使用Maude的规则。三个过程（扫描，标记和分析）是解决数独的经典技术。淘汰是我们采取的主要策略。该战略的假设和几个应急措施也得到了实施。保留字：重写逻辑，莫德，数独，拼图。1引言重写逻辑[13]是一种并发更改逻辑，可以自然地处理状态和高度不确定的并发计算。它具有良好的属性，作为一个灵活和通用的语义框架，为各种语言和并发模型提供语义此外，它允许用户定义语法，完全自由地选择适合每个问题的运算符和结构属性。重写逻辑及其实现的自然性，Maude [9]，用于建模和实验数学问题，已经在许多作品中得到了说明。我们在这篇论文中的目标是进一步促进这一池，但在一个更休闲的背景下，沿着[14]的路线由Mi n提供的软件包包含Ci enciayTe cnolog’aI+D+iProjectsBFF 2003-08998-C 03-01和TIC-2003-01000。1电子邮件：santos@usal.es2电子邮件：miguelpt@sip.ucm.es1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.00980G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）793 7 216 95 84 915 256 184297 642 351 71 23 958 6 45 8 3 7 2 4 1 9 61 2 6 9 3 5 8 7 44 9 7 6 1 8 3 5 23 5 9 8 4 2 7 6 18 1 4 5 6 7 2 3 97 6 2 3 9 1 5 4 82 3 8 4 5 9 6 1 76 4 1 2 7 3 9 8 59 7 5 1 8 6 4 2 3为此，我们提出了一个案例研究如何使用Maude执行和解决一种流行的难题，即数独。在Maude中，通过重写规则以完全声明的方式支持对象和分布式对象交互非常容易我们描述了如何数独可以表示在一个面向对象的方式，并给出正式的规则，转换成一个解决形式的初始数独，以及如何这种表示可以直接映射到莫德。这些规则的应用，虽然总是导致一个解决方案，可以这样做在许多不同的方式;一些引起组合爆炸，因此应该避免。为了处理这个问题，我们采用了策略来指导Maude2数独一个（标准）数独是一个9× 9的网格，由3× 3的子网格组成，也称为“区域”。最初，一些单元格包含最初叫做数字之地，FIG。1.一、 As udokupuzzl e（《你的时间》，2005年，现在。 295）andditss olution.第一个这样的谜题是由Howard Garnes在1979年创造的，他是一个自由解谜师[1]。该谜题由专业谜题出版商Dell Magazines在其杂志Math Puzzles and LogicProblems中首次在纽约出版。1984年4月，日本出版公司Nikoli在《MonthlyNikolist》上后来，这个名字被缩写为sudoku，发音为sue-do-koo;su=数字，doku=单一;在日语中，只取复合词的第一个汉字来形成一个较短的版本是一种常见的做法。1986年，Nikoli引入了两项创新，保证了谜题的流行：给定数被限制在不超过30个，谜题变得对称（这意味着给定数分布在旋转对称的单元中）。它现在发表在日本主流期刊上，如朝日新闻。2005年，数独的流行程度激增G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）7981RNB 一NBRA OMNS NE MEUA OBSME OMSO R E S N M B 一 UN M U 一B E R O SS B 一 O U R M N EB O R M E S 一 U NU S N R 一 B E M OE 一M N O U S B RM N S U R 一 O E B一U B E S O N R MR E O B M N U S 一数独游戏中的数字是为了方便而使用的如果数字被字母、形状、颜色或其他符号取代，它也同样数独不是一个数学或算术难题;数字之间的算术关系事实上，Penny Press在他们的scramblets版本中使用了字母; Knight FeaturesSyndicate也在他们的Sudoku Word中使用了字母（见图2）。FIG。 二、 ASudokuWordpuzzl e（《科学知识》杂志，2005年），并发表了一篇文章。 Comleterids s oe eR e d s o e r e S o e e s o e s& o s o一行或一列包含一个7个字母的单词。你说什么？《卫报》称这些为“godoku”，并将其描述为所需的字母在拼图下面：一旦排列好，它们就在左上角和右下角之间拼出一个主题词。这增加了一个额外的维度数独，因为它可能是猜测这个词是什么。这个谜题的吸引人之处在于，完成规则很简单，但得出答案所需的推理可能很困难。它还提出了一些有趣的问题，其中一些是开放的：测量一个难题的难度，构建新的数独，建立可能的数独的数量，确定一个单一的解决方案可能的难题的数量，优化解决方案的搜索等等。2.1一个NP问题约束编程已经普及到大众。在解决他们每天的数独难题时，成千上万的报纸读者应用约束编程中的经典传播方案，如X翼和剑鱼[4]-覆盖多个行和列的模式，寻找一个可以从相应列和行的其他列表中删除的候选数字-以找到解决方案。已知在n×n块的n2×n2板上解决数独谜题的一般问题是NP-完全的[15]。这给出了一些模糊的指示，为什么数独很难解决，但对于有限大小的董事会，问题也是有限的，可以通过一个知道整个搜索树的确定性有限自动机来解决。然而，对于非平凡的起始板，搜索树非常大，因此该方法是不可行的。一个有效的数独解决方案也是一个拉丁方。拉丁方是n×n用不同符号填充的表，每个符号都精确地出现82G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）79每行一次，每列正好一次。数独还附加了一个区域限制;尽管如此，标准9× 9网格的有效数独解决方案网格数为6， 670， 903， 752， 021， 072， 936， 960。这个数字等于九！×722× 27× 27， 704， 267， 971，其中最后一个因子是素数。 结果是通过逻辑和蛮力计算得出;这种分析的方法可以在[10]中找到。3定义和符号3.1求解方法如[12]所述，三个过程（扫描，标记和分析）是解决数独的经典技术。这些过程的应用是不确定的，因此数独求解器的实际性能取决于它们组合中的方法：如果盲目地应用这些过程，可能会发生组合爆破。理想情况下，人们需要找到这些技术的组合，以有效的方式找到解决方案扫描它在手术开始时进行，并在整个过程中定期进行。在分析期间可能需要执行多次。扫描由三种基本方法组成，可以交替使用：交叉影线，计数和交叉影线是通过消除过程来扫描行以识别特定网格中的哪一行然后对柱重复该过程。重要的是要系统地执行这个过程，检查所有的数字1-9。为了获得最快的结果，这些数字按其频率顺序考虑。对数字1到9在网格、行和列中出现的次数进行计数，试图识别丢失的数字。根据最后发现的数字计数可以加快搜索速度。高级解算器在扫描时查找当这些单元格都位于同一行（或列）和网格内时，它们可以在交叉影线和计数期间用于消除目的根据定义，更难的数独不能仅仅通过基本扫描来解决，需要检测突发事件。标记当没有更多的数字可以被发现时，扫描停止。此时，在空白单元格中标记候选编号非常有用。下标是一种流行的表示法：候选数字在单元格中写为下标。通常在报纸上使用这种方法是困难的，因为单元格空间很小。还有第二种带点的符号（左上角的点代表1，G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）7983右下角的点表示9）。这种表示法的优点是可以在原始数独上使用分析有两种主要的分析方法：排除法和假设法。从单元格中排除可能的数字允许留下唯一可能的选择。有许多消除策略。最常见的一种是不匹配的候选删除：如果每个单元中的候选数字的数量等于n，则具有相同可能数字的n个单元的集合被称为匹配。然后可以删除在不匹配单元格中的相同行、列或网格中的其他地方作为候选出现的数字例如，如果在同一行中有三个单元格，其中{2， 7， 8}作为其可能的数字集合，则可以从该行中的剩余单元格中丢弃2，7和8作为可能的数字使用假设方法（在[12]中称为归谬法），选择只有两个候选数字的单元格并进行猜测。然后，该过程继续得到的数独，如果没有找到解决方案，则尝试替代数字。3.2数独规则我们将数独表示为对象的定义3. 1一个sudokuoforddern可以由对象Cij，1 ≤i，j≤n组成，一个对象对应于第i行和第j列的每个单元格，其中每个对象具有以下属性：• Gij=n·int（（i−1）/n）+int（（j−1）/n）+1是单元格所在的网格属于• Pij是这个单元格中可能出现的数字的集合。当这个属性对于所有单元格都是酉集时，数独将被解决;如果P对于某些单元格为空，则数独没有解决方案。• Nij是P ij中元素的个数。请注意，没有必要将i和j视为附加属性，因为它们是单元格名称的一部分。标准的数独是一个9× 9的网格，也就是说，一个数独的阶数n=9。初始地，Pij等于{1，.，n}，除非Pij是给定g ij的单元，在这种情况下Pij={gij}。属性Gij和Nij是显式存储的，但可以从对象的其余元素中计算出来。我们将对单元格应用几个归约规则来获得数独的解决方案。目标是针对所有细胞达到Pij在这个过程中，由于假设规则，一个数独可能会被分成两个，为了区分一个和另一个，我们将包含相应的对象84G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）79括号中。因此，例如，两个9阶数独的表示将如下所示：[C11C12. C99] [C11C12. C99]。在解决数独的不同过程（扫描，标记和分析）中，我们考虑的主要策略是分析消除。它由下面的规则1定义，它从单元格中的可能数字集合中删除一个元素。我们用二阶和三阶简化的规则2和规则3补充了它，它们分别考虑两个和三个元素。规则4至6涵盖了与扫描过程相对应的几种意外情况。 假设策略使用数独分割规则（规则7和8）实现。接下来，我们将详细介绍每一条规则。 它们可以被理解为一个可能并发的系统中的局部转换规则，可以并发地应用于汤的不同片段：每个子块的上部的单元变成下面的单元，而其余的保持不变（因为属性Nij和Gij是从Pij计算的，我们没有明确提到它们的新值）。我们用（）c来表示一个集合的补集。规则1（一阶简化规则）如果一个单元格中只有一个数字是可能的，那么我们将这个数字从同一行、列或网格中所有其他单元格的 可 能 数 字 集 合 中删除。象征性地，Cij CiJjJCijCiJjJ其中：(i) i=iJ或j=jJ或Gij=GiJjJ，(ii) Pij={p}<$PiJjJ，并且C i j j j的属性PiJjJ等于PiJjJ-{p}。规则2（二阶简化规则）如果同一行（列或网格）中的两个单元格具有相同的可能数集合，并且其基数为2，则这些数字可以从同一行（列或网格）中的每一个其他单元格的可能数集合中删除：哪里Cij CiJjJ CiJJj jJ JCij CiJjJ CiJJj jJ J(i) i=iJ=iJJ或j=jJ=jJJ或Gij=GiJjJ=GiJJjJJ，(ii) Nij=NiJjJ= 2，(iii) Pij=PiJjJ;Pij=PiJJjJ/=P iJ J Jj，并且CiJJjJ J的属性P I JJ J Jj等于PiJJjJ J-Pij。规则3（三阶简化规则）如果同一行（列或网格）中的三个像元具有相同的可能数字集合，并且其基数为3，则可以从每隔一个像元的可能数字集合中删除这些数字G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）7985在同一行（列或网格）中。实际上，该规则可以稍微推广，允许集合的基数对于除了一个之外的一些单元为2Cij CiJjJ CiJJ JjJJ CiJJJjJJJCij CiJjJ CiJJ JjJJ CiJJJjJJJ哪里(i) i=iJ=iJJ=iJJJ或j=jJ=jJJ=jJJJ或Gij=GiJjJ=GiJJjJJ=GiJJJjJJJ，(ii) Nij=3; 2≤NiJjJ，NiJJjJ J≤ 3，(iii) PiJjJ，PiJJJjPij;PijPiJJjJ Jj，并且C i jjj j jjj的属性P i JJJjJJJ等于P i JJJjJJJ-P ij。可以添加进一步的简化规则，但它们并不需要，实际上匹配对它们来说要昂贵得多。规则4（只有一个数字规则）当一个数字在一行（列或网格）的任何单元格中都是不可能的，但只有一个，并且这个单元格的可能数字的集合的基数大于1，那么这个集合可以成为包含该数字的单例集合。象征性地，其中：Ci1j1{Cikjk}2≤k≤nCi1j1{Cikjk}2≤k≤n(i) 存在一个数N，1≤N≤n，使得N =ik或N=jk或对于所有1≤k≤n，N =Gikjk，(ii) Ni1j1>1，(iii) 存在一个数p，1≤p≤n，使得p∈Pi1j1n并且Ci 1 j 1的属性Pi 1 j1等于0{p}。.布拉奇2≤l≤nPiljl，规则5（只有两个数字规则）当两个数字p1和p2在一行（列或网格）的任何单元格中不可能，但两个，并且这些单元格的可能数字的集合具有大于2的基数，那么这些集合可以成为{p1，p2}。Ci1 j1C i2 j2{Cikjk}3≤k≤nCi1 j1C i2 j2{C ik jk}3≤k≤n其中：(i) 存在一个数N，1≤N≤n，使得N =ik或N=jk或对于所有1≤k≤n，N =Gikjk，(ii) Ni1j1，Ni2j2>2，(iii) .本文给出了一个新的定义，即：p1，p2，1≤p1，p2≤n，且p1，p2∈Pi1j1<$Pi2j2<$C3≤l≤nPiljl，并且Ci k j k的属性Pi 1 j1和Pi 2 j2都等于{p1，p2}。规则6（孪生规则）如果在一个给定的网格中，一个数字只可能出现在一行86G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）79（或一列）中，那么这个数字可以从所有可能出现的数字中删除。G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）7987J在同一行（或列）但不同网格中的单元格。Ci0j0{Cikjk}1≤k≤nCi0j0{Cikjk}1≤k≤n其中：(i) 存在一个数N，1≤N≤n，使得N=Gikjk，对所有 1≤k≤n，(ii) i0ik和j0jk对于所有4≤k≤n，(iii) i0=i1或j0=j1，(iv) 存在一个数p，1≤p≤n，使得p∈Pi0j0<$Pi1j1<$.布拉奇4≤l≤nPiljl，并且Ci0j 0的第一个预存集合的属性P i 0 j0等于Pi0j0−{p}。规则7（通用数独拆分规则）当其他规则都不能应用时，此规则将数独拆分。我们选择一个可能数字最少（大于1）的单元格。然后用第一个可能的数字创建一个数独，用剩下的可能的数字创建另一个数独：Cij {Ckl}k/=i，l/=j，Cij{C kl} k i，l jCij{Ckl}k i=i，li=j如果满足这些条件：(i) Nij≥2且Nij最小（但大于1），(ii) p∈Pij，Cij的属性P i j等于{p}，Cij的属性Pi j等于Pij−{p}。规则8（数独拆分规则）这条规则是前一条规则的特例，当单元格中可能的数字数量等于2时。每一条规则的正确性都直接取决于它们的定义。然而，它的应用不会导致一个并发系统：如果数独有几个解决方案，那么根据规则的执行顺序，达到的解决方案可能会有所不同;当数独有唯一的解决方案时，这是可以获得的。系统正在终止：即使规则7引入了一个新的数独，每个规则都会减少一个单元格中可能数字集合4重写逻辑与莫德Maude [8，9]是一种高性能语言和系统，支持广泛应用的等式和重写逻辑计算Maude的关键新颖之处在于，除了有效地支持方程计算和代数规范之外，它还支持重写逻辑计算。重写理论是四元组T=（Ω，E，L，R），其中（Ω，E）是等式逻辑中的理论，L是规则的标签集合，R是将系统的局部状态转换公理化的标签重写规则集合。R中的一些规则可能是有条件的。在数学上，重写规则的形式为l：t−→tJ，如果C，其中t，t项的类型相同，可以包含变量。直觉，一个规则88G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）79描述了系统中的局部并发转换：在任何地方找到t的替换实例σ（t），可以发生该状态片段到新的局部状态σ（tJ）的局部转换。我们可以把等式理论看作重写理论的特殊情况，其中标签集L和规则集R都是空的;这样，等式逻辑自然地表现为重写逻辑的子语言。Maude是一种语言，其模块是重写逻辑的理论。最一般的Maude模被称为系统模，并被写为modTendm，其中T是重写理论，其语法与相应的数学符号非常接近。重写理论T=（Ω，E，L，R）的方程理论（Ω，E）中的方程E被表示为一个并集E=A<$EJ，其中A是作为签名Ω中某些运算符的属性引入的一组方程公理-例如，运算符+可以用关键字ask和ask-声明为关联和交换的，其中EJ是一组方程，假设它是Church-Rosser的，并以公理A为模终止。Maude支持重写这些等式属性的模不同组合：运算符可以被声明为结合的、可交换的、有单位的和幂等的。4.1莫德的数独我们的数独系统模块叫做SUDOKU。mod数独是我们首先向其中导入一些预定义的模块，这些模块定义自然数、引用标识符以及字符串和数字的转换。Maude通过允许定义模块层次结构为模块化提供了有用的支持;一个模块可以在不同的模式下导入其他Maude模块作为子模块，在这种情况下使用关键字protecting（可以缩写为pr）：pr NAT。每日一次。pr转换。我们提出的解决数独问题的框架构成了一个基于对象的系统的例子[9，第8章]。Maude通过一个名为CONFIGURATION的预定义模块，以简单直接的方式支持此类系统的规范。然而，我们不使用这个模块，因为我们希望我们的输出以表格的方式格式化，并使用不同的颜色，我们将显式地声明所有的运算符，我们将用它们来介绍Maude语法。如前所述，数独中的单元格对应于对象，我们将使用消息来显示谜题的当前状态：SearchingSolution，NoSolution，FinalSolution。这样的对象和消息的因此，我们为对象和消息声明排序，它们是配置的子排序，以及对象和类标识符（称为Oid和Cid）。排序Oid Cid对象消息配置。subsort对象消息<配置。为了创建对象，我们引入了关键字op，一个操作符<：|>那G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）7989接受一个对象标识符、一个类标识符和一组属性作为参数。操作<_：_|_>：Oid Cid AttributeSet ->Object [ctor object format（n r！ o g otm！ ot d）]。下划线允许指定mix fix语法，并且是应该写入参数的占位符。(The括在方括号中的命令只是指定输出的格式[9，Chapter 4]。配置是用一个空语法（）的运算符声明的，它是结合的、可交换的，并且有一个单位元素。op none：->配置。op：配置配置->配置[ctor config aspherid：none]。求解过程的当前状态将表示为排序项数独，它由一组数独组成，每个数独都被双角包围排序数独。操作无：-> 数独op<<_>>：配置->数独。欧泊颗数独OUBK->数独[ctorconfigasblogid：none].对象的属性属于一个新的排序属性，它是使用_，_构建的AttributeSet。对属性AttributeSet排序。subsort属性 AttributeSet。op _，_：AttributeSet AttributeSet -> AttributeSet[ctor阿糖胞苷：无格式（m！o sm！o）]。对于我们的数独规范，我们需要声明与每个单元格相关联的三个属性：它所属的网格，可以放置在其中的可能数字的集合，以及它的基数;列和行将由单元格标识符给出。属性被声明为返回排序Attribute项的运算符。opgrd：_ ：Nat->Attribute。op pss：_：Set-> Attribute。op num：_：Nat -> Attribute。操作id：Nat Nat -> Oid。- 行和列所有这些声明都指定了表示数独和我们在Maude中的求解过程所需的核心语法。现在，它们的行为通过方程和规则来具体化。使用关键字eq和变量声明方程关键字var。例如，返回关联网格的运算符可以将列C和行R的单元格指定为op grd：Nat Nat -> Nat.vars R C：Nat.等式grd（R，C）=（sd（R，1）<$3）* 3+（sd（C，1）<$3）+1。其中sd和quo分别是对称差和整数商的算子数独的初始棋盘可以指定为常数项数独。为了避免显式编写数独的完整表示的繁琐任务（9× 9单元格及其对应的行，列，数字，网格，... . ，对于9阶的数独），我们使用了几个可转换运算符，将数独更接近于基于对象的格式。例如，对于图1中的数独：欧泊颗数独（Sudoku）eq数独=90G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）79<>.例如，这里，辅助运算符fill将给定的数放置在它们相应的单元格中，从而使它们的可能数集合成为单例，而其余的单元格将具有{1， 2， 3， 4，5， 6， 7， 8， 9}作为它们的可能数集合排序列表是一种辅助排序，自然数列表是用操作符_;_以通常的方式构造的[9，第7章]。op fill：Nat Nat List->Object。eqfill（R， C，（N;LL））=如果C== 9，则填充（sR，1，LL）else fill（R，s C，LL）fi.eqfill（R， C，N）=。算子和方程一起定义了系统的静态部分。 接下来，我们需要定义它的动力学，即系统朝着解决方案的方向发展的方式，通过捕捉3.1节中解释的解决数独问题的过程的规则。当然，我们的目标是找到一个存在的解（可能的数字集合对于每个单元格来说都是一个单例），或者返回一个警告它不存在的消息（一些可能的数字集合变成空的）。我们的每一个重写规则都减少了某个单元格的可能数集合中的元素数，这一方式忠实地模仿了3.2节中给出的求解规则的表示。我们通过介绍其中的两个来说明它们是用Maude写的;对于其他的，我们请读者参阅www.example.comhttp://maude.sip.ucm.es/~miguelpt/bibliography上的文件。Sudoku Split规则将一个数独分成两个，当可能的数独数量如果一个单元格中的数字等于2，则用第一个可能的数字创建一个数独，用第二个可能的数字创建另一个数独，var VConf：配置。rl [sudokuSplit2]：<=><<.如果数独项的单元格在其可能的数字集合中只有两个元素P1 P2，则在这种情况下，该术语将被重写为一个具有两个串联数独术语的术语：一个以P1作为其可能数字的集合，另一个以P2作为其可能数字的集合。G. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）7991作为另一个例子，为了说明条件重写规则的使用，让我们考虑二阶简化规则：如果同一行（列或网格）中的两个单元格具有相同的可能数字集合，并且其基数为2，则可以从同一行（列或网格）中的每个其他单元格的可能数字集合中删除这些数字：crl [simplify2nd]：=> if（（R1 == R2）and（R1 == R3））or（（C1 == C2）and（C1 == C3））或（（G1 == G2）和（G1 == G3））。其余的数独规则也以类似的方式表示。除了解决数独的规则外，还有一些方程式和规则来处理“维护”问题：当没有可能的解决方案时完成程序，当最终解决方案已经达到时例如，我们已经找到了一个解决方案，因此可以停止求解过程，如果可能的数字集合的最大和最小基数（由辅助运算符maxCard和minCard计算）都是等于1：ceq msg（'SearchingSolution）VConf >>=<>if（maxCard（VConf）== 1）and（minCard（VConf）== 1）.最后，为了以所需的格式显示最终项（解决的数独），将一个新的属性添加到表示单元格的对象中，该对象被分配给给定行中所有值的列表：op val'：_：List ->Attribute。eq msg= msg.然后，当存在解时，最终项具有以下形式：<（srew sudoku usingsolve.）用策略重写：数独数独（Sudoku）：<>5最后发言我们在本文中介绍了一个案例研究如何使用Maude执行并解决数独。我们首先以面向对象的方式展示了数独的表示，并介绍了解决它们的规则，其在Maude中的实现 由于这些规则的盲目应用会引起组合爆炸，我们已经解释了如何利用MaudeG. Santos-García，M.Palomino/Electronic Notes in Theoretical Computer Science 176（2007）7993策略语言以非昂贵的方式应用规则。我们的方法的主要优势是数独在莫德表示的自然性和容易与解决过程是implemented。该规范可以很容易地修改，以处理任意顺序的数独，只需扩展规则，添加额外的对象来表示额外的单元格。然而，正是这种需要在规则中增加额外的子项，防止使用单一的规范来涵盖所有订单;这样的规范可以通过诉诸Maude的元水平[ 9 ]来编写 为了说明扩展是如何工作的，对于解决数独怪物（4阶数独）的规范，以及本文中提出的数独求解器的完整规范，可在http://maude.sip.ucm.es/~ miguelpt.另一方面，我们的实施的弱点在于它的效率。即使使用策略来修剪搜索树，我们的实现也无法与网络中可用的众多求解器（例如，[5、6、7]）。确认我们欢 迎 AlbertoVerdej o ndNarcoMart′s-Olietforhelpfulcommentsanddi s-cussions（特别是关于战略语言的），以及匿名推荐人的建议。引用[1] 这是我的女儿德雷尔·马加兹。 http://www.dellmagazines。com/.[2] 从Nikoli网站的。http://www.nikoli.co.jp/puzzles/[3] 数独的历史，康思 编辑部 http://www.