Analyzing the Instances of the MaxSAT Evaluation
A New Algorithm for Weighted Partial MaxSAT
Publication Type:
Conference PaperSource:
Proceedings of the 24th AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA (2010)Abstract:
We present and implement a Weighted Partial MaxSAT solver based on successive calls to a SAT solver. We prove the correctness of our algorithm and compare our solver with other Weighted Partial MaxSAT solvers.
Exact MinSAT Solving
New Insights into Encodings from MaxCSP into Partial MaxSAT
Resolution-Based Lower Bounds in MaxSAT
Publication Type:
Journal ArticleSource:
Constraints, Volume 15, Issue 4, p.29 (2010)Keywords:
Max-SAT; lower boundAbstract:
The lower bound (LB) implemented in branch and bound MaxSAT solvers is decisive for obtaining a competitive solver. In modern solvers like MaxSatz and MiniMaxSat, the LB relies on the cooperation of the underestimation and inference components. Actually, the underestimation component of some solvers guides the application of the inference component when a conflict is reached and certain structures are found. In this paper we analyze algorithmic and logical aspects of the underestimation components that have been implemented in MaxSatz during its evolution. From an algorithmic point of view, we define novel strategies for selecting unit clauses in UP (the underestimation of LB in UP is the number of independent inconsistent subformulas detected using unit propagation), the extension of UP with failed literal detection, and a clever heuristic for guiding the application of MaxSAT resolution when UP augmented with failed literal detection is applied in the presence of cycles structures. From a logical point of view, we prove that the inconsistent subformulas detected by UP are minimally unsatisfiable, but this property does not hold if failed literal detection is added. In the presence of cycle structures in conflicts detected by UP augmented with failed literal detection, we prove that the application of MaxSAT resolution produces smaller inconsistent subformulas and, besides, generates additional clauses that may be used to improve the LB. The conducted empirical investigation indicates that the LB techniques described in this paper lead to better quality LBs.
Sequential Encodings from Max-CSP into Partial Max-SAT
Exploiting Cycle Structures in Max-SAT
Solving (Weighted) Partial MaxSAT Through Satisfiability Testing
Publication Type:
Conference PaperSource:
Proc. of the 20th Int. Conf. on Theory and Applications of Satisfiability Testing, SAT'09, Springer-Verlag, Volume 5584, p.427-440 (2009)Abstract:
Recently, Fu and Malik described an unweighted Partial MaxSAT solver based on successive calls to a SAT solver. At the kth iteration the SAT solver tries to certify that there exist an assignment that satisfies all but k clauses. Later Marques-Silva and Planes implemented and extended these ideas. In this paper we present and implement two Partial MaxSAT solvers and the weighted variant of one of them. Both are based on Fu and Malik ideas. We prove the correctness of our algorithm and compare our solver with other (Weighted) MaxSAT and (Weighted) Partial MaxSAT solvers.
A Preprocessor for Max-SAT Solvers
Publication Type:
Conference PaperSource:
11th International Conference on Theory and Applications of Satisfiability Testing (SAT-2008), Springer, Volume 4996, Guangzhou, China, p.15-20 (2008)Abstract:
We describe a preprocessor that incorporates a variable saturation
procedure for Max-SAT, and provide empirical evidence that it improves
the performance of some of the most successful state-of-the-art solvers
on several partial (weighted) Max-SAT instances of the 2007 Max-SAT
Evaluation.
Modelling Max-CSP as Partial Max-SAT
Publication Type:
Conference PaperSource:
11th International Conference on Theory and Applications of Satisfiability Testing (SAT-2008), Springer, Volume 4996, Guangzhou, China, p.1-14 (2008)Keywords:
Max-SAT; Max-CSPAbstract:
We define a number of original encodings that map Max-CSP instances
into partial Max-SAT instances. Our encodings rely on the well-known
direct and support encodings from CSP into SAT. Then, we report on an
experimental investigation that was conducted to compare the
performance profile of our encodings on random binary Max-CSP
instances. Moreover, we define a new variant of the support encoding
from CSP into SAT which produces fewer clauses than the standard
support encoding.
