文章基本信息

标题：Improving PPSZ for 3-SAT using Critical Variables
本地全文：下载
作者：Timon Hertli ; Robin A. Moser ; Dominik Scheder 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2011
卷号：9
页码：237-248
DOI：10.4230/LIPIcs.STACS.2011.237
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：SAT; satisfiability; randomized; exponential time; algorithm; 3-SAT; 4-SAT