2024-03-29T07:32:06Zhttp://digital.csic.es/dspace-oai/requestoai:digital.csic.es:10261/1624472020-12-10T16:53:34Zcom_10261_60com_10261_4col_10261_313
Bonet, María Luisa
Levy, Jordi
Manyà, Felip
2018-03-19T12:28:00Z
2018-03-19T12:28:00Z
2007
Artificial Intelligence 171: 606- 618 (2007)
http://hdl.handle.net/10261/162447
10.1016/j.artint.2007.03.001
http://dx.doi.org/10.13039/501100003339
http://dx.doi.org/10.13039/501100007273
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. © 2007 Elsevier B.V. All rights reserved.
eng
closedAccess
Saturation
Weighted Max-SAT
Max-SAT
Completeness
Resolution
Satisfiability
Resolution for Max-SAT
artículo