Skip to content

Using a SAT solver

This guide shows how to load an external SAT solver plugin, add clauses, run the solver, and read the satisfying assignment.

Paramita does not implement SAT solvers itself. Instead, it loads compiled solvers as shared libraries.

Prerequisites

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

paramita plugins build cmake "#sat-solvers/cadical-3.0.0"

To create an instance of a SatSolver, we use the [from_name][paramita.solvers.SatSolver.from_name] static method from the class, which will look on the default paths for a solver with this name:

from paramita.solvers import SatSolver

s = SatSolver.from_name("Cadical300")

Note

Alternatively, if we have the path to the plugin file, we can use [dynamic_load][paramita.solvers.SatSolver.dynamic_load]:

s = SatSolver.dynamic_load(".plugins/sat/incremental-solvers/libsat-solvers-cadical-300.so")

s is now a SatSolver instance, and we can add clauses to it. Clauses are lists of integers. Positive integers represent variables (1 means \(x_1\)), negative integers represent negated literals (-1 means \(\neg x_1\)). Variables do not need to be declared beforehand; they are created automatically when first used.

To add clauses we can use the methods from ClauseContainer: add_clause, add_clauses, and add_lit.

s.add_clause([1, 2])

s.add_clause([-1, 3])

s.add_clauses([[2, -3], [-2, 3]])

To solve the current set of clauses, call solve.

result = s.solve()

The return value is True if the formula is satisfiable, False if unsatisfiable, and None if the solver could not decide.

Note

An usual case where a solver cannot decide if the formula is satisfiable or not is when using a budget that sets some limits to its underlying algorithm. We will see those later on.

If the result is True, we can retrieve the satisfying assignment with model. The method returns a list where every variable appears exactly once: positive if the variable is true, negative if false. For example, [1, -2, 3] means x1 is true, x2 is false, x3 is true.

if result:
    model = s.model()
    print(model)  # for example, [1, -2, 3] means x1=true, x2=false, x3=true

We can also query the truth value of a specific literal using val_lit: 

print(s.val_lit(1))   # True if x1 is true
print(s.val_lit(2))   # False if x2 is false

The solver is incremental, meaning we can add more clauses after a solve call and run solve again without recreating the solver. The previously added clauses stay in place.

s.add_clause([-1, -3])
new_result = s.solve()

Note

When we do not need incremental solving, we can use a NonIncrSatSolver plugin. The methods are similar, with the main difference being that those solvers can accept multiple calls to solve, but after the first one we cannot add more clauses to it.

Solving with assumptions and unsatisfiable cores

Assumptions let us impose temporary unit clauses for a single solve call. They are useful for testing hypotheses or performing incremental solving without permanently modifying the clause database. For example, we can ask: "If I assume x1 = false and x2 = true, is the formula still satisfiable?"

To use assumptions, we pass a list of literals to the assumptions parameter of solve:

# Assume x1 = false, x2 = true
result = s.solve(assumptions=[-1, 2])

Warning

The solver does not remember assumptions across different solve calls. Each call starts with a clean assumption set.

If the result is True (satisfiable), we can use model as we saw before to retrieve a satisfying assignment.

But what if the result is False? When using assumptions, we can query the solver to provide us a subset of the assumptions that make the formula unsatisfiable. This is called an unsatisfiable core, and we can retrieve it using the core method:

if result is False:
    core = s.core()
    print("Unsatisfiable core:", core)  # e.g., [-1, 2]

The core contains literals that are jointly responsible for the unsatisfiability. It is always a subset of the assumptions you provided. You can use it to debug over‑constrained problems or to implement advanced algorithms like MaxSAT or MUS extraction.

Warning

core is only meaningful after an unsatisfiable result (solve returned False).

Here is a complete example, where we work with the following formula:

\[ (x_1 \vee x_2) \wedge (\neg x_1 \vee x_3) ∧ (\neg x_2 \vee \neg x_3) \]

from paramita.solvers import SatSolver

solver = SatSolver.dynamic_load(".plugins/sat/incremental-solvers/libsat-solvers-cadical-300.so")

solver.add_clauses([
    [1, 2],
    [-1, 3],
    [-2, -3]
])

# Assume x1=false, x2=false
result = solver.solve(assumptions=[-1, -2])

assert result is False # we cannot satisfy the first clause!
core = solver.core()
print("Core assumptions:", core) # Output: [-1, -2]
In this example the core is [-1, -2], because assuming both \(x_1\) and \(x_2\) to false makes the clause \((x_1 \vee x_2)\) false.

Next steps