在线获取：ASP程序设计方法的理论计算机科学电子笔记354（2020）29-44

可在www.sciencedirect.com在线获取理论计算机科学电子笔记354（2020）29-44www.elsevier.com/locate/entcs走向一个答案集程序设计方法，用于按照半自动方法Flavio Everardoa，[0000−0002−6421−3158]，1 Mauricio Osorioba波茨坦大学，德国电子邮件：Eschavio.cs.uni-potsdam.debUniversidad de las Americas Puebla，Mexico电子邮件：osoriomauri@gmail.com摘要答案集编程（ASP）是一种成功的基于规则的形式化建模和解决知识密集型组合（优化）问题。尽管它在学术和工业上都取得了成功，自动源代码优化和软件工程等挑战仍然存在。这是因为编码到ASP中的问题与等效的表示相比可能没有期望的解决性能。基于这两个挑战，本文有三个主要贡献。首先，我们提出了一个发展过程中的方法来实现ASP程序，忠实于现有的方法。其次，从开发过程出发，介绍了作为基础的ASP编码。第三，我们展示了使用ASP来逆转标准的解决过程。也就是说，提前知道答案集，并期望强等价属性，本文最初的动机是搜索的命题公式（如果它们存在），表示一个新的聚合运算符的语义特别是，平价聚合。这个集合体是一个对来自Xorro的现有奇偶校验（XOR）约束的改进，其中Xorro缺乏表达性，即使这些约束完全适合于诸如采样或模型计数之类的推理模式。为此，这个扩展版本涵盖了奇偶校验约束以及xorro系统的基础。因此，我们在示例和所提出的奇偶约束方法中进行了更多的研究。最后，我们讨论我们的结果，通过显示唯一可用的表示，满足与经典逻辑异或运算符不同的性质，这也与异或运算符的奇偶约束语义一致。关键词：nswer集规划，组合优化问题，奇偶凝聚算子1介绍答案集编程（ASP; [5]）是一种基于规则的形式主义，用于建模和解决知识密集型组合（优化）问题。ASP1与墨西哥普埃布拉的莫恩特里校园技术学校合作。https://doi.org/10.1016/j.entcs.2020.10.0041571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。30F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）29高效求解引擎，允许指定给定的（搜索）问题，而不是编程算法来解决它。换句话说，给定一个搜索问题，程序员指定搜索空间域和问题特定属性。结合起来，让ASP求解器提出称为答案集的解决方案目前，ASP已经足够健壮和成熟，拥有许多重要的语言结构，如聚合、（弱）约束、不同类型的否定和优化语句，以及高性能的求解器。最先进且屡获殊荣的ASP求解器的一个例子是clasp[7]，它展示了其竞争力和多功能性，自2011年以来在各种求解器竞赛中获得第一名（例如，ASP、CASC、MISC、PB和SAT竞赛）。2clasp与groundergringo [9]相结合，构成clingo[10]，一个基于ASP的逻辑程序的系统。对于本文，我们希望读者熟悉ASP。有关技术方面，包括理论工作，实现和应用，请参见[11，8，10]。 [13]我们把它当作一种自我介绍。 完整阅读ASP。尽管ASP在学术界和工业界都取得了成功，3在规划，调度，配置，设计和诊断等领域（仅举几例），自动源代码优化和软件工程等挑战仍然存在，需要将软件工程方法和工具集成到ASP中[4]，幸运的是，它们是携手并进的。基于这两个挑战，本文有三个主要贡献。首先，我们提出了一个实现ASP程序的方法的开发过程，（尽可能）忠实于[14]提出的方法。其次，我们提出了属于元程序[12]范畴的ASP编码，作为我们开发过程的基础。第三，我们展示了使用ASP来逆转标准的解决过程。也就是说，提前知道答案集，并且期望强等价属性，如果它们存在，则按照[24，25]的方法彻底重建ASP程序。值得注意的是，本文是[6]的扩展版本，其中所提出的方法朝向更一般化的框架，是搜索表示新聚合算子语义的不同命题公式（如果存在）的结果特别是，这个操作符试图表现为奇偶校验聚合，作为对xorro已经存在的奇偶校验约束的改进。尽管这些约束完全适合于采样或模型计数等推理模式[42，41，39，40，43]，但它们对其他应用缺乏表达能力，这些应用也在安全性测试（SAT）[2]的邻近领域，如密码学[45，3]。为此，本文其余部分的结构如下。在第2节中，我们重点介绍了[6]中使用的非标准概念，用于ASP程序实现，如强等价（SE）的形式化定义，从G3的3值逻辑中的解释构造公式的方法，这与Here-and-There（HT）的逻辑直接相关。还有，2有关扣、奖杯和赛道的更多详细信息，请参见http://potassco.sourceforge.net/trophy。HTML.3一个不完整但庞大的ASP应用程序列表：https：//www.dropb ox.com/s/pe261e4qi6bcyyh/aspAppT able.pdfF. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）2931我们涵盖了从软件工程的角度设计和开发ASP程序的最佳实践。在结束这一节时，我们将简要介绍奇偶约束的形式以及xorro系统。为了设置预期过程的上下文，第3节展示了一个使用ASP的运行示例，作为对标准求解过程的概述从那里，我们通过显示唯一可用的表示来讨论我们的结果，该表示满足与经典逻辑XOR运算符不同的性质，这也与xorro的奇偶约束的语义一致。最后，我们总结了本文，并在第4节中指导未来的工作。2背景在本节中，我们将介绍我们所提出的方法中感兴趣的理论和实践方面，例如强等价的形式定义，使用哥德尔的3- v逻辑（G 3）[ 28 ]构造命题的形式，以及它与Here-and-There（HT）[ 27 ]逻辑的直接关系。我们从[14]中概括了ASP程序的设计和开发过程（已在行业中得到验证）。 最后，我们用XOR约束的基础以及xorro系统的简要描述来2.1强等效强等价[21]一词是关于ASP程序的，它是指当有两个程序（公式）F1和F2时，如果F1在哥德尔的三值逻辑（G3）中等价于F2，则F1与F2此外，通过约简[31]，如果对于每个原子集合X，约简FX和FX在经典逻辑中等价，则F1是SE到F2。是1 2相关说明强等价性在软件工程中的重要性从这个角度来看，不仅F1和F2包含相同的答案集（即F1<$F2），而且我们可以用另一个R扩展这两个公式，使得F1<$R和F2<$R产生相同的答案集（由F1<$SEF2表示）。2.2从G3或HT出于软件工程的目的，可以从HT中的解释构造命题公式（因此，ASP程序）[24，25]。然而，也可以使用G3逻辑，它相当于HT，并且关系是直接的。4对于G3的值0、1和2，0等于0或falseThere，1等于falseHere但trueThere，2等于T或trueHere。因此，考虑到两个逻辑G3和HT是等价的，我们在本文的剩余部分保留G3也就是说，给定4.我们只提到G3和HT逻辑中所需的概念。有关更多信息，我们可以参考读者[32，33]。32F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）29G3-解释I，我们应用[ 25 ]中的以下规范或条款C。 5为了创建一个子句，只要解释等于2，我们就应用下面的公式。更详细的示例见第3节的表3。.我知道了。I（v）=2好吧。我知道。（y→z）n（1）然后，为了构造命题公式，我们需要在结果子句上应用析取。这个命题公式可以根据（但不一定全部）[31，34，35]简化。具 体 的例子，请参见第3.1节。另一方面，我们可以应用相同的过程来为两个程序P1和P2找到一个反例，使得P1和P2（产生相同的答案集），但不是在结果子句上应用析取，而是将它们合并[30]。这个反例用来证明这两个程序是否是强等价的，这意味着P1等于P2，如前一节所示2.3软件工程[14]的工作提出了ASP程序开发的六步方法，遵循项目管理（PM）标准ISO21500：2012，还与项目管理知识体系（PMBOK）的生命周期开发背后的原则协调[26]。接下来，我们总结这六个领域，并指出它们与第3节中的方法学阶段的交叉点。(i) 在ASP比传统方法更强大的地方发现机会。正确定义并记录申请要求（第一阶段）。(ii) 设计一个有效的问题规范用小实例实现一个ASP规范进行测试（第二阶段在第一阶段的支持下）。(iii) 性能工程探索ASP程序实现的替代方案（在前两个阶段的支持下的第三阶段），并考虑“真实世界”大小的实例来评估其性能。6对于原型化过程，就像我们的方法学一样，我们更关注可读性而不是性能。(iv) 整合到现有的环境中从可行性研究中选择最佳的ASP方案。评估其他解决策略，并处理答案集。设计接口以实现完整的实现，使标准库和API受益于ASP解决方案，如clingo，使用Python或C++等语言。5原始公式是在HT的上下文中。 为了保持一致性，我们将其调整为G3.6特别是，对于第三个领域，我们只专注于探索ASP程序的替代方案及其实现。关于“真实世界”大小的实例，他们的性能评估I（w）=0I（x）=1I（y），I（z）=1，y/=zF. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）2933(v) 测试和调试通过自动化测试和调试ASP程序（如果适用）确保高质量。例如，ASP Debbuggers喜欢[18，19]。(vi) 维护专注于一个定义良好的程序结构，并从ASP的模块化中受益，以进一步适应。此外，[14]指出，在这个开发过程中，他们认为知识库设计和性能工程是最重要和最不同于传统软件工程的我们的方法属于这两个步骤，特别是，涵盖了前三个步骤，让我们看到发展最后三个步骤的机会此 外 ， 在 [14] 中 ， 他 们 将 面 向 对 象 的 方 法 （ OO ） 用 于 ASP ， 称 为OOASP，这允许分析OO软件模型及其使用ASP的实例OOASP方法已经在Siemens中成功实现，作为对任何OO建模环境的扩展。它已经与西门子内部工具一起进行了评估。这种建模方法目前超出了本文的范围，但它将被考虑用于未来的工作开发。2.4奇偶校验（XOR）约束为了定义奇偶性约束，让T和T分别代表布尔常量true和false给定原子a1和a2，1和a2的异或（简称XOR）用a1≠a2表示，如果 1或a2为真（但不是两者都为真），则满足。由于结合性，我们可以将n个不同原子的概念推广为1，...，作为n元奇偶校验或XOR约束，由多个应用程序的多个应用 程 序。因为它满足于在1，...，a n为真，我们可以简单地将其称为奇奇偶校验约束。类似地，偶数奇偶校验约束由1 × 1定义。在一个1，...，等等。然后，例如，如果1和2都没有或都没有保持，则满足1/2/1/2/1/2/1/2/2/1 最后，异或运算有四个基本性质，我们可以从中找到结合性和交换性。 另外两个属性是身份一个人的生活（resp. aT T）和自逆，其中aa。这些与单个原子的约束被称为一元。2.5Xorro系统奇偶性约束最近已被纳入ASP作为系统xorro[36]的基础，允许用户在ASP程序之上解决奇偶性约束。xorro是一个系统，它提供了六种替代方案，通过标准语法将奇偶校验约束处理到ASP解决方案中。一方面，xorro利用clingo的高级接口来集成外部约束和相应的推理形式。另一方面，xorro利用SAT中开发的复杂求解技术来处理奇偶约束。更准确地说，xorro提出了两种类型的方法，即依赖于奇偶校验约束的ASP编码的渴望方法，以及使用理论传播器的懒惰方法。34F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）29方法描述计数使用模2运算列表，树将二进制异或运算符转换为形成列表和树结构计数简单计算总赋值上的真值文字的计数器起来实现单元传播的栀子实现（非增量）Gauss-Jordan的消除表1处理奇偶性约束的异或clingo7表1总结了处理奇偶校验约束的六种实现。前三个对应于渴望，后三个对应于懒惰的方法。本文中的实验评估了不同的方法，考虑到它们对求解性能的影响，同时改变奇偶约束的数量和密度，与clingo求解时间（无奇偶约束）相比。结果表明，xorro尺度依赖于奇偶约束的数量，当增加采样中使用的高密度约束的数量时（XOR的大小为程序变量的一半），我们开始看到解决时间增加了。为了适应输入语言中的奇偶性约束，我们依赖于clingo1&奇数{1：p（1）}。2&偶数{ X：p（X），X>1}。也就是说，xorro通过集合名称&even和&odd扩展了clingo的输入语言，这些名称后面跟着一个集合，其元素是由逗号分隔的文字的组合条件的术语。 8在选择规则{p（1.. 3）}。，上面所示的奇偶性约束相当于异或运算p（1）和p（2）p（3）T，产生答案集{p（1）}和{p（1），p（2），p（3）}。目前，这些约束被解释为指令，并且在划分搜索空间时，它们充当不满足所讨论的奇偶性约束的答案集过滤器。9因此，第一个约束过滤出不包含原子p（1）的答案集，而第二个约束要求不包含或包含原子p（2）和p（3）。[7]渴望方法和懒惰方法的区别遵循可满足性模理论[1]中的方法论。[8]反过来，聚合中的多个条件项由子分隔。9目前，对等约束可能不会出现在机构或规则的首长中。F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）29353方法和做法本节描述并举例说明我们的方法，首先介绍一个使用ASP作为概述的运行示例，以逆转标准求解过程。 然后，我们深入研究围绕奇偶校验约束的底层ASP编码3.1运行实例让我们假设有一个名为ProgramBuilder的系统，它的核心被称为clingo，并包括（在其他功能中）三个阶段。第一阶段以一组答案集和可选的SE属性作为输入，并提供中间表示。第二阶段采用这个中间表示来构造一个起始命题公式。第三个也是最后一个阶段采用这个公式，并根据用户需求提出一个与初始公式强等效的新公式。ProgramBuilder系统受益于ASP的声明式方法，将一系列底层程序包含在一个称为SPF的单一程序中，该程序忠实地表示整个系统的工作流程。为了描述这项工作，让我们考虑一个非常简单的例子，目的是将我们的方法非常清楚有兴趣找到一个两个变量p和q的命题公式，使得它有{p}和{q}作为唯一的答案集，并丢弃空集，{p，q}。第一阶段从已知的答案集作为输入，系统调用clingo，让它猜测一个满足前面条件的公式。然而，在这方面，在这些条件下，clingo找到了超过300个不同的中间表示（潜在公式），满足给定的输入。如前所述，用户可以从SE属性中受益，以分隔更多的搜索。这意味着用户可以直接在SPF中指定要满足的所需属性例如，用户可以要求满足交换性、结合性和恒等性的表示。再次调用SPF和用户给定的属性，clingo遇到了四个中间表示。让我们提到，这些中间表示由基于G3的3x3矩阵组成，如2a和2b所示。现在假设我们有两个用户，第一个用户决定通过添加另一个属性（例如幂等性）来进一步细化搜索。现在clingo生成一个矩阵，允许用户进入第二阶段。相反，第二个用户要求ProgramBuilder从剩下的四个矩阵中选取两个矩阵M1和M2，推迟决定，并进入第二阶段。第二阶段如果用户有一个以上的矩阵，他或她可以进入一个对话过程，直到选择一个解决方案。然而，用户也可以保留矩阵并继续工作。假设用户有两个矩阵M1和M2，他或她想选择一个其中更具体地说，设M1和M2分别为表2a和2b我们可以看到，两个真值表2a和2b在一个值中不同，36F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）290 1 20 1 200 1 200 1 211 1 211 2 222 2 222 2 2(a)M1的真值表表2(b) M2真值表在G3的逻辑中，两个输入都等于1的M1和M2分集.两个输入都是1。 [10]如前所述，这些中间表示用于构造初始命题公式。ProgramBuilder接受每个矩阵并构造其相应的公式。让我们回想一下，每个公式都是子句的析取，其中每个子句对应于结果等于2的解释，并让函数F负责构建以下公式：F1=F（M1）=（p<$$>q）<$（q <$$>p）<$（p<$$>q）<$（q <$$>p）<$（p<$q）F2=F（M2）=（pq）p）q）p）pq）pq）ProgramBuilder可以警告用户，如果你添加另一个程序Q，包括规则（p<$$>q）<$（q <$$>p）到公式F1和F2，那么，答案集的计算（由函数表示）AS（F1<$Q）={{p}，{q}}，而AS（F2<$Q）={}。换句话说，对于第一种情况，存在一个单一的答案集{p，q}，与不满足的第二种情况相反。这意味着，F1/SEF2。值得一提的是，用户可以选择其中一个或继续到第三阶段。第 三 阶 段 系 统 采 用 每 个 公 式 ， 并 提 出 一 个 新 的 强 等 效 替 代 方 案 。ProgramBuilder配备了一个逻辑转换代数（关于SE），可以将F1转换为给定的标准形式。在这种情况下，F1被简化为析取p<$q<$（p<$q），即SE为构造的公式p<$q。11通过上面的例子，我们提出了一个第一步的方法，有可能将其实现到一个交互式软件中，通过定义的属性来构建ASP程序。此外，该软件可以包括转换模块，以可视化多种形式的构造程序。此外，这个例子有助于激发更一般的框架或具体示例的概念，如下所示。3.2寻找奇偶校验聚合语义值得一提的是，本文是通过应用Ferraris[23]的定义的命题公式（如果存在）来搜索奇偶集合的语义。这种聚合是对xorro已经存在的奇偶性约束的改进。换句话说，我们正在寻找一个运营商，[10]我们为读者提供这些表格，也是为了清楚起见。但是，它们可能与用户无关对于感兴趣的读者，G3的语义可以在[38]中找到.[11]关于简化的更多细节，我们参考[25]。F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）2937(at至少）两个条目，类似于关于ASP中某些SE属性的二进制XOR[12]让我们再次用问题的定义来激励自己问题定义。 给定（一组不完整的）答案集，以及可选的强等价属性作为输入，我们希望测试现有的中间表示或搜索新的中间表示，从ASP构建一个或多个命题公式（并在最近被ASP使用）。要做到这一点，我们可以添加我们的中间表示或遵循ASP的标准猜测和检查范例。在这两种情况下，都要测试候选解决方案的可行性，可能会产生零个、一个或多个答案集。 通常，这些答案集作为编码程序的解决方案，但对于我们的目的，它们是G3中的解释，允许我们构建公式。在深入研究这三个阶段之前，让我们解释一下我们有两种类型的答案集（由于我们的元编程方法），答案集作为输入，答案集作为中间表示。从现在开始，我们很容易将它们分别区分为答案集输入和答案集输出，并且我们可以本文遵循ASP的一般做法，通过分别提供一个实例和一个编码，将核心问题实现到ASP中 正如上面在问题的定义中所述，实例对应于答案集输入和SE属性，编码包括证明命题公式存在与否的方法。再一次，我们从已知的答案集input{p}和{q}开始，并再次丢弃空集和{p，q}，使用相同的变量p和q。 我们用原子答案集表示每个输入答案集，原子答案集有一个字符串值作为其参数，如清单1所示。1：-不是answer_set（“p”）。2：-不是answer_set（“q”）。3：-answer_set（“”）。4：- answer_set（“p q”）。清单1：作为实例一部分的答案集（answersets.lp）。由于要求是事先明确的，作为第一阶段的一部分，我们可以将经典逻辑XOR的四个基本属性表示为我们输入的一部分。这些性质与2.4节中的交换性、结合性、自逆和恒等式相同。13要查看ASP上下文中的这些SE属性，请参考清单2。1%%交换性：X xor Y = Y xor X2：- op（X，Y，R1），op（Y，X，R2），R1！=R2.4%%关联性：（X xor Y）xor Z = X xor（Y xor Z）5left（X，Y，Z，R）：- op（X，Y，W1），op（W1，Z，R）. %%左侧6right（X，Y，Z，R）：-op（Y，Z，W1），op（X，W1，R）.%%正确7：-左（X，Y，Z，R1），右（X，Y，Z，R2），R1！= R2.9%%自逆：X xor X = 010：- op（X，X，R），R！=0.[12]本文并不打算对奇偶校验集合及其语义进行完整的描述。我们只打算使用该方法作为一个系统的证明，以找到满足经典xor运算符性质的命题公式。13对于identity属性，一个变量pXORed with x，等于输入的双重否定。例如，p等于p。这在ASP中表示为约束：：-而不是p。38F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）29∨ ∧ ¬ ∨ ¬12%%同一性：X xor 0 =非X13：- op（X，0，Y），neg（X，X1），neg（X1，Z），value（Y），Y！= Z.清单2：经典XOR运算符（xorstreng.lp）的基本SE从上面的代码中，我们将每个属性表示为完整性约束，其中原子op（X，Y，R）对应于两个参数（变量）X和Y及其结果R的期望运算符。让我们继续前进，并提到这个原子是答案集输出或中间表示的一部分。在我们进入第二阶段之前，我们描述产生中间表示的编码。编码由四个部分组成，测试现有的中间表示或猜测一个新的，逻辑运算符的定义，理论完成，和G3持久性。当然，这是一个完全自然和直接的情况，测试经典的XOR公式作为第一次尝试，而不是直接要求一个中间表示。也就是说，我们首先对经典的XOR公式进行编码， （p q）（p q）转换为规则，如清单3所示。1op（X，Y，Z）：-或（X，Y，R1），neg（X，X1），neg（Y，Y1），或（X1，Y1，R2），和（R1，R2，Z）。清单3：经典XOR公式的编码（经典xor.lp）。在这种编码中，我们首先表示两个输入X和Y的析取，然后，我们对第二个析取的两个输入取反。最后，我们把两个结果结合起来。此外，我们可以用清单4中的选择规则代替清单3中的规则，而不是提出不同的中间表示，对它们进行编码并测试它们的可满足性，允许从任意两个值X和Y中对运算符op（X，Y，R）进行clingo猜测，从而得到R，这就是两个边界都设置为1的选择规则。11 {op（X，Y，Z）：value（Z）} 1：-value（X），value（Y）。清单4：通过G3中的解释猜测公式（guess formula.lp）。编码的第二部分是G3中逻辑运算符的定义and、or、negation和implications，如清单5所示。1value（0.. 2）。%% G3值3和（X，X，X）：-value（X）。4和（X，Y，X）：-值（X），值（Y），XY。5和（X，Y，Y）：-值（X），值（Y），Y X。7或者（X，X，X）：-value（X）。8或（X，Y，X）：- value（X），value（Y），Y X。9或（X，Y，Y）：- value（X），value（Y），XY。11neg（0，2）. neg（2，0）. neg（1，0）.13implications（X，Y，2）：-value（X），value（Y），X = Y。14implications（X，Y，Y）：-value（X），value（Y），X> Y。清单5：G3值和逻辑运算符（logicaloperators.lp）.为了找到或测试输出的答案，我们需要根据什么来描述它们F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）2939--我们称之为理论完成，如清单6所示。141completion（0，X，Y，R）：-neg（X，X1），neg（Y，Y1），and（X1，Y1，R）。2完成（1，X，Y，R）：-neg（X，X1），neg（X1，X2），neg（Y，Y1）和（X2，Y1，R）。3完成（2，X，Y，R）：-neg（Y，Y1），neg（Y1，Y2），neg（X，X1）和（X1，Y2，R）。4完成（3，X，Y，R）：-neg（Y，Y1），neg（Y1，Y2），neg（X，X1），neg（X1，X2），and（X2，Y2，R）。6属于（1，p）。属于（2，q）。属于（3，p）. 属于（3，q）。8code（0，"”）.code（1，“p”）.code（2，“q”）. code（3，“p q”）.10completion_asp（A_ID，X，Y，R）：- op（X，Y，Z），completion（A_ID，X，Y，C），and（Z，C，R）.12consistent（A_ID）：-completion_asp（A_ID，X，Y，R），value（R），R>0.13incomplete（A_ID）：-belongs（A_ID，x），completion_asp（A_ID，X，Y，Z），implications（Z，X，R），R 2.14incomplete（A_ID）：-belongs（A_ID，y），completion_asp（A_ID，X，Y，Z），implications（Z，Y，R），R 2。16answer_set（S）：- consistent（A_ID），not incomplete（A_ID），code（A_ID，S）.清单6：答案集的理论补全（theory completion.lp）。清单6中的前四条规则概括了这段代码的主要功能，它们捕获了关于输入p和q的所有可能答案集（与答案集输入相关）所需的补全。然后，第6行中的事实显示了常量p和q与所有可能的答案集之间的对应关系第10行形成关于操作符的补全。然后，完成必须是一致的（第12行），我们定义什么是不完全性（第13行和第14行）。最后，第16行，通过它们的相关代码以字符串表示导出相应的答案集。这些答案集必须满足一致性和完整性，以及答案集输入（清单1）。最后，我们需要保证G3持久性属性[29，25].它们显示在清单7中。 这里，第1行指出，如果存在一个解释{1，0，2}，则不可能存在另一个输入为2和0的解释，其评估为不同于2的任何其他值。第2行描述了换向属性，第3行指出，不可能导致1的解释来自不同于1的输入。1：- op（1，0，2），op（2，0，X），X！= 二、2：- op（0，1，2），op（0，2，X），X！= 二、3：- op（X，Y，1），X！= 1，Y！= 1.一、清单7：G3持久性（g3persistence.lp）解决实例和编码两者产生中间表示以移动到第二阶段。然而，对于这两种情况（使用经典的XOR公式或猜测一种），都没有答案集输出。这意味着不可能在ASP中将XOR运算符表示为两个参数函数，并且满足所有四个属性。尽管消极的解决方案，没有公式来构建，它是积极的意义上，这种方法可以节省时间，金钱和资源，从软件工程的角度来看。此外，这完全适合迭代软件工程方法，让用户[14]为了清楚起见，我们修改了关于示例性签名p，q的编码。然而，可以为给定的签名生成这种编码40F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）29解释条款{0， 1，2}¬p¬¬Q{0， 2， 2}¬pQ{1， 0， 2}¬¬p¬Q{2， 0， 2}p¬Q表3矩阵2的结果子句。回到初始或设计阶段，想知道需求。另一方面，根据我们的XOR动机，我们也会问自己，我们是否能找到一个公式，在语义上表现为xorro[36]中使用的奇偶约束。也就是说，我们正在寻找一个约束公式，丢弃候选答案集从一个独立的生成过程中，不满足这两个，答案集输入和SE属性。因此，XOR公式现在由两部分组成，生成部分与测试或约束相结合。生成过程由形式为xx的子句的合取组成，对于每个变量x。清单8显示了将关于任意两个值X和Y的所有答案集生成到谓词xor g/3中的编码。这个测试被建模为一个选择规则，类似于清单4中的规则，但是使用了新的谓词异或t/3。结合两者，它导致规则op（X，Y，Z）：- xor g（X，Y，Z1），xor t（X，Y，Z2），and（Z1，Z2，Z）.对于这种方法，需要指出的是，SE属性必须只计算公式的测试部分，而不是整个表达式或生成。1xor_g（X，Y，Z）：- neg（X，X1）、neg（Y，Y1）或（X，X1，Z1）或（Y，Y1，Z2）和（Z1，Z2，Z）.清单8：候选答案集的生成（generate.lp）。在穷尽了所有可能的中间表示之后，clingo发现了一个单一的答案集输出。这意味着，只有一个替代方案来将XOR表示为满足矩阵2中所示的上述性质的ASP中的约束。有了这个中间表示作为M1或M2形式的矩阵（来自运行示例），我们可以进入第二阶段。xor t（0，0，0），xor t（0，1，2），xor t（0，2，2）xor t（1，0，2），xor t（1，1，0），xor t（1，2，0）xor t（2，0，2），xor t（2，1，0），xor t（2，2，0）（二）由于我们只有一个表示，我们构造公式Fxort，它给出了表3中的以下条款，并采用公式Eq.1.一、这导致初始命题公式：Fxort=（q）q）pq）q）F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）2941最后，第三阶段提出Fxort的变换。例如，从Fx或t得到的公式或简化可以是（pq）q）。从相反的方向来看，我们可以通过给出一个命题公式，让clingo不仅测试它，而且搜索答案集，来反转所提出的方法。例如，让我们将简化的Fxort公式编码为：xor t（X，Y，Z2）：-或（X，Y，R1），neg（X，X1），neg（Y，Y1），或（X1，Y1，R2），和（R1，R2，Z），neg（Z，Z1），neg（Z1，Z2）。这个公式替换了清单1、4和3中的代码，并重用了前面提到的编码、逻辑运算符（清单5）、理论完成（清单6）和G3持久性属性（清单7）。因此，clingo得到了答案集{p}和{q}，以及矩阵2中所示的相同的G3表示。 这意味着所建立的公式在语义上表现为XORRO中使用的奇偶约束。最后，值得一提的是，目前我们有一个使用Python和clingo的初始和非常基本的实现。有关更多详细信息，请访问https：//github.com/flavioeverardo/Propositional-Formula-Builder-PFB网站。此外，还提供了一个完整的、可随时使用的编码，该编码将论文中的所有清单组合在一起，https://github.com/flavioeverardo/Propositional-Formula-Builder-PFB/blob/master/lpwww.example.com/full_xor_encoding.lp。4讨论自动生成声明式搜索问题的解决方案是人工智能最成功的领域之一[4]，其中答案集编程由于其对搜索问题的紧凑表示的全面支持而突出。此外，自动源代码优化的需要，以及ASP中的软件工程工具和方法学。受编码到ASP中的问题与等效表示相比可能不具有所需的解决性能的情况的启发。出于这些需要，我们提出了一个初步的开发过程中实现ASP程序的方法，现有的方法。我们将这个开发过程捕获到一个由ASP编码组成的初始原型中，该原型将标准的求解工作流程逆转为对命题公式的穷举搜索，所有这些都在ASP中。所得公式必须满足强等价（SE）性质以及已知或期望的答案集。本文是[6]的扩展版本，它允许我们在查找奇偶校验集合的语义的上下文中进行更多的研究，作为对xorro中使用的奇偶校验约束的改进。我们的方法，让我们不仅测试命题公式，但也要求他们的存在，通过ASP解决，铺平了道路，ASP程序的基准程序，找到一个最佳的表示。对于未来的工作，有太多的事情要做。首先，我们计划继续开发一个与拟议方法有关的完全集成的软件，包括用于重建更复杂公式的工具这个最初的原型42F. Everardo，M.Osorio/理论计算机科学电子笔记354（2020）29使用ASP在其整体，因为它是设想感谢高层次的接口，复杂的算法接地和解决，包括搜索算法和学习技术的基础上nogoods，等等。因此，该倡议构建了命题公式。然而，它还远远没有配备齐全的软件。一个可能的扩展是不仅可以构造命题公式，还可以构造非基础ASP程序。也就是说，包括变量。然后，我们可以受益于anthem[37]等工具，用于验证gringo输入语言中的SE程序。好处是我们可以安全地替换一段知识表示与另一个人无关。换句话说，我们可以安全地更改代码，而无需修改程序的语义在软件工程方面，据我们所知，[14]是描述标准软件工程过程的唯一方法，该过程包括ASP程序的开发和设计，并已在工业环境中进行了测试然而，我们的方法和原型都可以从ASP社区的其他几种技术中受益，这些技术与软件工程有关系，例如归纳逻辑编程（ILP）[15，16]，过程内容生成（PCG）[17]，ASP Debbuggers[18]（包括元编程[19]），以及称为ASPIDE的ASP IDE[20]。引用[1] 巴雷特角，Ragtiani，R.，Seshia，S.，Tinelli，C.：满足模理论。见：Biere等人[2]，第二章。26，pp. 825-885.[2] Biere，A.，Heule，M.，van Maaren，H.，沃尔什，T.（编辑）：满足性手册，人工智能和应用的前沿，卷。一百八十五IOS Press（2009）.[3] 苏斯，M.，Nohl，K.，卡斯特卢西亚角：将SAT求解器扩展到加密问题。Kullmann，O.（编辑）第12届国际 会 议 的 理 论 和 应 用 的 满 意 度 测 试 （ SAT 计 算 机 科 学 讲 义 ， 卷 。 5584 ， pp.244-257 Springer-Verlag（2009）.[4] S chaub，T.， Woltran，S.： Ans wersetprogrammingunleased！. KI-KünstlicheI ntelligenz，32（2-3），105-108，（2018）.[5] Lifschitz ， V. ： 答 案 集 规 划 。 在 逻 辑 编 程 和 非 单 调 推 理 国 际 会 议 pp. 373-374. Springer ， Berlin ，Heidelberg（1999）.[6] Everardo ， F.， 奥 索 里 奥 ， M. ： Towards an Answer Set Programming Methodology for ConstructingPrograms Following a Semi-Automatic Approach在2019年拉丁美洲推理新方法研讨会（LANMR 2019）上接受了Apper。[7] Gebser，M.，Kaufmann，B.，和Schaub，T.：Constructive Driven Answer Set Solving：From Theory toPractice （ 英 语 ： Constructive Driven Answer Set Solving ） Arti Ficial Intelligence ， 187 ， 52-89（2012）。[8] Gebser，M.，卡明斯基河，Kaufmann，B.，和Schaub，T.：在实践中解决问题。人工智能和机器学习综合讲座，6（3），1-238（2012）。[9] Gebser，M