Skip to content

Implementing a SAT solver

Solver extensions define components that reason over propositional formulas and expose their results through a common API. They abstract away the internal search, learning, and optimization mechanisms of concrete solvers, while standardizing how satisfiability, assignments, conflicts, and related solver state can be observed and controlled.

In Paramita, solver extensions are represented by the Paramita::NonIncrSatSolver and its incremental variant Paramita::SatSolver (the difference is explained later in this chapter).

Class Paramita::NonIncrSatSolver

A SAT solver.

Note:

Use SATSOLVER_C_INTERFACE to register any subclass of this interface.

  • #include <NonIncrSatSolver.hpp>

Inherits the following classes: Paramita::ClauseContainer

Class Paramita::SatSolver

An incremental SAT Solver.

Note:

Use SATSOLVER_C_INTERFACE to register any subclass of this interface.

Incremental solvers allow to modify the formula and call solve as many times as needed. After modifying the formula (by adding new clauses), solve with the same parameters (i.e. assumptions, budgets...) can return different values.

  • #include <SatSolver.hpp>

Inherits the following classes: Paramita::NonIncrSatSolver

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

Implement the clause container interface

A solver is also a clause container. Before it can reason about a formula, it must be able to accept clauses and keep track of the variables involved. Before implementing any solver-related functions, please follow the guide on how to implement the container interface.

At least you need to implement:

  • add_clause
  • max_var
  • set_minimum_var

Implementing the solving procedure

The core responsibility of a solver is to determine the satisfiability of the stored formula. This is exposed through the solve method:

function solve

Solve the underlying formula under the given assumptions. 

virtual std::optional< bool > Paramita::NonIncrSatSolver::solve (
    const std::vector< Literal > & assumptions,
    const SolvingBudget & budget
) = 0

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

See also: interrupt

Parameters:

  • assumptions A vector with literals that will be fixed during this solve call.
  • budget Solving limits for this call.

Precondition:

The method solve was not called previously OR no the formula has not been modified since the last solve call.

Postcondition:

The solving budget is reset to unlimited.

Returns:

An option with a boolean representing the satisfiability status of the formula under the specified assumptions, or std::nullopt if it could not be determined.

Note

For now ignore assumptions and budget, later in the chapter we will go back to this.

Calling solve triggers the internal solving algorithm and returns:

  • true if the formula is satisfiable,
  • false if the formula is unsatisfiable, or
  • std::nullopt if the solver could not determine satisfiability (for example due to budget exhaustion or interruption).

The exact behaviour of the solving process is entirely implementation defined.

Model extraction

On satisfiable formulas, the users can query the solver for a satisfying assignment using the model method:

function model

Get the model (solution) after solving. 

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

Returns:

The vector where the solution will be stored. Each element of the vector is a literal that was set to true.

Precondition:

The method solve was called.

Precondition:

A solution was found by solve.

Warning:

Undefined behaviour if solve returned std::nothing.

Exception:

A model is represented as a list of integers. The absolute value of the each integer denotes a variable identifier, while the sign represents the assigned truth value (positive for true, negative for false).

The solver is responsible for ensuring that the returned model is consistent with the result of the most recent call to solve.

Assumptions and unsatisfiable cores

Some use cases require the solver to evaluate the feasibility of the formula under a certain set of assumptions. The solve method optionally accepts a set of assumptions, which are literals that are (temporarily) fixed to a value for the duration of a single solving call.

On an unsatisfiable formula under a set of assumptions, some solvers are able to find an explanation about which of the literals in the core led to a conflict. This information is exposed through the core method:

function core

Retrieve the unsatisfiable core. 

virtual std::vector< Literal > Paramita::NonIncrSatSolver::core ()

Returns:

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:

Note

The core is a subset of the assumptions, but this subset might not be minimal.

Budget constraints

Solvers may support limiting the resources used during the solving process by using budget constraints. The budget is provided to the solve method, and can restrict, for example, the number of conflicts the solver is allowed to find.

Once the budget is exhausted, the solve method returns, and if the feasibility of the instance couldn't be determined, it returns std::nullopt.

Struct Paramita::SolvingBudget

A budget for the underlying solver.

The budget allows to set a limit to the solvers based on different limits. Currently the supported limits are:

  • num_conflicts: Number of conflicts
  • num_propagations: Number of propagations

  • cpu_time_seconds: CPU Time in seconds

  • #include <definitions.hpp>

Warning

Support for different budget constraints is implementation defined.

Incremental vs non-incremental solvers

Paramita distinguishes between non-incremental and incremental solvers.

A non-incremental solver implements the Paramita::NonIncrSatSolver. Once solve is called, the internal formula is considered fixed. While multiple calls to solve are allowed (e.g. with different assumptions or budgets), the formula itself must not be modified.

An incremental solver implements Paramita::SatSolver. In this case, new clauses may be added after a call to solve, and subsequent calls will reason over the extended formula.

Unless explicitly stated otherwise, all methods defined for :class:Paramita::NonIncrSatSolver behave identically for incremental solvers.

Registering the solver as an extension

Imagine you have created your SAT solver, and have the following class:

// in satsolver.hpp
class MySatSolver : public SatSolver {
      // ...
};

// in satsolver.cpp
MySatSolver::MySatSolver() { /* ... */ };
// other methods...

Now you want to expose this solver as a loadable extension for Paramita. For this, you only need to use the macro SATSOLVER_C_INTERFACE in your satsolver.cpp file:

// in satsolver.cpp
MySatSolver::MySatSolver() { /* ... */ };
// other methods...
SATSOLVER_C_INTERFACE(MySatSolver)

Note

This macro is defined in the header paramita/sat/SatSolver.hpp.

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

!!! note:: A similar macro is provided by paramita/sat/NonIncrSatSolver.hpp: NON_INCR_SATSOLVER_C_INTERFACE

Testing the SAT solver

To ensure that the solver implementation behaves like Paramita expects, we have provided some tests using the doctest framework.

To enable those tests, create a test_solver.cpp file and use the doctest macro to expand the templated tests for your solver:

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

#include "satsolver.hpp"
#include <paramita/tests/sat/TestSatSolver.hpp>

GENERATE_DOCTESTS_FOR_SAT_SOLVER(MySatSolver)

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

Note

A similar macro is provided by paramita/sat/TestNonIncrSatSolver.hpp: GENERATE_DOCTESTS_FOR_NON_INCR_SAT_SOLVER

Other optional solvers' capabilities

IPASIR compatibility

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

function val_lit

Get the truth value for a literal. 

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

Parameters:

  • lit The literal to check.

Returns:

lit if the literal belongs to the model, -lit if its negation belongs to the model, and 0 if it is not determined.

Precondition:

solve was called.

Precondition:

A solution was found by solve.

See BALYO201645 for more details.

Exception:

function failed

Check if a literal belongs to the unsatisfiable core. 

virtual bool Paramita::NonIncrSatSolver::failed (
    Literal lit
)

Parameters:

  • lit The literal to be checked.

Returns:

true if the literal belongs to the unsatisfiable core, false otherwise.

Precondition:

The instance must be unsatisfiable under the given assumptions.

See BALYO201645 for more details.

Exception:

4 -->

4 -->

MkDoxy Error: Incorrect class method configuration

4 -->

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

4 -->
4 -->Available classes and methods: 4 -->yaml 4 --> NonIncrSatSolver()=default 4 --> NonIncrSatSolver(const NonIncrSatSolver &)=delete 4 --> NonIncrSatSolver(NonIncrSatSolver &&)=delete 4 --> assume(Literal lit) 4 -->NonIncrSatSolver * clone() override 4 -->std::vector< Literal > core() 4 -->bool failed(Literal lit) 4 --> freeze(Literal lit) 4 -->std::optional< bool > get_phase(Literal lit) 4 --> interrupt() 4 -->std::optional< bool > is_fixed(Literal lit) 4 -->bool is_frozen(Literal lit) 4 --> melt(Literal lit) 4 -->std::vector< Literal > model() const =0 4 -->int num_active_vars() 4 -->long num_conflicts() 4 -->NonIncrSatSolver & operator=(const NonIncrSatSolver &container)=delete 4 -->NonIncrSatSolver & operator=(NonIncrSatSolver &&)=delete 4 --> phase(Literal lit) 4 -->std::pair< bool, std::vector< Literal > > propagate(const std::vector< Literal > &assumptions) 4 --> simplify(unsigned int num_rounds) 4 -->std::optional< bool > solve(const std::vector< Literal > &assumptions, const SolvingBudget &budget)=0 4 --> unphase(Literal lit) 4 -->std::optional< bool > val_lit(Literal lit) 4 --> ~NonIncrSatSolver() override=default 4 --> 4 -->
4 -->
4 -->Snippet 4 -->```yaml 4 -->::: doxy.paramitaInterfaces.class.method 4 --> name: Paramita::NonIncrSatSolver 4 --> method: seed 4 --> heading_starting_level: 4 4 --> indent_level: 4 -->

4 -->``` 4 -->

Operations on the underlying formula

Some solvers allow to perform the :term:unit propagation step isolated from a solving process. Paramita exposes this as the propagate method:

function propagate

Propagate the given assumptions. 

virtual std::pair< bool, std::vector< Literal > > Paramita::NonIncrSatSolver::propagate (
    const std::vector< Literal > & assumptions
)

Parameters:

  • assumptions A list of literals assumed to be true.

Returns:

A pair with a) true if propagation succeeded without a conflict, false if a conflict was found; and b) a vector with the literals propagated as a result of the assumptions. In case the propagation fails, the vector might be empty.

Exception:

Paramita also exposes a method to simplify the internal formula in the SAT solver:

function simplify

Simplify the formula. 

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

Parameters:

  • num_rounds The number of simplification rounds to apply.

Exception:

Interrupting the solving process

During the solving algorithm, some solvers might check if an external event triggered termination, and stop the process, reporting that the formula's satisfiability could not be determined.

With the interrupt method, users can notify the solver that they wish to terminate the solving process asynchronously.

Warning

When and how the solver is interrupted, as well as if it is an immediate operation or not is implementation defined.

function interrupt

Interrupts the resolution process. 

virtual Paramita::NonIncrSatSolver::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:

Decision heuristics

These are the optional methods for setting, unsetting and obtaining the phase of a given literal:

function get_phase

Returns the default phase for a decision variable. 

virtual std::optional< bool > Paramita::NonIncrSatSolver::get_phase (
    Literal lit
)

Parameters:

  • lit The literal representing the decision variable. Only its absolute value (i.e. the variable) is considered.

Returns:

True if the phase is positive, False if negative, or std::nothing if it was not set.

Exception:

function unphase

Removes the default phase for a decision variable. 

virtual Paramita::NonIncrSatSolver::unphase (
    Literal lit
)

Parameters:

  • lit The literal representing the decision variable. Only its absolute value (i.e. the variable) is considered.

Exception:

function get_phase

Returns the default phase for a decision variable. 

virtual std::optional< bool > Paramita::NonIncrSatSolver::get_phase (
    Literal lit
)

Parameters:

  • lit The literal representing the decision variable. Only its absolute value (i.e. the variable) is considered.

Returns:

True if the phase is positive, False if negative, or std::nothing if it was not set.

Exception:

Frozen variables

These are the methods to freeze and melt variables, and to check if a given variable is frozen in the SAT solver:

function freeze

Freeze a variable. 

virtual Paramita::NonIncrSatSolver::freeze (
    Literal lit
)

A frozen variable is a variable that is potentially needed in the future (for example, new assumptions). Internally, the solver can decide to perform variable elimination.

A variable can be frozen multiple times, as in Lingeling or CaDiCaL. You must call melt the same number of times to "unfreeze" a variable.

See

Parameters:

  • lit The literal representing the variable. Only its absolute value (i.e. the variable) is considered.

See also: melt, is_frozen

Exception:

function melt

Melts a variable. 

virtual Paramita::NonIncrSatSolver::melt (
    Literal lit
)

Parameters:

  • lit The literal representing the variable. Only its absolute value (i.e. the variable) is considered.

See also: freeze, is_frozen

Exception:

function is_frozen

Checks if a variable is frozen. 

virtual bool Paramita::NonIncrSatSolver::is_frozen (
    Literal lit
)

Parameters:

  • lit The literal representing the variable. Only its absolute value (i.e. the variable) is considered.

Returns:

See also: freeze, melt

Exception:

Querying information of the solver and the formula

Additional methods can be provided by the solver to report richer information about the formula.

Currently the following are supported:

function is_fixed

Detect if a variable is implied at root level. 

virtual std::optional< bool > Paramita::NonIncrSatSolver::is_fixed (
    Literal lit
)

Parameters:

  • lit The literal representing the variable. Only its absolute value (i.e. the variable) is considered.

Returns:

True if the variable is implied by the formula, False if its negation is implied, or std::nothing if it has not yet been determined.

Exception:

function num_conflicts

Get the number of conflicts encountered. 

virtual long Paramita::NonIncrSatSolver::num_conflicts ()

Returns:

The total number of conflicts found during solve.

Exception:

function num_active_vars

Counts how many variables are active. 

virtual int Paramita::NonIncrSatSolver::num_active_vars ()

An active variable is a variable that exists in an irredundant clause (i.e. not satisfied, subsumed, or eliminated). Variable become inactive if they are eliminated or fixed at the root level.

Returns:

The number of active variables.

Exception:

  1. 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. ↩