发帖
雷达卡
摘要翻译：
消解是推理规则，是大多数自动推理过程的基础。在这些过程中，输入公式首先被转换成合取范式(CNF)的均衡公式，然后表示为一组子句。演绎开始于通过解析来推断新的子句，并一直进行到空子句被产生或子句集合的可满足性被证明为止，例如，因为不能产生新的子句。在本文中，我们将注意力限制在量化布尔公式的求值问题上。在这种情况下，如果在CNF中给出一个公式，如果使用一种称为Q-分辨率的分辨率形式，上述推导过程是合理和完整的。我们在项上引入q-分辨，用于析取范式中的公式。我们证明了基于命题可满足性的Davis-Logemann-Loveland过程(DLL)的QBFs的大多数可用过程所进行的计算对应于一棵树，其中项和子句的Q-分解交替。这为引入学习提供了理论基础，对应于记录与树的节点相关联的Q分辨率公式。我们讨论了与在基于DLL的过程中引入学习相关的问题，并提出了解决方案，扩展了来自命题可满足性文献的最新建议。最后，我们证明了我们的基于DLL的求解器经过学习扩展后，在2003年QBF求解器比较评估中的基准测试中表现明显更好。
---
英文标题：
《Clause/Term Resolution and Learning in the Evaluation of Quantified
Boolean Formulas》
---
作者：
E. Giunchiglia, M. Narizzano, A. Tacchella
---
最新提交年份：
2011
---
分类信息：
一级分类：Computer Science 计算机科学
二级分类：Artificial Intelligence 人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--
---
英文摘要：
Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures, the input formula is first translated into an equisatisfiable formula in conjunctive normal form (CNF) and then represented as a set of clauses. Deduction starts by inferring new clauses by resolution, and goes on until the empty clause is generated or satisfiability of the set of clauses is proven, e.g., because no new clauses can be generated. In this paper, we restrict our attention to the problem of evaluating Quantified Boolean Formulas (QBFs). In this setting, the above outlined deduction process is known to be sound and complete if given a formula in CNF and if a form of resolution, called Q-resolution, is used. We introduce Q-resolution on terms, to be used for formulas in disjunctive normal form. We show that the computation performed by most of the available procedures for QBFs --based on the Davis-Logemann-Loveland procedure (DLL) for propositional satisfiability-- corresponds to a tree in which Q-resolution on terms and clauses alternate. This poses the theoretical bases for the introduction of learning, corresponding to recording Q-resolution formulas associated with the nodes of the tree. We discuss the problems related to the introduction of learning in DLL based procedures, and present solutions extending state-of-the-art proposals coming from the literature on propositional satisfiability. Finally, we show that our DLL based solver extended with learning, performs significantly better on benchmarks used in the 2003 QBF solvers comparative evaluation.
---
PDF链接：
https://arxiv.org/pdf/1111.0860
京公网安备 11010802022788号
