• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of Automated Reasoning >Simulating Circuit-Level Simplifications on CNF
【24h】

Simulating Circuit-Level Simplifications on CNF

机译：在CNF上模拟电路级简化

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Boolean satisfiability (SAT) and its extensions have become a core technology in many application domains, such as planning and formal verification, and continue finding various new application domains today. The SAT-based approach divides into three steps: encoding, preprocessing, and search. It is often argued that by encoding arbitrary Boolean formulas in conjunctive normal form (CNF), structural properties of the original problem are not reflected in the CNF. This should result in the fact that CNF-level preprocessing and SAT solver techniques have an inherent disadvantage compared to related techniques applicable on the level of more structural SAT instance representations such as Boolean circuits. Motivated by this, various simplification techniques and intricate CNF encodings for circuit-level SAT instance representations have been proposed. On the other hand, based on the highly efficient CNF-level clause learning SAT solvers, there is also strong support for the claim that CNF is sufficient as an input format for SAT solvers. In this work we study the effect of CNF-level simplification techniques, focusing on SatElite-style variable elimination (VE) and what we call blocked clause elimination (BCE). We show that BCE is surprisingly effective both in theory and in practice on CNF formulas resulting from a standard CNF encoding for circuits: without explicit knowledge of the underlying circuit structure, it achieves the same level of simplification as a combination of circuit-level simplifications and previously suggested polarity-based CNF encodings. We also show that VE can achieve many of the same effects as BCE, but not all. On the other hand, it turns out that VE and BCE are indeed partially orthogonal techniques. We also study the practical effects of combining BCE and VE for reducing the size of formulas and on the running times of state-of-the-art SAT solvers. Furthermore, we address the problem of how to construct original witnesses to satisfiable CNF formulas when applying a combination of BCE and VE.
机译：布尔可满足性（SAT）及其扩展已成为许多应用程序领域的核心技术，例如计划和形式验证，并且在今天继续寻找各种新的应用程序领域。基于SAT的方法分为三个步骤：编码，预处理和搜索。经常有人争辩说，通过以合取范式（CNF）编码任意布尔公式，原始问题的结构特性未反映在CNF中。与适用于更结构化的SAT实例表示形式（例如布尔电路）的相关技术相比，这应该导致CNF级预处理和SAT求解器技术具有固有的缺点。因此，已经提出了用于电路级SAT实例表示的各种简化技术和复杂的CNF编码。另一方面，基于高效的CNF级子句学习SAT求解器，也强烈支持CNF足以作为SAT求解器的输入格式的说法。在这项工作中，我们研究CNF级别简化技术的效果，重点是SatElite样式的变量消除（VE）和我们所谓的阻塞子句消除（BCE）。我们证明BCE在理论上和实践上对电路的标准CNF编码所产生的CNF公式都具有令人惊讶的有效效果：在没有对底层电路结构有明确了解的情况下，BCE可以达到与电路级简化和先前建议的基于极性的CNF编码。我们还表明，VE可以实现许多与BCE相同的效果，但不是全部。另一方面，事实证明，VE和BCE确实是部分正交的技术。我们还研究了结合BCE和VE来减小公式大小以及对最新SAT求解器的运行时间的实际效果。此外，我们解决了在结合使用BCE和VE时如何构造可满足CNF公式的原始证人的问题。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号