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