Skip to content

Using a MaxSAT solver

This guide shows how to load an external MaxSAT solver plugin, add hard and soft clauses, run the solver, and read the optimal solution and its cost.

Paramita provides a uniform interface to MaxSAT solvers compiled as shared libraries. You need a plugin file (you can obtain one from the Paramita Plugins repository). Once you have it, you can load it in Python.

Prerequisites

You need a MaxSAT solver compiled as a Paramita extension. Start by fetching EvalMaxSAT2022 from the Paramita Plugins repository using the CLI helper:

paramita plugins build cmake "#maxsat-solvers/mse22-EvalMaxSAT2022"

Start by loading the MaxSAT solver by name: 

from paramita.solvers import MaxSatSolver
s = MaxSatSolver.from_name("EvalMaxSAT2022")

Now add clauses. The solver distinguishes hard clauses (must be satisfied) and soft clauses (can be violated, but incur a cost). Hard clauses use a special weight. You can either specify it explicitly or omit the weight:

from paramita.containers import SPECIAL_WEIGHTS

# Hard clause
s.add_clause([1, 2], weight=SPECIAL_WEIGHTS.TOP_WEIGHT)

# Hard clause
s.add_clause([-1, 3])

Soft clauses are added with a positive integer weight. The goal is to satisfy all hard clauses while minimizing the total weight of unsatisfied soft clauses. 

s.add_clause([2], weight=5)
s.add_clause([-3, 1], weight=3)

To solve the problem, call solve: 

result = s.solve()

The return value is an integer constant. To interpret it, import the MAXSAT_ANSWER enum:

from paramita.solvers import MAXSAT_ANSWER

if result == MAXSAT_ANSWER.OPTIMAL:
    print("Optimal solution found")
elif result == MAXSAT_ANSWER.SATISFIABLE:
    print("Feasible (but possibly suboptimal) solution found")
elif result == MAXSAT_ANSWER.UNSATISFIABLE:
    print("Hard clauses are unsatisfiable")
else:  # MAXSAT_ANSWER.UNKNOWN
    print("Solver could not decide")

If a solution exists (OPTIMAL or SATISFIABLE), retrieve the assignment with model. The method returns a list where every variable appears exactly once: positive if true, negative if false.

if result in (MAXSAT_ANSWER.OPTIMAL, MAXSAT_ANSWER.SATISFIABLE):
    assignment = s.model()
    print(assignment)   # e.g., [1, -2, 3] means x1=true, x2=false, x3=true

To get the total weight of satisfied soft clauses (not the cost), use val_objective. The cost (sum of weights of unsatisfied soft clauses) is the total soft weight minus the satisfied weight.

MaxSatSolver is incremental. If you don't need incrementality, you can use the class NonIncrMaxSatSolver.

Next steps

Now you have seen how to start manipulating raw CNF and WCNF formulas.

You can follow up by learning how to model optimization problems.