Showing 1–3 of 3 results for author: Hertli, T

Breaking the PPSZ Barrier for Unique 3-SAT

Authors: Timon Hertli

Abstract: The PPSZ algorithm by Paturi, Pudlák, Saks, and Zane (FOCS 1998) is the fastest known algorithm for (Promise) Unique k-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 ha… ▽ More The PPSZ algorithm by Paturi, Pudlák, Saks, and Zane (FOCS 1998) is the fastest known algorithm for (Promise) Unique k-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 allover, 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. △ Less

Submitted 17 February, 2014; v1 submitted 11 November, 2013; originally announced November 2013.

Comments: 13 pages; major revision with simplified algorithm but slightly worse constants

MSC Class: 68R05; 68W20; 68W40 ACM Class: F.2.2; G.2.1

3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General

Authors: Timon Hertli

Abstract: The PPSZ algorithm by Paturi, Pudlák, Saks, and Zane [1998] is the fastest known algorithm for Unique k-SAT, where the input formula does not have more than one satisfying assignment. For k>=5 the same bounds hold for general k-SAT. We show that this is also the case for k=3,4, using a slightly modified PPSZ algorithm. We do the analysis by defining a cost for satisfiable CNF formulas, which we pr… ▽ More The PPSZ algorithm by Paturi, Pudlák, Saks, and Zane [1998] is the fastest known algorithm for Unique k-SAT, where the input formula does not have more than one satisfying assignment. For k>=5 the same bounds hold for general k-SAT. We show that this is also the case for k=3,4, using a slightly modified PPSZ algorithm. We do the analysis by defining a cost for satisfiable CNF formulas, which we prove to decrease in each PPSZ step by a certain amount. This improves our previous best bounds with Moser and Scheder [2011] for 3-SAT to O(1.308^n) and for 4-SAT to O(1.469^n). △ Less

Submitted 5 May, 2011; v1 submitted 10 March, 2011; originally announced March 2011.

Comments: 12 pages, no figures; critical variables are now called frozen, added reference to Makino et al., shortened some proofs and fixed typos

ACM Class: F.2.2; G.2.1

Improving PPSZ for 3-SAT using Critical Variables

Authors: Timon Hertli, Robin A. Moser, Dominik Scheder

Abstract: A critical variable of a satisfiable CNF formula is a variable that has the same value in all satisfying assignments. Using a simple case distinction on the fraction of critical variables of a CNF formula, we improve the running time for 3-SAT from O(1.32216^n) by Rolf [2006] to O(1.32153^n). Using a different approach, Iwama et al. [2010] very recently achieved a running time of O(1.32113^n). Our… ▽ More A critical variable of a satisfiable CNF formula is a variable that has the same value in all satisfying assignments. Using a simple case distinction on the fraction of critical variables of a CNF formula, we improve the running time for 3-SAT from O(1.32216^n) by Rolf [2006] to O(1.32153^n). Using a different approach, Iwama et al. [2010] very recently achieved a running time of O(1.32113^n). Our method nicely combines with theirs, yielding the currently fastest known algorithm with running time O(1.32065^n). We also improve the bound for 4-SAT from O(1.47390^n) [Iwama, Tamaki 2004] to O(1.46928^n), where O(1.46981^n) can be obtained using the methods of [Iwama, Tamaki 2004] and [Rolf 2006]. △ Less

Submitted 19 May, 2011; v1 submitted 24 September, 2010; originally announced September 2010.

Comments: 12 pages, 2 figures, corrected a typo in the title, added appendix with bound O(1.32065^n)

ACM Class: F.2.2; G.2.1