Skip to main content
This guide shows how to create a solver, add clauses, and check satisfiability.

​
Simple SAT problem

Here’s a complete example that solves a simple SAT problem: 
#include "minisat/core/Solver.h"
#include <iostream>

using namespace Minisat;

int main() {
    // Create solver instance
    Solver solver;
    
    // Create three boolean variables
    Var x = solver.newVar();
    Var y = solver.newVar();
    Var z = solver.newVar();
    
    // Add clause: (x OR y)
    solver.addClause(mkLit(x), mkLit(y));
    
    // Add clause: (NOT x OR NOT y OR z)
    solver.addClause(~mkLit(x), ~mkLit(y), mkLit(z));
    
    // Add clause: (NOT z)
    solver.addClause(~mkLit(z));
    
    // Solve the formula
    bool sat = solver.solve();
    
    if (sat) {
        std::cout << "SAT" << std::endl;
        std::cout << "x = " << (solver.modelValue(x) == l_True ? "true" : "false") << std::endl;
        std::cout << "y = " << (solver.modelValue(y) == l_True ? "true" : "false") << std::endl;
        std::cout << "z = " << (solver.modelValue(z) == l_True ? "true" : "false") << std::endl;
    } else {
        std::cout << "UNSAT" << std::endl;
    }
    
    return 0;
}
1
Create solver instance
2
Instantiate the Solver class:
3
Solver solver;
4
Create variables
5
Use newVar() to create boolean variables. Variables are represented as integers:
6
Var x = solver.newVar();
Var y = solver.newVar();
7
Create literals
8
Literals are created using mkLit(). Use ~ for negation:
9
Lit pos_x = mkLit(x);    // positive literal
Lit neg_x = ~mkLit(x);   // negative literal (NOT x)
10
Add clauses
11
Clauses can be added in several ways:
12
// Unit clause
solver.addClause(mkLit(x));

// Binary clause
solver.addClause(mkLit(x), mkLit(y));

// Ternary clause
solver.addClause(mkLit(x), mkLit(y), mkLit(z));

// Quaternary clause
solver.addClause(mkLit(x), mkLit(y), mkLit(z), mkLit(w));

// Arbitrary length using vec<Lit>
vec<Lit> clause;
clause.push(mkLit(x));
clause.push(~mkLit(y));
solver.addClause(clause);
13
Solve
14
Call solve() to check satisfiability:
15
bool sat = solver.solve();
if (sat) {
    // Formula is satisfiable
} else {
    // Formula is unsatisfiable
}
16
Extract model
17
If satisfiable, extract variable assignments:
18
if (sat) {
    lbool val_x = solver.modelValue(x);
    if (val_x == l_True) {
        std::cout << "x is true" << std::endl;
    } else if (val_x == l_False) {
        std::cout << "x is false" << std::endl;
    }
}

​
Checking solver state

You can check if the solver is in a consistent state: 
if (!solver.okay()) {
    // Solver detected a conflict during clause addition
    std::cout << "Formula is trivially UNSAT" << std::endl;
}
The okay() method returns false if the solver has detected that the formula is unsatisfiable during clause addition or simplification.

​
Getting solver statistics

Access solver statistics after solving: 
std::cout << "Variables: " << solver.nVars() << std::endl;
std::cout << "Clauses: " << solver.nClauses() << std::endl;
std::cout << "Decisions: " << solver.decisions << std::endl;
std::cout << "Conflicts: " << solver.conflicts << std::endl;
std::cout << "Propagations: " << solver.propagations << std::endl;

// Or print all statistics
solver.printStats();

​
Simplification

Call simplify() to perform unit propagation and remove satisfied clauses: 
if (!solver.simplify()) {
    std::cout << "UNSAT by simplification" << std::endl;
    return;
}

bool sat = solver.solve();
Simplification is automatically performed during solving, but you can call it explicitly to detect unsatisfiability early.

Build docs developers (and LLMs) love

Get started for freeTalk to us