Resolution for Max-SAT

详细信息    查看全文

• 作者：Marí ; a Luisa Bonet ; Jordi Levy ; Felip Manyà
• 关键词：Satisfiability ; Resolution ; Completeness ; Saturation ; Max-SAT ; Weighted Max-SAT
• 刊名：Artificial Intelligence
• 出版年：2007
• 出版时间：June 2007
• 年：2007
• 卷：171
• 期：8-9
• 页码：606-618
• 全文大小：179 K

文摘

Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses in a CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound.

We also define a weighted Max-SAT resolution-like rule, and show how to adapt the soundness and completeness proofs of the Max-SAT rule to the weighted Max-SAT rule.

Finally, we give several particular Max-SAT problems that require an exponential number of steps of our Max-SAT rule to obtain the minimal number of unsatisfied clauses of the combinatorial principle. These results are based on the corresponding resolution lower bounds for those particular problems.