An Exponential Time/Space Speedup For Resolution
An Exponential Time/Space Speedup For Resolution
复制标题
分辨率的指数时间/空间加速
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
T. Pitassi
中科院分区：
文献类型：
--
作者：
Philipp Hertel;T. Pitassi
可满足性算法已成为解决各种现实问题的最实用和最成功的方法之一，包括硬件验证，实验设计，规划和诊断问题。成功的主要原因是基于分辨率的SAT高度优化算法。其中最成功的是子句学习，这是一种基于缓存中间子句的DPLL方案，这些子句在整个回溯搜索过程中都是“学习”的。这种方法的主要瓶颈是空间，因此已经有大量的研究旨在确定用于决定缓存哪些信息的良好算法。哈肯首先提出了一个正式的方法来解决这个问题，本-萨森[3]提出了一个问题，即是否有一个时间/空间权衡的解决方案。我们的主要结果是一个最佳的时间/空间权衡的分辨率。也就是说，我们提出了一个无限的命题公式，其最小空间证明都有指数时间，但如果只允许三个额外的存储单元，那么公式可以证明在线性时间。我们还证明了另一个相关定理。给定一个不可满足公式F和一个整数k，归结空间问题是确定F是否有一个归结证明，该证明可以使用空间k来验证。我们证明了这个问题是PSPACE完全的。
Satisfiability algorithms have become one of the most practi cal and successful approaches for solving a variety of real-world problems, including hardware verifi cation, experimental design, planning and diagnosis problems. The main reason for the success is due to highly optimized algorithms for SAT based on resolution. The most successful of these is clause learning, a DPLL scheme based on caching intermediate clauses that are “learned” throughout the backtrack search procedure. The main bottleneck to this approach is space, and thus there has been a tremendous amount of research aimed at identifying good heuristics for deciding what information to cache. Haken first suggested a formal approach to this issue, and Ben-Sasson [3] posed the question of whether there is a time/space tradeoff for resolution. Our main result is an optimal time/space tradeoff for resolution. Namely, we present an infinite family of propositional formulas whose minimal space proofs all have exponential time, but if just three extra units of storage are allowed, then the formulas can be proved in linear time. We also prove another related theorem. Given an unsatisfiabl e formula F and an integer k, the resolution space problem is to determine if F has a resolution proof which can be verified using space k. We prove that this problem is PSPACE complete.