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) [Rolf 2006] to O(1.32153^n). Using a different approach, Iwama et al. 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) [Hofmeister et al. 2002] to O(1.46928^n), where O(1.46981^n) can be obtained using the methods of Hofmeister and Rolf.
@InProceedings{hertli_et_al:LIPIcs.STACS.2011.237, author = {Hertli, Timon and Moser, Robin A. and Scheder, Dominik}, title = {{Improving PPSZ for 3-SAT using Critical Variables}}, booktitle = {28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)}, pages = {237--248}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-25-5}, ISSN = {1868-8969}, year = {2011}, volume = {9}, editor = {Schwentick, Thomas and D\"{u}rr, Christoph}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.237}, URN = {urn:nbn:de:0030-drops-30147}, doi = {10.4230/LIPIcs.STACS.2011.237}, annote = {Keywords: SAT, satisfiability, randomized, exponential time, algorithm, 3-SAT, 4-SAT} }
Feedback for Dagstuhl Publishing