An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances

详细信息    查看全文

• 关键词：Satisfiability ; Parameterized complexity ; Resolution size ; Incidence graph ; Pathwidth
• 刊名：Lecture Notes in Computer Science
• 出版年：2017
• 出版时间：2017
• 年：2017
• 卷：10167
• 期：1
• 页码：359-369
• 丛书名：WALCOM: Algorithms and Computation
• ISBN：978-3-319-53925-6
• 卷排序：10167

文摘

We show the first upper bound for resolution size of a SAT instance by pathwidth of its incidence graph. Namely, we prove that if an incidence graph of an unsatisfiable CNF formula has pathwidth \({\mathrm {pw}}\), the formula can be refuted by a resolution proof with at most \(O^*(3^{\mathrm {pw}})\) clauses. It is known that modern practical SAT-solvers run efficiently for instances which have small and narrow resolution refutations. Resolution size is one of the parameters which make SAT tractable, whereas it is shown that even linearly approximating the resolution size is NP-hard. In contrast, computing graph based parameters such as treewidth or pathwidth is fixed-parameter tractable, and also efficient FPT algorithms for SAT of bounded such parameters are widely researched. However, few explicit connection between these parameters and resolutions or SAT-solvers are known. In this paper, we provide an FPT algorithm for SAT on path decomposition of its incidence graph. The algorithm can construct resolution refutations for unsatisfiable formulas, and analyzing the size of constructed proof gives the new bound.