Implementing the Linear MaxSAT solver¶
This tutorial shows how to implement the Linear1 algorithm for MaxSAT using Paramita’s building blocks. We will write a class that inherits from NonIncrMaxSatSolver, using an incremental SAT solver and an incremental PB encoder to enforce constraints over the soft clauses.
The Linear MaxSAT algorithm¶
This is the pseudocode for the Linear MaxSAT algorithm:
The algorithm receives as input a weighted CNF formula \(\varphi\), consisting on a set of \(m\) soft clauses, \(\{C_1,w_1),...,(C_m,w_m)\}\), and a set of \(m'\) hard clauses, \(\{(C_{m+1},\infty),...,(C_{m+m'}, \infty)\}\).
Then, we build a CNF formula by considering all the hard clauses, and by adding \(C_i \lor b_i\) for each soft clause, where \(b_i\) is a new fresh variable. This way, whenever \(b_i\) is assigned to true, the soft clause \(C_i\) can be falsified.
We also compute the initial upper bound \(ub\) as the sum of all the weights of the soft clauses.
In the main loop, we build a new formula \(\varphi_{ub}\) by adding to \(\varphi'\) the CNF encoding of the Pseudo-Boolean constraint \(\sum w_i \cdot b_i \leq ub - 1\). With this step, we are enforcing that the number of variables \(b_i\) that can be set to true must be less than or equals to the \(ub\) minus one.
We check the \(\varphi_{ub}\) formula with a SAT solver, which returns the status \(st\) (sat or unsat) and a model \(\mathcal{I}\) (only if \(st = sat\)). If the \(\varphi_{ub}\) formula is satisfiable, we compute the new upper bound \(ub\) (which must be less than or equals to \(ub -1\), therefore better than the one that we had) by checking the unsatisfied soft clauses in the original formula \(\varphi\). Otherwise, if the \(\varphi_{ub}\) formula is unsatisfiable, we know it is not possible to satisfy more clauses such that the upper bound is \(ub -1\). Therefore, the optimal upper bound must be \(ub\), so we just return \(ub\) and exit the procedure.
Implementing the solver¶
Although the pseudocode for the Linear MaxSAT algorithm is rather simple, there are some key implementation details that we must handle to improve the algorithm's performance. In particular, we will use an incremental SAT solver to build and solve the formulas incrementally, as well as an incremental Pseudo-Boolean encoder to efficiently build the iterative \(\sum w_i \cdot b_i \leq ub - 1\) transformations to CNF.
First of all, we will create a subclass of NonIncrMaxSatSolver. In this case, this class will receive as parameters an instance of SatSolver and an instance of PbToCnfEncoder.
Additionally, we will record the soft clauses, its related weights, the original maximum variable (which we will use later to output the model correctly), as well as the best upper bound and models found:
class LinearMaxSat(NonIncrMaxSatSolver):
def __init__(self, sat_solver: SatSolver, pb_encoder: PbToCnfEncoder):
super().__init__()
self.sat_solver = sat_solver
self.pb_encoder = pb_encoder
self._soft_clauses = []
self._weights = []
self._original_max_var = None
self.ub_ = None
self.best_model_ = None
The add_clause method distinguishes hard and soft clauses. Hard clauses (weight TOP_WEIGHT) go directly into the SAT solver. Soft clauses are stored for later processing. We also update the maximum variable index so that the SAT solver knows about the variables used.
def max_var(self):
return self.sat_solver.max_var()
def set_minimum_var(self, var):
self.sat_solver.set_minimum_var(var)
def add_clause(self, clause, weight):
if weight == SPECIAL_WEIGHTS.TOP_WEIGHT:
self.sat_solver.add_clause(clause)
else:
self._soft_clauses.append(clause)
self._weights.append(weight)
mv = max(map(abs, clause))
self.set_minimum_var(mv)
In the solve method (which in this implementation ignores the assumptions and the budget), we first check if the formula consisting only in the hard clauses is unsatisfiable.
If this is not the case, we record the original max var and reify the soft clauses by adding the blocking variables \(b_i\):
def solve(self, assumptions=[], budget=SolvingBudget()):
# NOTE: At the moment we ignore assumptions and budget
# Check if hard constraints are unsatisfiable
is_sat = self.sat_solver.solve()
if is_sat is False:
return MAXSAT_ANSWER.UNSATISFIABLE
self._original_max_var = self.sat_solver.max_var()
# Reify soft clauses
next_aux = self.max_var() + 1
soft_lits = []
for c in self._soft_clauses:
self.sat_solver.add_clause(c + [next_aux])
soft_lits.append(next_aux)
next_aux += 1
Next, we prepare the first Pseudo-Boolean constraint that we will encode to CNF \((\sum w_i \cdot b_i \leq \sum w_i)\), and encode it to the SAT solver using the specified PB encoder.
We store the returned context ctx, as this is what the encoder will use to incrementally encode the subsequent constraints, which is more efficient than encoding the new constraints from scractch.
# Prepare PB constraint
pb = PbConstraint(
lits=soft_lits,
weights=self._weights,
op=PbConstraint.LTE,
bound=sum(self._weights),
)
# Encode the constraint to the SAT solver
ctx = self.pb_encoder.encode(pb, container=self.sat_solver)
The main loop is essentially the same that we discussed in the pseudocode, with the detail that we are building the formula \(\varphi_{ub}\) incrementally in the SAT solver, as well as the CNF encoding of the \(\sum w_i \cdot b_i \leq ub - 1\) constraint.
while True:
is_sat = self.sat_solver.solve()
if is_sat:
model = self.sat_solver.model()
# Update the upper bound cost
self.ub_ = sum(
w
for c, w in zip(self._soft_clauses, self._weights)
if not self._is_satisfied(c, model)
)
print(f"o {self.ub_}")
self.best_model_ = model
pb.bound = self.ub_ - 1 # Update the PB bound
ctx = self.pb_encoder.encode(pb, container=self.sat_solver, context=ctx)
elif is_sat is None:
if self.ub_ is None:
print("s UNKNOWN")
return MAXSAT_ANSWER.UNKNOWN
print("s SATISFIABLE")
return MAXSAT_ANSWER.SATISFIABLE
else:
print("s OPTIMUM FOUND")
return MAXSAT_ANSWER.OPTIMAL
We use the _is_satisfied auxiliary function to check if a soft clause is satisfied by the returned model:
def _is_satisfied(self, clause, model):
for lit in clause:
if model[abs(lit) - 1] == lit:
return True
return False
Finally, we provide methods to retrieve the model and the objective value. The objective value returned by val_objective is the sum of the weights of the satisfied soft clauses (i.e., total soft weight minus the accumulated cost).
def model(self):
if self.best_model_:
return self.best_model_[: self._original_max_var]
raise NotImplementedError("no model available")
def val_objective(self):
return sum(self._weights) - self.ub_
Using the solver¶
Prerequisites
You need a SAT solver compiled as a Paramita extension (e.g. CaDiCaL 3.0.0):
And an incremental PB to CNF encoder:
This MaxSAT solver can be used as any other MaxSAT solver implementing the NonIncrMaxSatSolver Paramita interface.
For example, in the following code we use the LinearMaxSat solver to load a WCNF formula using Paramita's load_wcnf function:
if __name__ == "__main__":
import argparse
from paramita.io import load_wcnf
parser = argparse.ArgumentParser()
parser.add_argument("wcnf_file", type=str)
parser.add_argument("--sat-name", "-sat", type=str, default="Cadical300")
parser.add_argument("--pb-name", "-pb", type=str, default="IncrSwcEncoder")
args = parser.parse_args()
sat_solver = SatSolver.from_name(args.sat_name)
pb_encoder = PbToCnfEncoder.from_name(args.pb_name)
msat = LinearMaxSat(sat_solver, pb_encoder)
load_wcnf(args.wcnf_file, msat)
result = msat.solve()
print(result)
Source code¶
This is the complete source code for the Linear MaxSAT tutorial:
from paramita.solvers import (
NonIncrMaxSatSolver,
MAXSAT_ANSWER,
SatSolver,
SolvingBudget,
)
from paramita.containers import SPECIAL_WEIGHTS
from paramita.encoders import PbToCnfEncoder
from paramita import PbConstraint
class LinearMaxSat(NonIncrMaxSatSolver):
def __init__(self, sat_solver: SatSolver, pb_encoder: PbToCnfEncoder):
super().__init__()
self.sat_solver = sat_solver
self.pb_encoder = pb_encoder
self._soft_clauses = []
self._weights = []
self._original_max_var = None
self.ub_ = None
self.best_model_ = None
def max_var(self):
return self.sat_solver.max_var()
def set_minimum_var(self, var):
self.sat_solver.set_minimum_var(var)
def add_clause(self, clause, weight):
if weight == SPECIAL_WEIGHTS.TOP_WEIGHT:
self.sat_solver.add_clause(clause)
else:
self._soft_clauses.append(clause)
self._weights.append(weight)
mv = max(map(abs, clause))
self.set_minimum_var(mv)
def solve(self, assumptions=[], budget=SolvingBudget()):
# NOTE: At the moment we ignore assumptions and budget
# Check if hard constraints are unsatisfiable
is_sat = self.sat_solver.solve()
if is_sat is False:
return MAXSAT_ANSWER.UNSATISFIABLE
self._original_max_var = self.sat_solver.max_var()
# Reify soft clauses
next_aux = self.max_var() + 1
soft_lits = []
for c in self._soft_clauses:
self.sat_solver.add_clause(c + [next_aux])
soft_lits.append(next_aux)
next_aux += 1
# Prepare PB constraint
pb = PbConstraint(
lits=soft_lits,
weights=self._weights,
op=PbConstraint.LTE,
bound=sum(self._weights),
)
# Encode the constraint to the SAT solver
ctx = self.pb_encoder.encode(pb, container=self.sat_solver)
while True:
is_sat = self.sat_solver.solve()
if is_sat:
model = self.sat_solver.model()
# Update the upper bound cost
self.ub_ = sum(
w
for c, w in zip(self._soft_clauses, self._weights)
if not self._is_satisfied(c, model)
)
print(f"o {self.ub_}")
self.best_model_ = model
pb.bound = self.ub_ - 1 # Update the PB bound
ctx = self.pb_encoder.encode(pb, container=self.sat_solver, context=ctx)
elif is_sat is None:
if self.ub_ is None:
print("s UNKNOWN")
return MAXSAT_ANSWER.UNKNOWN
print("s SATISFIABLE")
return MAXSAT_ANSWER.SATISFIABLE
else:
print("s OPTIMUM FOUND")
return MAXSAT_ANSWER.OPTIMAL
def model(self):
if self.best_model_:
return self.best_model_[: self._original_max_var]
raise NotImplementedError("no model available")
def val_objective(self):
return sum(self._weights) - self.ub_
def _is_satisfied(self, clause, model):
for lit in clause:
if model[abs(lit) - 1] == lit:
return True
return False
if __name__ == "__main__":
import argparse
from paramita.io import load_wcnf
parser = argparse.ArgumentParser()
parser.add_argument("wcnf_file", type=str)
parser.add_argument("--sat-name", "-sat", type=str, default="Cadical300")
parser.add_argument("--pb-name", "-pb", type=str, default="IncrSwcEncoder")
args = parser.parse_args()
sat_solver = SatSolver.from_name(args.sat_name)
pb_encoder = PbToCnfEncoder.from_name(args.pb_name)
msat = LinearMaxSat(sat_solver, pb_encoder)
load_wcnf(args.wcnf_file, msat)
result = msat.solve()
print(result)
-
Daniel Le Berre and Stéphanie Roussel. Sat4j 2.3.2: on the fly solver configuration system description. J. Satisf. Boolean Model. Comput., 8(3/4):197–202, 2014. URL: https://doi.org/10.3233/sat190098, doi:10.3233/SAT190098. ↩