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 [10] to O(1.32153(n)). Using a different approach, Iwama et al. [5] 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)) [6] to O(1.46928(n)), where O(1.46981(n)) can be obtained using the methods of [6] and [10]. |
Year | DOI | Venue |
---|---|---|
2010 | 10.4230/LIPIcs.STACS.2011.237 | Leibniz International Proceedings in Informatics |
Keywords | Field | DocType |
SAT,satisfiability,randomized,exponential time,algorithm,3-SAT,4-SAT | Discrete mathematics,#SAT,Combinatorics,Satisfiability,Critical variable,Mathematics | Journal |
Volume | ISSN | Citations |
9 | 1868-8969 | 8 |
PageRank | References | Authors |
0.63 | 5 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Timon Hertli | 1 | 30 | 2.46 |
Robin A. Moser | 2 | 240 | 12.51 |
Dominik Scheder | 3 | 85 | 13.54 |