Impact of SAT-Based Preprocessing on Core-Guided MaxSAT Solving

Abstract

We present a formal analysis of the impact of Boolean satisfiability (SAT) based preprocessing techniques on core-guided solvers for the constraint optimization paradigm of maximum satisfiability (MaxSAT). We analyze the behavior of two solver abstractions of the core-guided approaches. We show that SAT-based preprocessing has no effect on the best-case number of iterations required by the solvers. This implies that, with respect to best-case performance, the potential benefits of applying SAT-based preprocessing in conjunction with core-guided MaxSAT solvers are in principle solely a result of speeding up the individual SAT solver calls made during MaxSAT search. We also show that, in contrast to best-case performance, SAT-based preprocessing can improve the worst-case performance of core-guided approaches to MaxSAT.

Work supported by Academy of Finland, grants 251170 COIN, 276412, 284591; and DoCS Doctoral School in Computer Science at the University of Helsinki.

Appendices

Appendix

A Proof of Proposition 1

(1) If an optimal solution $\tau$ to F assigns $\tau (C) = 0$, then an optimal solution $\tau ^P$ to $F_P$ has to assign $F_P(l_C) = 1$. Similarly, if $\tau (C) = 1$, then $\tau ^P$ can assign $\tau ^P(l_C) = 0$.

(2) We sketch the conversion of an $\mathcal {A}$ core trace $T_P = (\kappa _P^1, \ldots , \kappa _P^{n})$ on $F_P$ into a core trace $T= (\kappa ^1, \ldots , \kappa ^{n})$ on F, the other direction is similar. For $\mathcal {A}=\text {HS}$, every $\kappa _P^i$ is a core of $F_P$. The corresponding core trace of F is obtained by exchanging each $\kappa _P^i = \{ (\lnot l_{C_i}) \mid i=1,\ldots ,n\}$ with $\kappa ^i = \{ C_i \mid i=1,\ldots ,n \}$. Now $\kappa _P^i$ is a core of $F_P$ iff $\kappa ^i$ is a core of F. To see this, note that if $\kappa ^i$ is not a core of F, then it can be satisfied by some assignment $\tau$. The same $\tau$ extended by setting all $l_{C_i}$ variables to 0 to satisfies both $\kappa _P^i$ and the hard clauses $\{ C_1 \vee l_{C_1}, \ldots , C_n \vee l_{C_n} \}$. Hence $\kappa _P^i$ is not a core of $F_P$ either. A similar argument shows the other direction. Finally the termination of HS after n iterations follows by a similar argument showing that $F \setminus hs$ is satisfiable for some $hs = \{C_1, \ldots , C_i\}$ iff $F^P \setminus hs^P$ is satisfiable for $hs^P = \{ (\lnot l_{C_1}), \ldots , (\lnot l_{C_i}) \}$. Hence the trace $T = (\kappa ^1, \ldots , \kappa ^{n})$ is a HS trace on F of the same length as $T_P$.

For $\mathcal {A}=\text {CG}$ the argument is similar but inductive. To form a CG trace T on F, every occurrence of a $(\lnot l_{C_i})$ in a clause $C^i \in \kappa _P^i$ is replaced by $C_i$ to form a core $\kappa ^i$ of $F^i$. For $i > 0$, each such $C^i$ may have been augmented with blocking variables, i.e., $C^i = (\lnot l_{C_i} \vee \bigvee b)$ for some set of blocking variables. However, the substitution $(\lnot l_{C_i} \vee \bigvee b) \rightarrow C_i \vee \bigvee b$ is still valid as, by induction, if CG adds $\bigvee b$ to $(\lnot l_{C_i})$ on the execution corresponding to $T_P$, then it also adds $\bigvee b$ to $C_i$ on the execution corresponding to T.    $\square$