Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > DETAIL:

Revision(s):

Revision #1 to TR16-034 | 10th March 2016 16:31

On the Computational Complexity of MaxSAT

Revision #1
Authors: Mohamed El Halaby
Accepted on: 10th March 2016 16:31
Keywords:

Abstract:

Given a Boolean formula in Conjunctive Normal Form (CNF) $\phi=S \cup H$, the MaxSAT (Maximum Satisfiability) problem asks for an assignment that satisfies the maximum number of clauses in $\phi$. Due to the good performance of current MaxSAT solvers, many real-life optimization problems such as scheduling can be solved efficiently by encoding them into MaxSAT. In this survey, we discuss the computational complexity of MaxSAT in detail in addition to major results on the classical and parameterized complexities of the problem.

Paper:

TR16-034 | 7th March 2016 01:33

On the Computational Complexity of MaxSAT

TR16-034
Authors: Mohamed El Halaby
Publication: 10th March 2016 16:17
Keywords:

Abstract:

Given a Boolean formula in Conjunctive Normal Form (CNF) $\phi=S \cup H$, the MaxSAT (Maximum Satisfiability) problem asks for an assignment that satisfies the maximum number of clauses in $\phi$. Due to the good performance of current MaxSAT solvers, many real-life optimization problems such as scheduling can be solved efficiently by encoding them into MaxSAT. In this survey, we discuss the computational complexity of MaxSAT in detail in addition to major results on the classical and parameterized complexities of the problem.

ISSN 1433-8092 | Imprint