Quick start

Your first SAT problem

This guide walks you through creating a simple C++ program that uses MiniSat to solve a Boolean satisfiability problem.

Make sure you have installed MiniSat before proceeding.

Basic concepts

Before diving into code, let’s understand the core components:

Variables

Variables are represented as integers (Var type) starting from 0.

Literals

A literal is a variable or its negation, created with mkLit(var, sign).

Clauses

A clause is a disjunction (OR) of literals, added with addClause().

Solver

The Solver class manages the SAT solving process.

Complete example

Let’s solve a simple 3-SAT problem:

(x_1 \vee \neg x_3) \wedge (x_2 \vee x_3 \vee \neg x_1)

Create the program file

Create a file named example.cc:

example.cc

#include <iostream>
#include "minisat/core/Solver.h"

using namespace Minisat;

int main()
{
    // Create solver instance
    Solver solver;
    
    // Create three variables
    Var x1 = solver.newVar();
    Var x2 = solver.newVar();
    Var x3 = solver.newVar();
    
    // Add clause: (x1 OR NOT x3)
    solver.addClause(mkLit(x1), mkLit(x3, true));
    
    // Add clause: (x2 OR x3 OR NOT x1)
    solver.addClause(mkLit(x2), mkLit(x3), mkLit(x1, true));
    
    // Solve the SAT problem
    bool result = solver.solve();
    
    if (result) {
        std::cout << "SATISFIABLE" << std::endl;
        std::cout << "Solution:" << std::endl;
        std::cout << "  x1 = " << (solver.modelValue(x1) == l_True ? "true" : "false") << std::endl;
        std::cout << "  x2 = " << (solver.modelValue(x2) == l_True ? "true" : "false") << std::endl;
        std::cout << "  x3 = " << (solver.modelValue(x3) == l_True ? "true" : "false") << std::endl;
    } else {
        std::cout << "UNSATISFIABLE" << std::endl;
    }
    
    return 0;
}

Compile the program

g++ -std=c++11 -I/usr/local/include -o example example.cc \
    -L/usr/local/lib -lminisat -lz

Adjust the include and library paths if you installed MiniSat to a different location.

Run the program

./example

Expected output:

SATISFIABLE
Solution:
  x1 = true
  x2 = false
  x3 = false

Understanding the API

Creating variables

Variables are created using newVar():

Var x = solver.newVar();              // Create variable with default polarity
Var y = solver.newVar(l_True);        // Suggest positive polarity
Var z = solver.newVar(l_False, true); // Suggest negative polarity, decision variable

The parameters are:

lbool upol (default: l_Undef): User polarity preference
bool dvar (default: true): Whether the variable is a decision variable

Creating literals

Literals represent variables or their negations:

Var x = solver.newVar();
Lit pos_x = mkLit(x);        // Positive literal: x
Lit neg_x = mkLit(x, true);  // Negative literal: NOT x
Lit also_neg_x = ~mkLit(x);  // Alternative: NOT x

Adding clauses

MiniSat provides several convenient methods to add clauses:

// Add clause: (x)
solver.addClause(mkLit(x));

Clauses are automatically simplified. Adding contradictory clauses may cause addClause() to return false.

Solving

Solve the SAT problem with or without assumptions:

Basic solving
With assumptions
With resource limits

// Solve without assumptions
bool sat = solver.solve();

if (sat) {
    // Problem is satisfiable
    std::cout << "SAT" << std::endl;
} else {
    // Problem is unsatisfiable
    std::cout << "UNSAT" << std::endl;
}

// Solve assuming x is true
bool sat = solver.solve(mkLit(x));

// Solve with multiple assumptions
vec<Lit> assumptions;
assumptions.push(mkLit(x));
assumptions.push(mkLit(y, true));  // Assume NOT y
bool sat2 = solver.solve(assumptions);

// Set conflict budget (max 1000 conflicts)
solver.setConfBudget(1000);

// Set propagation budget
solver.setPropBudget(100000);

// Solve with limits
vec<Lit> dummy;
lbool result = solver.solveLimited(dummy);

if (result == l_True) {
    std::cout << "SAT" << std::endl;
} else if (result == l_False) {
    std::cout << "UNSAT" << std::endl;
} else {
    std::cout << "UNKNOWN (budget exceeded)" << std::endl;
}

// Remove budgets
solver.budgetOff();

Extracting models

When a problem is satisfiable, extract the solution:

if (solver.solve()) {
    // Access individual variable values
    lbool val_x = solver.modelValue(x);
    lbool val_lit = solver.modelValue(mkLit(y));
    
    // Check the value
    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;
    } else {
        std::cout << "x is undefined" << std::endl;
    }
    
    // Print all variable values
    for (int i = 0; i < solver.nVars(); i++) {
        std::cout << "x" << i << " = ";
        if (solver.model[i] == l_True) {
            std::cout << "true";
        } else if (solver.model[i] == l_False) {
            std::cout << "false";
        } else {
            std::cout << "undefined";
        }
        std::cout << std::endl;
    }
}

Advanced example: Incremental solving

MiniSat supports incremental solving, where you can add clauses and re-solve:

#include <iostream>
#include "minisat/core/Solver.h"

using namespace Minisat;

int main()
{
    Solver solver;
    
    // Create variables
    Var x = solver.newVar();
    Var y = solver.newVar();
    Var z = solver.newVar();
    
    // Add initial clauses
    solver.addClause(mkLit(x), mkLit(y));        // (x OR y)
    solver.addClause(mkLit(y, true), mkLit(z)); // (NOT y OR z)
    
    // First solve
    std::cout << "First solve: ";
    if (solver.solve()) {
        std::cout << "SAT" << std::endl;
        std::cout << "  x=" << (solver.modelValue(x) == l_True) << std::endl;
    }
    
    // Add more constraints
    solver.addClause(mkLit(x, true));  // (NOT x)
    solver.addClause(mkLit(z, true));  // (NOT z)
    
    // Solve again
    std::cout << "Second solve: ";
    if (solver.solve()) {
        std::cout << "SAT" << std::endl;
        std::cout << "  y=" << (solver.modelValue(y) == l_True) << std::endl;
    } else {
        std::cout << "UNSAT" << std::endl;
    }
    
    return 0;
}

Using the simplified solver

For problems that benefit from preprocessing, use SimpSolver:

#include <iostream>
#include "minisat/simp/SimpSolver.h"

using namespace Minisat;

int main()
{
    SimpSolver solver;
    
    // Create variables
    Var x = solver.newVar();
    Var y = solver.newVar();
    Var z = solver.newVar();
    
    // Add clauses
    solver.addClause(mkLit(x), mkLit(y));
    solver.addClause(mkLit(y, true), mkLit(z));
    solver.addClause(mkLit(z, true), mkLit(x, true));
    
    // Solve with preprocessing enabled
    bool result = solver.solve(true, false);
    // Parameters: do_simp=true, turn_off_simp=false
    
    if (result) {
        std::cout << "SATISFIABLE" << std::endl;
        // Note: eliminated variables may not appear in the model
        if (!solver.isEliminated(x)) {
            std::cout << "x = " << (solver.modelValue(x) == l_True) << std::endl;
        }
    } else {
        std::cout << "UNSATISFIABLE" << std::endl;
    }
    
    return 0;
}

Use SimpSolver when dealing with large formulas that may contain redundant variables or clauses. The preprocessing can significantly reduce solving time.

Common solver statistics

Access solver statistics during or after solving:

Solver solver;

// Enable verbose output
solver.verbosity = 1;

// ... add clauses and solve ...

// Print statistics
solver.printStats();

// Access specific statistics
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;

Makefile for your project

Create a Makefile to simplify compilation:

CXX = g++
CXXFLAGS = -std=c++11 -Wall -O3
INCLUDES = -I/usr/local/include
LDFLAGS = -L/usr/local/lib
LIBS = -lminisat -lz

all: example

example: example.cc
	$(CXX) $(CXXFLAGS) $(INCLUDES) -o $@ $< $(LDFLAGS) $(LIBS)

clean:
	rm -f example

Then simply run make to build your program.

Reading DIMACS files

To read problems in DIMACS CNF format:

#include <iostream>
#include <zlib.h>
#include "minisat/core/Solver.h"
#include "minisat/core/Dimacs.h"

using namespace Minisat;

int main(int argc, char** argv)
{
    if (argc < 2) {
        std::cerr << "Usage: " << argv[0] << " <input.cnf>" << std::endl;
        return 1;
    }
    
    Solver solver;
    
    // Open and parse DIMACS file
    gzFile in = gzopen(argv[1], "rb");
    if (in == NULL) {
        std::cerr << "ERROR: Could not open file: " << argv[1] << std::endl;
        return 1;
    }
    
    parse_DIMACS(in, solver);
    gzclose(in);
    
    std::cout << "Parsed " << solver.nVars() << " variables and " 
              << solver.nClauses() << " clauses" << std::endl;
    
    // Solve
    if (solver.solve()) {
        std::cout << "SATISFIABLE" << std::endl;
    } else {
        std::cout << "UNSATISFIABLE" << std::endl;
    }
    
    return 0;
}

Compile with:

g++ -std=c++11 -I/usr/local/include -o dimacs_solver dimacs_solver.cc \
    -L/usr/local/lib -lminisat -lz

Troubleshooting

Compilation errors about missing headers

Ensure the include path points to your MiniSat installation:

g++ -I/usr/local/include ...

Or if installed locally:

g++ -I$HOME/.local/include ...

Linking errors about undefined references

Make sure to link against both MiniSat and zlib:

g++ ... -L/usr/local/lib -lminisat -lz

Runtime error: cannot open shared object file

Add the library path to LD_LIBRARY_PATH:

export LD_LIBRARY_PATH=/usr/local/lib:$LD_LIBRARY_PATH
./example

Solver returns UNSAT but problem should be SAT

Check your clause construction:

Ensure literals are created correctly with mkLit(var, sign)
Remember that sign=true means negation
Verify clause order and variable indices

Next steps

API reference

Detailed documentation of the Solver class

Advanced features

Resource limits, interruption, and optimization

Get Started

Core Concepts

Advanced Usage

Examples

Your first SAT problem

Basic concepts

Variables

Literals

Clauses

Solver

Complete example

Understanding the API

Creating variables

Creating literals

Adding clauses

Solving

Extracting models

Advanced example: Incremental solving

Using the simplified solver

Common solver statistics

Makefile for your project

Reading DIMACS files

Troubleshooting

Next steps

API reference

Advanced features

Build docs developers (and LLMs) love

Get Started

Core Concepts

Advanced Usage

Examples

​Your first SAT problem

​Basic concepts

Variables

Literals

Clauses

Solver

​Complete example

​Understanding the API

​Creating variables

​Creating literals

​Adding clauses

​Solving

​Extracting models

​Advanced example: Incremental solving

​Using the simplified solver

​Common solver statistics

​Makefile for your project

​Reading DIMACS files

​Troubleshooting

​Next steps

API reference

Advanced features

Build docs developers (and LLMs) love

Your first SAT problem

Basic concepts

Complete example

Understanding the API

Creating variables

Creating literals

Adding clauses

Solving

Extracting models

Advanced example: Incremental solving

Using the simplified solver

Common solver statistics

Makefile for your project

Reading DIMACS files

Troubleshooting

Next steps