Breaking the PPSZ Barrier for Unique 3-SAT
Breaking the PPSZ Barrier for Unique 3-SAT
复制标题
打破独特 3-SAT 的 PPSZ 障碍
DOI：
10.1007/978-3-662-43948-7_50
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Timon Hertli
中科院分区：
文献类型：
--
作者：
Timon Hertli
由Paturi， Pudlák， Saks和Zane （FOCS 1998）提出的PPSZ算法是目前已知最快的（Promise） Uniquek-SAT算法。我们给出了一个改进算法，该算法具有指数速度更快的唯一3-SAT边界。对于唯一可满足的3-CNF公式，我们做以下区分：如果只有一个文字满足唯一可满足赋值，我们称子句为临界。如果一个公式有许多关键子句，我们观察到PPSZ本身已经更快了。如果总共只有几个子句，我们使用Wahlström （ESA 2005）的算法，在这种情况下，它比PPSZ快。否则，我们就会得到一个只有少数关键子句和许多非关键子句的公式。非关键子句至少满足两个字面量；我们将展示如何利用这一点来改进PPSZ。
The PPSZ algorithm by Paturi, Pudlák, Saks, and Zane (FOCS 1998) is the fastest known algorithm for (Promise) Uniquek-SAT. We give an improved algorithm with exponentially faster bounds for Unique 3-SAT.For uniquely satisfiable 3-CNF formulas, we do the following case distinction: We call a clause critical if exactly one literal is satisfied by the unique satisfying assignment. If a formula has many critical clauses, we observe that PPSZ by itself is already faster. If there are only few clauses in total, we use an algorithm by Wahlström (ESA 2005) that is faster than PPSZ in this case. Otherwise we have a formula with few critical and many non-critical clauses. Non-critical clauses have at least two literals satisfied; we show how to exploit this to improve PPSZ.