Skip to main content

​
Variables

In MiniSat, variables are the fundamental building blocks of Boolean formulas. They represent Boolean values that can be either true or false.

​
Variable representation

Variables are represented as simple integers:
SolverTypes.h
typedef int Var;
const Var var_Undef = -1;
Variables are just integers chosen from 0 to N-1, allowing them to be used directly as array indices for efficient access to variable-related data structures.

​
Creating variables

You create new variables using the newVar() method: 
Solver solver;
Var x = solver.newVar();  // Creates variable 0
Var y = solver.newVar();  // Creates variable 1
Var z = solver.newVar();  // Creates variable 2
Variables are numbered sequentially starting from 0. The solver maintains an internal counter for the next variable ID.

​
Variable properties

Each variable can have associated properties:
The preferred truth value for branching decisions:
solver.setPolarity(x, l_True);  // Prefer x = true
solver.setPolarity(y, l_False); // Prefer y = false
Whether the variable can be used in decision branching:
solver.setDecisionVar(x, true);  // x can be decided
solver.setDecisionVar(y, false); // y is determined by propagation
A heuristic score that tracks variable importance:
// Internal: activity is updated automatically
VMap<double> activity;  // Higher activity = more important

​
Literals

A literal is a variable or its negation. Literals are how variables appear in clauses.

​
Literal structure

Literals are represented by a single integer that encodes both the variable and its sign:
SolverTypes.h
struct Lit {
    int x;  // Encoded variable and sign
    
    bool operator == (Lit p) const { return x == p.x; }
    bool operator != (Lit p) const { return x != p.x; }
    bool operator <  (Lit p) const { return x < p.x; }
};
The encoding scheme uses the formula: x = var * 2 + signThis clever encoding makes positive and negative literals of the same variable adjacent in memory, which is efficient for various operations.

​
Creating literals

Use the mkLit() function to create literals: 
Var x = 0;

// Create positive literal (x)
Lit pos_x = mkLit(x, false);
Lit pos_x = mkLit(x);  // Default is positive

// Create negative literal (¬x)
Lit neg_x = mkLit(x, true);
SolverTypes.h
inline Lit mkLit(Var var, bool sign) {
    Lit p;
    p.x = var + var + (int)sign;
    return p;
}

​
Literal operations

MiniSat provides several operations for working with literals: 
// Negate a literal using ~
Lit p = mkLit(x, false);  // x
Lit neg_p = ~p;           // ¬x

// Implementation
inline Lit operator ~(Lit p) {
    Lit q;
    q.x = p.x ^ 1;  // Flip the last bit
    return q;
}

​
Special literal constants

MiniSat defines special literal values: 
const Lit lit_Undef = { -2 };  // Undefined literal
const Lit lit_Error = { -1 };  // Error indicator
Do not create literals manually by setting the x field. Always use mkLit() to ensure correct encoding.

​
Lifted booleans (lbool)

MiniSat uses a three-valued logic system represented by the lbool type:
SolverTypes.h
class lbool {
    uint8_t value;
    
public:
    explicit lbool(uint8_t v) : value(v) { }
    lbool() : value(0) { }  // Default is l_True
    explicit lbool(bool x) : value(!x) { }
};

const lbool l_True  ((uint8_t)0);
const lbool l_False ((uint8_t)1);
const lbool l_Undef ((uint8_t)2);

​
Using lbool

// Check variable assignment
lbool val = solver.value(x);

if (val == l_True) {
    // x is assigned true
} else if (val == l_False) {
    // x is assigned false
} else {
    // x is unassigned (l_Undef)
}

​
lbool operations

The lbool type supports logical operations: 
lbool a = l_True;
lbool b = l_False;
lbool c = l_Undef;

// Logical AND
lbool result1 = a && b;  // l_False
lbool result2 = a && c;  // l_Undef

// Logical OR
lbool result3 = a || b;  // l_True
lbool result4 = b || c;  // l_Undef

// XOR with boolean (negation)
lbool result5 = a ^ true;  // Flip value
The three-valued logic allows MiniSat to represent partial assignments during the search process. Variables can be true, false, or not yet assigned.

​
Data structures

MiniSat provides specialized map types for efficient variable and literal indexing: 
// Variable maps
template<class T> class VMap : public IntMap<Var, T>{};

// Literal maps
template<class T> class LMap : public IntMap<Lit, T, MkIndexLit>{};

// Literal sets
class LSet : public IntSet<Lit, MkIndexLit>{};

​
Example usage

// Map from variables to doubles
VMap<double> activity;
activity[x] = 1.5;

// Map from literals to assignment levels
LMap<int> levels;
levels[mkLit(x, false)] = 3;

// Set of literals (e.g., for conflict clauses)
LSet conflict;
conflict.insert(mkLit(x, true));
These specialized types use the integer representation of variables and literals for O(1) access time, making them much faster than hash tables for this use case.

​
Conversion functions

MiniSat provides functions to convert between different representations: 
// Variable to integer
int toInt(Var v);  // Returns the variable number

// Literal to integer
int toInt(Lit p);  // Returns the encoded literal

// Integer to literal
Lit toLit(int i);  // Reconstructs literal from encoding

// lbool conversions
int toInt(lbool l);      // Convert to 0, 1, or 2
lbool toLbool(int v);    // Convert from integer

​
Next steps

Clauses

Learn how literals are combined into clauses

SAT solving

Understand how variables are assigned during solving

DIMACS format

See how variables are represented in input files

Build docs developers (and LLMs) love

Get started for freeTalk to us