Resolution and linear CNF formulas: Improved (n, 3)-MAxSAT algorithms Academic Article

abstract

• 2016 Elsevier B.V. We study techniques for solving the MAXSAT problem on instances in which the variable degree is bounded by 3. The problem is NP-hard. We show how resolution principle can be applied that converts an instance into an equivalent instance in which the CNF formula becomes a linear CNF formula. We then show how more efficient branching strategies can be applied on linear CNF formulas. As applications, we present two algorithms: one of running time O(1.194k) that solves the parameterized version of the problem, and the other of running time O(1.237n) that solves the optimization version of the problem, both significantly improving previous best upper bounds.

authors

• Chen, Jianer

published proceedings

• THEORETICAL COMPUTER SCIENCE

author list (cited authors)

• Xu, C., Chen, J., & Wang, J.

citation count

• 6

complete list of authors

• Xu, Chao||Chen, Jianer||Wang, Jianxin

publication date

• June 2019

publisher

• Elsevier  Publisher

published in

• Theoretical Computer Science  Journal

keywords

• Exact Algorithm
• Linear Cnf Formula
• Maximum Satisfiability
• Parameterized Algorithm
• Resolution Principle

Digital Object Identifier (DOI)

• 10.1016/j.tcs.2016.08.008

start page

• 113

end page

• 123

volume

• 774

URL

• http%3A%2F%2Fdx.doi.org%2F10.1016%2Fj.tcs.2016.08.008