摘要翻译:
这是描述ZAP的三篇论文中的第三篇,ZAP是一个可满足性引擎,它基本上概括了现有的工具,同时保留了现代高性能求解器的性能特征。ZAP的基本思想是,传递给这类引擎的许多问题包含被所使用的布尔表示所掩盖的丰富的内部结构;我们的目标是定义一个表示,其中这种结构是明显的,可以用来提高计算性能。第一篇论文回顾了已有的利用问题结构来提高可满足性引擎性能的研究,第二篇论文表明,在任何特定的布尔理论中,问题结构可以用作用于单个子句的置换组来理解。我们通过讨论实现我们的想法所需的技术,并通过报告它们在各种问题实例中的性能来结束本系列。
---
英文标题:
《Generalizing Boolean Satisfiability III: Implementation》
---
作者:
H. E. Dixon, M. L. Ginsberg, D. Hofer, E. M. Luks, A. J. Parkes
---
最新提交年份:
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中的材料。
--
---
英文摘要:
This is the third of three papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high-performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal has been to define a representation in which this structure is apparent and can be exploited to improve computational performance. The first paper surveyed existing work that (knowingly or not) exploited problem structure to improve the performance of satisfiability engines, and the second paper showed that this structure could be understood in terms of groups of permutations acting on individual clauses in any particular Boolean theory. We conclude the series by discussing the techniques needed to implement our ideas, and by reporting on their performance on a variety of problem instances.
---
PDF链接:
https://arxiv.org/pdf/1109.2142