文章基本信息

标题：PPSZ for General k-SAT - Making Hertli's Analysis Simpler and 3-SAT Faster
本地全文：下载
作者：Dominik Scheder ; John P. Steinberger
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：79
页码：9:1-9:15
DOI：10.4230/LIPIcs.CCC.2017.9
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：The currently fastest known algorithm for k-SAT is PPSZ named after its inventors Paturi, Pudlak, Saks, and Zane. Analyzing its running time is much easier for input formulas with a unique satisfying assignment. In this paper, we achieve three goals. First, we simplify Hertli's analysis for input formulas with multiple satisfying assignments. Second, we show a "translation result": if you improve PPSZ for k-CNF formulas with a unique satisfying assignment, you will immediately get a (weaker) improvement for general k-CNF formulas. Combining this with a result by Hertli from 2014, in which he gives an algorithm for Unique-3-SAT slightly beating PPSZ, we obtain an algorithm beating PPSZ for general 3-SAT, thus obtaining the so far best known worst-case bounds for 3-SAT.
关键词：Boolean satisfiability; exponential algorithms; randomized algorithms