MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [2]

Now we start for minimal unsatisfiable subformulas (MUSes) which I categorize unsatisfiability driven as given in the first post. They are sometimes called as minimal unsatisfiable cores in the literature. I believe the research on computing MUSes made the relation between explanations and relaxations (relaxations in short) in CSP research more prominent. I can not say that one triggered/inspired the other as I do not have enough chronological information...

Explanations and Relaxations in CSP
Relaxations[1] are used to explain the reasons (culprits) of inconsistencies and to (optimally) resolve those inconsistencies in over-constrained CSP problems. Given a CSP problem with a set of user constraints C and background constraints B (hard constraints),  explanations and relaxations are sets of constraints CE ⊆ ℘C and CR ⊆ ℘C respectively. An explanation R ∈ CE is (subset) minimal if the following conditions hold:

• R = {ci, ... , cn} is unsatisfiable 
• Removal of a constraint c from R is satisfiable, i.e. R \ {c} is consistent.

Notice that a subset minimal explanation is not cardinality minimal explanation. A cardinality minimal explanation is a subset minimal explanation that the minimum number of constraints. A relaxation R ∈ CR is a maximal relaxation if the following conditions hold:

• R = {ci,...,cn} is satisfiable 
• Addition of a constraint c to R makes the formula unsatisfiable, i.e. let c ∉ R, the formula R ∪ c is inconsistent.

In very short terms, the relation between explanations and relaxations is the following: the complement of each hitting set of all minimal relaxations is one maximal relaxation. A constructive way of computing explanations is to check the consistency of B ∪ C and iteratively remove one constraint until an unconsistency is obtained. Thus relaxations are computed first. More details are available at [1].

We stop here with CSP explanations and relaxations and start with SAT MUSes in the next post...


References:
[1] Ulrich Junker, "QUICKXPLAIN: Preferred Explanations and Relaxations for Over-Constrained Problems", Proceedings of the Nineteenth National Conference on Artificial Intelligence (AAAI), 2004

MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [1]

I have been recently reading a lot about computation of some satisfiable/unsatisfiable subformulas from a given CNF SAT formula. There are many different problem definitions that represent these computations (respective subformulas). I will try to summarize all of them to the extent of my knowledge while trying to give some usecases and respective references. I am going to start first with satisfiability driven subformula computations. The available solvers may be considered as satisfiability-based, unsatisfiability-based or some other techniques [1,3]...

The general name of computing maximum number of satisfiable clauses from a given formula F is MaxSAT. In MaxSAT, we try to find a subset of clauses C  ⊆ F such that the followings hold:

• C is satisfiable
• There is no other satisfiable subset C' ⊆ F such that |C'| > |C|.

Notice that if F is satisfiable then C = F. Depending on the problem that F encodes, several MaxSAT variants have been proposed. I will discuss two of them: Partial MaxSAT and Weighted MaxSAT. In partial MaxSAT we have soft clauses (relaxable) and hard clauses (non-relaxable). A PMaxSAT solver tries to find the maximum number of satisfiable soft clauses while making sure hard clauses are satisfiable. According to MaxSAT'13 competition a PMaxSAT CNF is specified as : "p wcnf nbvar nbclauses top"[2] where nbvar is the variable number, nbclauses is the number of clauses and top is the weight of hard clauses. Soft clauses have the weight of 1. Example:
p wcnf 3 3 8
1 -1 2
1 -1 3
8 1 2 3

Weighted MaxSAT associates each clause with a weight that is greater than or equal to 1. A WMaxSAT solver tries to find a subformula that has the maximum sum of weights of clauses that are satisfiable (Note here: I think Wiki definition is a bit misleading here...). With weighted MaxSAT one can introduce an ordering between clauses (and thus the high level problem components). There is also a variant in which there are hard clauses. This is a slightly different version of partial MaxSAT with soft clauses having variable weights.

MaxSAT is an active area of research so different variants are proposed every now and then. Many efficient techniques have been/are proposed already...

Stay tuned...
 

References :
[1] http://en.wikipedia.org/wiki/Maximum_satisfiability_problem
[2] http://maxsat.ia.udl.cat/requirements/
[3] T. Alsinet, F. Manya, J. Planes, "Improved Exact Solvers for Weighted Max-SAT",  In Proceedings of Eighth International Conference on Theory and Applications of Satisfiability Testing 2005. NOTE for this paper : For instance, a MaxSAT solver may try to find a truth assignment that minimizes the sum of weights of unsatis ed clauses