发帖
雷达卡
摘要翻译：
本文提出了一种独立的SAT预处理器，它能够执行大多数已知的预处理技术。对SAT中的公式进行预处理对性能很重要，因为可以消除冗余。预处理器是SAT求解器riss的一部分，被称为协处理器。不仅riss，而且MiniSat2.2也从中受益，因为MiniSat的SatELite预处理器没有实现最新的技术。协处理器通过使用更先进的技术，可以进一步减少公式中的冗余，提高整体求解性能。
---
英文标题：
《Coprocessor - a Standalone SAT Preprocessor》
---
作者：
Norbert Manthey
---
最新提交年份：
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中的材料。
--
---
英文摘要：
In this work a stand-alone preprocessor for SAT is presented that is able to perform most of the known preprocessing techniques. Preprocessing a formula in SAT is important for performance since redundancy can be removed. The preprocessor is part of the SAT solver riss and is called Coprocessor. Not only riss, but also MiniSat 2.2 benefit from it, because the SatELite preprocessor of MiniSat does not implement recent techniques. By using more advanced techniques, Coprocessor is able to reduce the redundancy in a formula further and improves the overall solving performance.
---
PDF链接：
https://arxiv.org/pdf/1108.6208
京公网安备 11010802022788号
