Implementing a MaxSAT solver¶

MaxSAT solvers generalize SAT by associating weights to clauses and optimizing (minimizing) over unsatisfied soft clauses.

In Paramita, MaxSAT solver extensions are represented by the Paramita::NonincrMaxSatSolver and Paramita::MaxSatSolver:

Class Paramita::NonIncrMaxSatSolver¶

A MaxSAT solver.

Note:

Use NON_INCR_MAXSAT_SOLVER_C_INTERFACE to register any subclass of this interface.

#include <NonIncrMaxSatSolver.hpp>

Inherits the following classes: Paramita::WClauseContainer

Class Paramita::MaxSatSolver¶

An incremental MaxSAT solver.

Note:

Use MAXSAT_SOLVER_C_INTERFACE to register any subclass of this interface.

#include <MaxSatSolver.hpp>

Inherits the following classes: Paramita::NonIncrMaxSatSolver

This guide describes the required steps to implement a MaxSAT solver extension.

Implement the weighted clause container interface¶

Like a SAT solver is a clause container, a MaxSAT solver is a weighted clause container.

Please refer to the guide on how to implement the container interface. At least you need to implement:

function add_clause¶

Add a single clause with the specified weight.

virtual Paramita::WClauseContainer::add_clause (
    const Clause & clause,
    Weight weight
) = 0

Parameters:

clause The clause to be added to the container.
weight The associated weight for this clause.

function max_var¶

Get the largest variable used in the container.

virtual std::uint64_t Paramita::WClauseContainer::max_var () const = 0

Postcondition:

The return value is equal or larger to the absolute value for any literal passed to add_clause, add_clauses, or add_lit.

Returns:

The (positive) integer assigned to the largest variable.

function set_minimum_var¶

Sets the maximum variable known to the container to at least this one.

virtual Paramita::WClauseContainer::set_minimum_var (
    std::uint64_t var
) = 0

This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the WClauseContainer::max_var method to determine the next free variable, this method ensures that existing variables cannot be reused.

Postcondition:

The value returned by max_var must be larger or equal than the one provided.

Postcondition:

The value returned by max_var cannot be reduced by this call.

Parameters:

var The variable to be registered to the container.

Implementing the solving and optimization procedure¶

The core responsibility of a MaxSAT solver is to determine whether the hard clauses are satisfiable (feasibility) and, if so, to minimize the cost of unsatisfied soft clauses (optimality). This is exposed through the solve method:

function solve¶

Solve the formula under given assumptions.

virtual MAXSAT_ANSWER Paramita::NonIncrMaxSatSolver::solve (
    const std::vector< Literal > & assumptions,
    const SolvingBudget & budget
) = 0

The feasible solutions of the formula are assignments that satisfy all the hard clauses in the formula.

The cost of a solution is the sum of the weights of the soft clauses not satisfied by the solution.

An optimal solution is a feasible solution with minimal cost.

If interrupted, the solver is responsible from clearing the interruption.

See also: interrupt

Precondition:

solve method has not been called, or no clause has been added since the last solve call.

Postcondition:

The internal solving budget is reset to unlimited.

Parameters:

assumptions The literals manually assigned to true.
budget Budget restrictions for the solve process.

Returns:

MAXSAT_ANSWER::UNKNOWN if no feasible solution is found and the satisfiability of hard clauses has not been determined, MAXSAT_ANSWER::SATISFIABLE if a feasible solution is found but has not been proved to be optimal, MAXSAT_ANSWER::UNSATISFIABLE if the hard clauses are proven to be unsatisfiable, and MAXSAT_ANSWER::OPTIMAL if the feasible solution is proven to be optimal (each of those cases considering the given assumptions).

Calling solve triggers the internal optimization algorithm and may result in:

a feasible solution (hard clauses satisfiable),
proof that the hard clauses are unsatisfiable, or
termination without a definitive answer (e.g. due to interruption or limits).

Different MaxSAT solvers have different capabilities in terms of the queries they are able to answer in a formula. Some solvers focus on finding feasible solutions without being able to prove unsatisfiability, some other solvers find sub-optimal solutions, and some other solvers are entirely unable to prove optimality.

This is implementation defined, but the solve method MUST ensure that the return value represents the ability of the solver (e.g. not returning MAXSAT_ANSWER::OPTIMAL if the solver cannot prove it).

Note

Assumptions and budgets are similar to the ones defined for SAT solvers.

Objective values and models¶

Once a feasible solution is available (either solve returned OPTIMAL or SATISFIABLE), users can query for:

the value of the objective function (total weight of satisfied soft clauses)
a model corresponding to the best solution found so far

The value of the objective function is exposed through:

function val_objective¶

The sum of weights for satisfied soft clauses from the last feasible solution.

virtual std::uint64_t Paramita::NonIncrMaxSatSolver::val_objective () const = 0

The objective value of a solution corresponds to the sum of all the weights for the soft clauses minus the cost of the clauses.

Precondition:

Method solve was called.

Precondition:

Method solve returned MAXSAT_ANSWER::SATISFIABLE or MAXSAT_ANSWER::OPTIMAL.

Warning:

Undefined behaviour if solve returned MAXSAT_ANSWER::UNKNOWN.

Returns:

The sum of the weights of the satisfied soft clauses.

Exception:

NotSolvedException if solve was not called before.
UnsatisfiableException if solve returned MAXSAT_ANSWER::UNSATISFIABLE.

And the model through:

function model¶

Get the model (solution) after solving.

virtual std::vector< Literal > Paramita::NonIncrMaxSatSolver::model () const = 0

The model in a MaxSAT solver will correspond to the best solution found during solving (not only from the last call).

Precondition:

Method solve was called.

Precondition:

Method solve returned MAXSAT_ANSWER::SATISFIABLE or MAXSAT_ANSWER::OPTIMAL.

Warning:

Undefined behaviour if solve returned MAXSAT_ANSWER::UNKNOWN.

Returns:

A vector with the literals that were set to true by the last solve call.

Exception:

NotSolvedException if solve was not called before.
UnsatisfiableException if solve returned MAXSAT_ANSWER::UNSATISFIABLE.

Models are represented as explained in the SAT solvers guide.

Warning

Solvers are responsible for ensuring that the returned model and objective value are consistent with the best solution found so far.

Registering the solver as an extension¶

Assume you have implemented a MaxSAT solver with the following class:

// in maxsatsolver.hpp
class MyMaxSatSolver : public MaxSatSolver {
    // ...
};

// in maxsatsolver.cpp
MyMaxSatSolver::MyMaxSatSolver() { /* ... */ };
// other methods...

To expose this solver as a loadable Paramita extension, use the macro MAXSATSOLVER_C_INTERFACE in your maxsatsolver.cpp file:

// in maxsatsolver.cpp
MyMaxSatSolver::MyMaxSatSolver() { /* ... */ };
// other methods...
MAXSAT_SOLVER_C_INTERFACE(MyMaxSatSolver)

Note

This macro is defined in the header paramita/maxsat/MaxSatSolver.hpp.

When the project is compiled, the resulting shared object will be ready to be loaded by Paramita.

Testing the MaxSAT solver¶

To ensure that the solver implementation behaves as expected, Paramita provides tests based on the doctest framework.

To enable these tests, create a test_solver.cpp file and expand the templated tests for your solver:

#define DOCTEST_CONFIG_IMPLEMENT_WITH_MAIN
#include <doctest/doctest.h>

#include "maxsatsolver.hpp"
#include <paramita/tests/maxsat/TestMaxSatSolver.hpp>

GENERATE_DOCTESTS_FOR_MAXSAT_SOLVER(MyMaxSatSolver)

If using CMake, you can automatically register the tests with CTest using the ParamitaInterfaces_discover_tests function on the target that builds an executable from test_solver.cpp.

Optional MaxSAT solver capabilities¶

IPASIR compatibility¶

For compatibility with IPASIR¹, the interface also exposes literal-level inspection methods:

function val_lit¶

The truth value for a literal in the best solution.

virtual std::optional< bool > Paramita::NonIncrMaxSatSolver::val_lit (
    Literal lit
)

See also: model See ipamir2022 for more details.

function assume¶

Add an assumption for the next solve call.

virtual Paramita::NonIncrMaxSatSolver::assume (
    Literal lit
)

See ipamir2022 for more details.

Interrupting the solving process¶

During optimization, a solver may periodically check whether an external termination signal was issued.

Users can request asynchronous termination via:

function interrupt¶

Interrupts the resolution process.

virtual Paramita::NonIncrMaxSatSolver::interrupt ()

This method instructs the solver to stop solving or propagating. Note that this is a notification, not an immediate stop, when the solver is interrupted is implementation defined.

Precondition:

The solver is solving or propagating.

Postcondition:

After interrupting, the solver must stay in a stable state.

Exception:

UnsupportedMethodException This method is optional.

Warning

When and how interruptions are handled is implementation defined.

4 -->

MkDoxy Error: Incorrect class method configuration

4 -->

Did not find Class with name: Paramita::NonIncrMaxSatSolver and method: seed

4 -->

Available classes and methods:

4 -->

yaml
4 --> NonIncrMaxSatSolver()=default
4 --> NonIncrMaxSatSolver(const NonIncrMaxSatSolver &)=delete
4 --> NonIncrMaxSatSolver(NonIncrMaxSatSolver &&)=delete
4 --> assume(Literal lit)
4 -->NonIncrMaxSatSolver * clone() override
4 -->std::pair< std::uint64_t, std::vector< Literal > > core()
4 --> interrupt()
4 -->std::uint64_t lower_bound()
4 -->std::vector< Literal > model() const =0
4 -->std::uint64_t num_conflicts()
4 -->NonIncrMaxSatSolver & operator=(const NonIncrMaxSatSolver &container)=delete
4 -->NonIncrMaxSatSolver & operator=(NonIncrMaxSatSolver &&)=delete
4 --> simplify(unsigned int num_rounds)
4 -->MAXSAT_ANSWER solve(const std::vector< Literal > &assumptions, const SolvingBudget &budget)=0
4 -->std::optional< bool > val_lit(Literal lit)
4 -->std::uint64_t val_objective() const =0
4 --> ~NonIncrMaxSatSolver() override=default
4 -->

4 -->

Snippet

4 -->```yaml 4 -->::: doxy.paramitaInterfaces.class.method 4 --> name: Paramita::NonIncrMaxSatSolver 4 --> method: seed 4 --> heading_starting_level: 4 4 --> indent_level: 4 -->

4 -->``` 4 -->

Bounding the optimal value¶

Some solvers can provide a lower bound on the objective value:

function lower_bound¶

Returns a lower bound on the objective value of the formula.

virtual std::uint64_t Paramita::NonIncrMaxSatSolver::lower_bound ()

Note:

This method does not require a previous call to solve, as the solver could in theory compute an initial lower bound when adding clauses.

Returns:

The lower bound computed for the formula.

Note

An upper bound can be reported by returning a feasible model.

Unsatisfiable cores¶

If the hard clauses are unsatisfiable, or if infeasibility arises under certain conditions, some solvers may be able to provide an explanation in the form of an unsatisfiable core:

function core¶

Retrieve the unsatisfiable core.

virtual std::pair< std::uint64_t, std::vector< Literal > > Paramita::NonIncrMaxSatSolver::core ()

Returns:

A pair with a) a lower bound associated to the core, and b) a vector filled with a subset of the assumptions that are jointly unsatisfiable.

Precondition:

solve was called with assumptions.

Precondition:

The instance must be unsatisfiable under the given assumptions.

Exception:

UnsupportedMethodException This method is optional.

Formula simplification¶

To provide a hook for users to simplify the underlying formula, implement the satisfy method. This can be called before calling solve.

function simplify¶

Simplify the formula.

virtual Paramita::NonIncrMaxSatSolver::simplify (
    unsigned int num_rounds
)

Parameters:

num_rounds The number of simplification rounds to apply.

Exception:

UnsupportedMethodException This method is optional.

Querying solver statistics¶

Other information about the formula that the users can query is:

function num_conflicts¶

The number of conflicts triggered by a solve call.

virtual std::uint64_t Paramita::NonIncrMaxSatSolver::num_conflicts ()

Note:

The number of conflicts triggered while searching for a solution depends on each algorithm implementation.

Precondition:

Method solve was called.

Returns:

The number of conflicts.

Tomáš Balyo, Armin Biere, Markus Iser, and Carsten Sinz. Sat race 2015. Artificial Intelligence, 241:45–65, 2016. URL: https://www.sciencedirect.com/science/article/pii/S0004370216300984, doi:https://doi.org/10.1016/j.artint.2016.08.007. ↩