Skip to Main content Skip to Navigation
Journal articles

Optimizing with Minimum Satisfiability

Abstract : MinSAT is the problem of finding a truth assignment that minimizes the number of satisfied clauses in a CNF formula. When we distinguish between hard and soft clauses, and soft clauses have an associated weight, then the problem, called Weighted Partial MinSAT, consists in finding a truth assignment that satisfies all the hard clauses and minimizes the sum of weights of satisfied soft clauses. In this paper we describe a branch-and-bound solver for Weighted Partial MinSAT equipped with original upper bounds that exploit both clique partitioning algorithms and MaxSAT technology. Then, we report on an empirical investigation that shows that solving combinatorial optimization problems by reducing them to MinSAT is a competitive generic problem solving approach when solving MaxClique and combinatorial auction instances. Finally, we investigate an interesting correlation between the minimum number and the maximum number of satisfied clauses on random CNF formulae.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-00790507
Contributor : Laurent Simon Connect in order to contact the contributor
Submitted on : Wednesday, February 20, 2013 - 1:44:42 PM
Last modification on : Sunday, June 26, 2022 - 11:58:19 AM

Links full text

Identifiers

Collections

Citation

Zhu Zhu, Chu Min Li, Felip Manyi, Laurent Simon. Optimizing with Minimum Satisfiability. Artificial Intelligence, Elsevier, 2012, 190, pp.32-44. ⟨10.1016/j.artint.2012.05.004⟩. ⟨hal-00790507⟩

Share

Metrics

Record views

38