Recently, the Maximum Satisfiability (MaxSAT) discovers a rapidly increasing number of practical applications in a wide range of different areas. Unsatisfiability-based MaxSAT algorithms have been put forward aimed at improving the performance of solving MaxSAT problem. In these algorithms, several excellent Boolean Satisfiability (SAT) solvers are employed to iteratively identify unsatisfiable sub-formulas and the additional blocking variables are also applied to relax some of initial clauses or encode Boolean constraints into a CNF formula. Firstly, this paper proposes two novel optimizations to reduce the search space: finding all disjoint unsatisfiable cores with the original clauses removed and no blocking variables added; avoiding generating the largest number of blocking variables' clauses with heuristic strategy. Moreover, in order to reduce the number of satisfying iterations, the partial assignment is introduced into satisfiability-based framework as the tight bound accelerator which could find a smaller number of blocking variables. Experimental results show that the unsatisfiability-based algorithm with these optimizations results in an improved and more effective solver for MaxSAT problem than previous algorithms. In addition,this results in consistent performance gains in most cases and on average 1.5 times speed-up for MaxSAT with state-of-the-art algorithms.
The classical NP-complete problem of Boolean Satisfiability (SAT) [
MaxSAT as a well-known problem in Computer Science, consists of identifying the
largest number of clauses in a CNF formula that can be satisfied. The recent
application of MaxSAT and variants in design debugging and verification of complex designs
[
This paper firstly reviews previous MaxSAT algorithm based on unsatisfiable
subformulas named msu4 [
Firstly a finite set of Boolean variables is assumed X={ x1,x2,x3,. . . ,xn} . A CNF
formula φ is defined on the conjunction of clauses wi and each clause consists of the
disjunction of literals, which is either a variable xi or its complement xi. In the
context of search algorithms of SAT, variables can be assigned a logic value, either 0 or 1.
Alternatively, variables can defined as a function v: X →{ 0,u,1} , where u denotes a
variable whose value is uncertain. When all of variables are assigned a value in { 0,1} ,
then v is referred to as a complete assignment. Otherwise it is a partial assignment [
In this section Maximal Satisfiability and Minimal Unsatisfiability are firstly introduced. Afterwards, the previous MaxSAT algorithm using unsatisfiable cores named msu4 is described.
Our improved algorithm and previous methods are based on maximal satisfiability and minimal unsatisfiability. The MaxSAT problem as an optimization problem corresponds to the minimization of the number of false clauses in a CNF formula, which means that MaxSAT problem discovers an assignment to the variables of a CNF formula that maximizes the number of satisfied clauses.
In order to illustrate this problem, Maximally Satisfiable Subset (MSS) is defined as
a subset of clauses in a CNF formula, which is satisfiable and then adds any of the other
clauses in an original formula to MSS leading new clauses set to unsatisfiable. In this
context, Minimal Unsatisfiable Subset (MUS) is an inconsistent subset of the clauses of
the original formula and dropping one of its clauses will make it satisfiable. MSS and
MUS [
M SS(φ ) = {
m m ∪ { a} is satisf iable, if m⊆φ
is unsatisf iable, ∀a∈(φ -m) M U S(φ ) = {
m is m − { a} unsatisf iable, if m⊆φ is satisf iable, ∀a∈m
Notice that MSS as a satisfied subset of clauses cannot become bigger and MUS as an unsatisfiable subset that removes any of its clauses can render it satisfiable. The relationship between MaxSAT and MSS is subtle. Given an unsatisfiable instance, MaxSAT is the largest subset of clauses that can be satisfiable which means to find MSS with maximal number. However, all MSSes may have different sizes and cannot be all MaxSAT solutions with maximal number. Removing the clauses that are not included in the MSS makes CNF formula satisfiable. Therefore Minimal Correction Set (MCS) is introduced to describe the complement of MSS and the set of MCSes is shown: M CSes(φ ) = { m| m ⊆ φ and (φ − m) ∈ M SSes(φ )}
MCS as the complementary point of MSSes offers the real link to MUSes. Note that any clause of MUS in a CNF formula makes the formula unsatisfiable and the complement formula satisfiable,thus every MSS must contain at least one of clauses of every MUS. This relationship between MCSes and MUSes can usually be described as a solution to a set converting problem. Specifically, each hitting set of the MUSes is an MCS. Given a collection of sets, hitting set intersects all sets in the collection in at least one element and the problem of hitting set is an equivalent reformulation of set covering. A MCS is a hitting set of the MUSes with the additional limit that it cannot become smaller without losing its defining property: it is an irreducible hitting set and each hitting set of MCSes is an MUS. The example formula is shown to explain their relationship between MSSes, MCSes and MUSes.
φ = (x1) ∧ (x1 ∨ x2) ∧ (x2) ∧ (x2)
M SSes(φ ) = { { x1, x1 ∨ x2, x2} , { x1 ∨ x2, x2} , { x1, x2} }
In the example above, every MUS of a CNF formula is an irreducible hitting set of the MCSes of that CNF formula. In the given CNF formula above, the number of maximal satisfiable clauses is 3. More importantly, MSS and MUS also can tell us the relationship between MUS and MaxSAT problem.
Recently, several methods based on unsatisfiable cores are proposed. M su4 which
applies improved blocking variable into clauses is more effective than other algorithms in
the experiment results. More importantly, msu4 avoids interacting with a PBO solver
and instead is a fully SAT-based solver that relies on the most effective techniques,
such as Boolean Constraint Propagation, conflict based learning and conflict-directed
backtracking [
Proposition 1 MaxSAT Upper Bound(UB): In a CNF formula, φ corresponds to the number of clauses. Let K denote disjoint unsatisfiable cores, then φ - K corresponds to an MaxSAT Upper Bound.
Proposition 2 MaxSAT Lower Bound(LB): Let B define as the set of blocking variables assigned value TRUE when clauses become satisfiable, then φ - B denotes a MaxSAT Lower Bound.
In previous subsection, some relationships between MUS and MaxSAT are briefly
introduced and these properties are employed in the algorithm to define MaxSAT Upper
Bound and Lower Bound [
As shown previously, unsatisfiable-based algorithm is able to tackle MaxSAT problem.
However, msu4 works by the redundant lower and upper bounds in some SAT solver
iterations. This section proposes an improved algorithm based on msu4 with two key
optimizations, which are used as the tight bound accelerator. Firstly the thought of
binary search [
In algorithm 1, compared with the upper bound and lower bound in the msu4, two new bounds, which denote the lower and upper bounds of lower bound, are firstly proposed and then used into algorithm 1 and algorithm 2.
Proposition 3 Lower Bound of Lower Bound (L LB): φ corresponds to a CNF formula. Remove any L LB clauses to render new φ ∗ unsatisfiable. In our algorithm 2, L LB is initialized to the number of unsatisfiable cores.
Proposition 4 Upper Bound of Lower Bound (L UB):φ corresponds to a CNF formula. Remove the given L U B clauses to make new φ ∗ satisfiable. In algorithm 2, L U B is firstly assigned to the number of blocking variables.
Proposition 5 [
Compared with msu4, algorithm 1 uses the method of binary search to acquire MaxSAT solution and is also based on Proposition 5 defined in the BIN to guide algorithm 1. The pseudo code for msu5 bin is shown in Algorithm 1.
In msu4, lower bound only depends on the value of blocking variables when φ is satisfiable, and its variation is passive. Considering that msu4 calculates the size of lower bound by inches, this paper presents the binary search, whose algorithm in computer science finds the position of a specified value within a sorted key. Algorithm 1 employs the binary search to take the initiative to alter two bounds in order to accelerate the growth of two bounds for reducing the number of SAT solver iterations, which will solve the MaxSAT problem quickly.
In algorithm 1, there are several differences between msu4 and msu5 bin. L U B is initialized to the number of initial clauses and L LB is to 0. Before each call to the SAT solver, BSB which corresponds to the middle variable, needs to be computed under the method of binary search (line 6). Afterwards CN F (∑i∈VB bi ≤ BSB) is generated and then added to φ w (line 7 and 8). L LB is only updated on iterations when the SAT solver returns false. Considering such an iteration, for which the unsatisfiable core does not include initial clauses (line 17), L LB will be assigned to BSB. When the unsatisfiable core contains original clauses I > 0, this process is the same as msu4 from line 13 to 16. Consider now a satisfiable iteration. It occurs when the number of blocking variables assigned 1 is sufficient to make the current CNF formula get a satisfiable assignment, L U B will be updated(line 21). But it can not guarantee that this number is minimal. When L LB + 1 ≥ L U B, it is an answer of the MaxSAT solution.
Algorithm 1 Improving MaxSAT Algorithm based on binary search 1: ◃ the running condition of algorithm 1 is that φ is unsatisfiable 2: L LB ← 0 3: L U B ← | φ| 4: φw ← φ 5: while TRUE do 6: BSB ← (L LB + L U B)/2 ◃ BSB is the middle variable in the binary search 7: φCH ← CN F (∑i∈VB bi ≤ BSB) 8: (st, φc) ← SAT (φw ∪ φCH ) 9: if st = UNSAT then 10: φI ← φc ∩ φ 11: I ← { i| wi ∈ φI } 12: VB ← VB ∪ I 13: if | I| > 0 then 14: φN ← { wi ∪ { bi}| wi ∈ φI } 15: φa ← CN F (∑ 16: φw ← (φw − φIi)∈∪Ibφi N≥∪1)φa 17: else 18: L LB ← BSB 19: end if 20: else 21: L U B ← BSB 22: end if 23: if L LB + 1 ≥ L U B then 24: return a satisfiable assignment 25: end if 26: end while
Although the performance of msu5 bin is superior to previous methods, three novel improvements are proposed in algorithm 2, which can be more efficient to optimize the MaxSAT algorithm.
Firstly, when the SAT solver returns satisfiable, the upper bound only relies on the
middle variable in algorithm 1, which may not be the minimal number of blocking
variables assigned 1. In detail, after some satisfiable iterations, the assignments of upper
bounds are usually redundant. Our algorithm 2 (named msu6 bd) proposes the
technology of partial assignment, which could effectively reduce the number of satisfying
iterations in algorithm 1. Comparing the number of blocking variables (assigned value
TRUE) in partial assignment with the value of middle variable, the smaller value will
be assigned to the upper bound. Specifically, a partial assignment might not include
some blocking variables called irrelevant variables, which means that SAT solver only
needs to analyze several blocking variables and discard some other blocking variables
if they are not used for satisfying any clause. Our Algorithm is built on the interface of
PicoSAT [
Secondly, when the middle variable in algorithm 1 is assigned to half number of
blocking variables, it could generate the largest number of clauses for pseudo boolean
constraints. Considering that x1 + x2 + . . . + xn ≥ k results in BDDs with (n −
k + 1) × k nodes [
Lastly, when algorithm 1 iteratively obtains an unsatisfiable core each time, the CNF formula will be added more and more clauses generated by blocking variables. For this reason, algorithm 2 starts with finding all disjoint unsatisfiable cores as a prepossessing under the smaller search space with original clauses removed and no blocking variables added. In detail, whenever algorithm 2 finds an unsatisfiable core, some clauses in this core will be temporarily removed. When SAT solver can no longer obtain any unsatisfiable core, the CNF formula will be restored and then the method of binary search continues to solve MaxSAT problem. For this unsatisfiable core-solving preprocessing that requires to iterative calls to a SAT solver, the well-known incremental interface of PicoSAT solver can be considered, which is a SAT solver that after running a CNF formula, keeps all clauses and the internal state that can be reused when inserting additional clauses or deleting information learned from clauses. The pseudo code for msu6 bd is shown in Algorithm 2.
Algorithm 2 begins with finding out all disjoint unsatisfiable cores from line 2 to 11. Afterwards φ w is set as (φ − INC ) ∪ U NC ∪ CSC , which shows that φ removes unsatisfiable cores, and then adds those clauses including blocking variables and pseudo boolean constraints (line 12). L LB will be initialized to the number of unsatisfiable cores and L U B is assigned to the number of blocking variables, aiming at reducing the number of SAT solver iterations and speeding up to enhance the performance of algorithm 1 (line 13). In the process of binary search, the function of HSBS is to prevent the number of blocking clauses becoming large when HSBS is nearly equal to VB/2 (line 15). More importantly, L U B is assigned to the smaller value between VS and BSB (line 31).
This section presents the experimental results of the improved MaxSAT algorithm (msu6 bd).
In order to evaluate this new method, pbo [
In order to evaluate the improved MaxSAT algorithm, a set of instances are selected. These instances are obtained from existing unsatisfiable subsets of crafted and industrial MaxSAT benchmarks, the SAT competition archives and SATLIB. The majority of the considered industrial instances are originally from EDA applications, including model checking, equivalence checking , and test pattern generation. The total number of unsatisfiable instances considered is 447. All experiments are running on a Core 2 Dual 2.13 Ghz workstation with 4 GB of RAM and the CPU timeout of 1000 seconds for each instance.
Table 1 shows the number of solved instances for all selected benchmark sets. The improvements from msu4 and msu5 bin to msu6 bd are very clear. The overall number of solved instances (msu6 bd) is vastly improved as it now solves more instances than msu5 bin, msu4 and pbo. When solving MaxSAT crafted instances, the performances of msu5 bin and msu6 bd are parallel. Nevertheless, msu6 bd is not effective enough to solve all the selected instances. The MaxSAT algorithm based on the unsatisfiable cores needs to use SAT solver to iteratively execute, which is not suitable for the time-out instances.
1000 900 800 700 600 e 500 m i t 400 300 200 100 0 msu6_bd msu5_bin msu4 pbo 0.1 0.01 1X 2X3X
10X 0.01 0.1 1 10 100
1000 msu4 that it is more effective than pbo. Despite the performance advantage of the versions of msu6 bd, there are some exceptions.
This paper proposes an improved unsatisfiable-based MaxSAT algorithm. At first
partial assignment can be employed into binary search-based framework as the tight bound
accelerator: partial assignment could make upper bound select a smaller number of
clauses than previous algorithms. Moreover, HSBS avoids generating the largest
number of clauses for pseudo boolean constraints, which can reduce the search space of
binary search. Finally, another improvement strategy as the preprocessing of binary
search can find as much disjoint unsatisfiable cores as possible to speed up the
execution speed of MaxSAT algorithm. With the original clauses removed and no blocking
clauses added, this optimization can significantly reduce search space in these number
of unsatisfiable iterations. Preliminary experimental results show that these techniques
significantly improve the performance of our unsatisfiability-based algorithm in
solving industrial instances of MaxSAT problem. As a result, our algorithm maintains its
competitive advantage over other algorithms for MaxSAT problem. Despite the
promising results, additional application to msu6 bd is expected, which is to exploit structure
information [
The authors are thankful to the editor and anonymous reviewers for their valuable comments that help us improve the quality of the paper.