• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>AI communications >Practical algorithms for unsatisfiability proof and core generation in SAT solvers
【24h】

Practical algorithms for unsatisfiability proof and core generation in SAT solvers

机译：SAT求解器中不满足证明和核生成的实用算法

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

摘要

Since Zhang and Malik's work in 2003 [19], it is well-known that modern DPLL-based SAT solvers with learning can be instrumented to write a trace on disk from which, if the input is unsatisfiable, a resolution proof can be extracted (and checked), and hence also an unsatisfiable core: a (frequently small) unsatisfiable subset of the input clauses.rnIn this article we first give a new algorithmic approach for processing these (frequently huge) traces. It achieves the efficiency of a depth-first traversal, while preserving the property that memory usage remains upper bounded by that of the SAT solver that generated the trace.rnThe second part of this article is about in-memory algorithms for generating SAT proofs and cores, without writing traces to disk. We discuss advantages and disadvantages of this approach and investigate why the current SAT solvers with this feature still run out of memory on long SAT runs. We analyze several of these in-memory algorithms, based on carefully designed experiments with our implementation of each one of them, as well as with (our implementation of) a trace-based one. Then we describe a new in-memory algorithm which saves space by doing more bookkeeping to discard unnecessary information, and show that it can handle significantly more instances than the previously existing algorithms, at a negligible expense in time.
机译：自Zhang和Malik于2003年开展工作[19]以来，众所周知，可以对具有学习功能的基于DPLL的现代SAT求解器进行检测，以在磁盘上写迹，如果输入不满意，则可以从中提取分辨率证明（和检查），因此也是一个无法满足的核心：输入子句的一个（通常很小）无法满足的子集。在本文中，我们首先提供了一种新的算法方法来处理这些（频繁地）跟踪。它实现了深度优先遍历的效率，同时保留了内存使用仍然是生成跟踪的SAT求解器的上限的属性。本文的第二部分是有关生成SAT证明和核的内存中算法。 ，而无需将跟踪写入磁盘。我们讨论了这种方法的优缺点，并研究了为什么目前具有此功能的SAT解算器在长时间运行SAT时仍会用尽内存。我们基于精心设计的实验（其中每个算法的实现以及基于跟踪的算法的实现），对其中的几种内存算法进行了分析。然后，我们描述了一种新的内存中算法，该算法通过进行更多簿记以丢弃不必要的信息来节省空间，并表明与以前的算法相比，该算法可以处理大量实例，而时间却可以忽略不计。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号