SAT Reduction Technique, in depth: reducing your problem to SAT, with model, encode, solve, decode and verify, worked end to end on bounded model checking

Which direction, and what it must preserve

Getting the arrow the wrong way round is the classic mistake. Reducing your problem to SAT tells you nothing about how hard your problem is. It only says SAT is at least as expressive, and since SAT is NP-complete, every problem in NP reduces to it. It is useful because modern CDCL solvers handle millions of clauses on structured instances. For it to be useful, the reduction must be polynomial-size and must preserve the answer: the formula is satisfiable exactly when your instance is a yes-instance. For extraction you also need a witness map, a way to turn any model into a solution of the original problem.

Some problems reduce more cheaply to something else. A problem whose clauses all have two literals is 2-SAT, which strongly connected components solve in linear time. Check for that structure before reaching for a general solver.

The method in five steps

1. Model in the problem's own terms first. Here that is a table of guarded commands ("in pc idle, seeing the other flag down, go to mid"). This table is the specification, and both the encoder and the checker read it.
2. Pick variables that make constraints short. A one-hot encoding of a process's program counter (one Boolean per value per time step) turns every transition rule into a single implication clause. A binary encoding saves variables but makes each rule several clauses, and harder to get right.
3. Write implications, not formulas. "a and b and c imply d" is the clause (not a or not b or not c or d). If every rule has that shape, you never need a general CNF converter. Disjunctions of conjunctions need Tseitin auxiliary variables.
4. Constrain exactly-one explicitly. One clause gives at least one value. Pairwise clauses give at most one, which is fine for three values. Use a sequential counter for long domains.
5. Decode, then verify independently. The model is evidence, not truth. Replay it against the specification with code that shares nothing with the encoder.

A bounded model checker in one file

Two processes share one flag each. A step moves exactly one process, chosen by one Boolean per step. The encode function unrolls the transition relation k times, which is the core idea of bounded model checking, introduced by Biere, Cimatti, Clarke and Zhu in 1999. The DPLL here is deliberately tiny so the example is self-contained. For real sizes, write the clauses out as DIMACS and run a competition solver such as CaDiCaL or Kissat, which print an s SATISFIABLE line followed by v lines listing the model.

import itertools
PCS = ("idle", "mid", "crit")
# Guarded commands: (pc, other_flag, next_pc, my_flag_after or None = unchanged)
CHECK_THEN_SET = [("idle", False, "mid", None), ("idle", True, "idle", None),
                  ("mid", False, "crit", True), ("mid", True, "crit", True),
                  ("crit", False, "idle", False), ("crit", True, "idle", False)]
SET_THEN_CHECK = [("idle", False, "mid", True), ("idle", True, "mid", True),
                  ("mid", False, "crit", None), ("mid", True, "mid", None),
                  ("crit", False, "idle", False), ("crit", True, "idle", False)]

class Vars:
    """Name <-> DIMACS integer. Names are tuples like ("pc", proc, value, t)."""
    def __init__(self):
        self.ids, self.names = {}, [None]
    def __call__(self, *name):
        if name not in self.ids:
            self.ids[name] = len(self.names)
            self.names.append(name)
        return self.ids[name]

def encode(protocol, k, bad):
    """CNF whose models are exactly the k-step runs that end in a `bad` state."""
    assert len({(p, g) for p, g, _, _ in protocol}) == len(protocol) == 6
    V, cnf = Vars(), []
    pc = lambda i, p, t: V("pc", i, p, t)
    flag = lambda i, t: V("flag", i, t)
    mover = lambda i, t: V("m", t) if i == 1 else -V("m", t)   # one bit picks who moves
    for t in range(k + 1):
        for i in (0, 1):
            cnf.append([pc(i, p, t) for p in PCS])              # at least one value
            for a, b in itertools.combinations(PCS, 2):
                cnf.append([-pc(i, a, t), -pc(i, b, t)])         # at most one
    for i in (0, 1):
        cnf += [[pc(i, "idle", 0)], [-flag(i, 0)]]               # initial state
    for t in range(k):
        for i in (0, 1):
            j = 1 - i
            for p, g, nxt, f in protocol:                       # the mover obeys its command
                pre = [-mover(i, t), -pc(i, p, t), flag(j, t) if not g else -flag(j, t)]
                cnf.append(pre + [pc(i, nxt, t + 1)])
                if f is None:
                    cnf.append(pre + [-flag(i, t), flag(i, t + 1)])
                    cnf.append(pre + [flag(i, t), -flag(i, t + 1)])
                else:
                    cnf.append(pre + [flag(i, t + 1) if f else -flag(i, t + 1)])
            for p in PCS:                                       # the other process is frozen
                cnf.append([mover(i, t), -pc(i, p, t), pc(i, p, t + 1)])
            cnf.append([mover(i, t), -flag(i, t), flag(i, t + 1)])
            cnf.append([mover(i, t), flag(i, t), -flag(i, t + 1)])
    for i, p in bad:
        cnf.append([pc(i, p, k)])                               # bad state at step k
    return V, cnf

def dpll(cnf, assign=None):
    """Tiny DPLL with unit propagation: fine for hundreds of variables, not millions."""
    assign = dict(assign or {})
    while True:
        unit, clauses = None, []
        for cl in cnf:
            if any(assign.get(abs(l)) == (l > 0) for l in cl):
                continue
            rest = [l for l in cl if abs(l) not in assign]
            if not rest:
                return None                                      # conflict
            if len(rest) == 1:
                unit = rest[0]
            clauses.append(rest)
        if unit is None:
            break
        assign[abs(unit)] = unit > 0
    if not clauses:
        return assign
    x = abs(clauses[0][0])
    for val in (True, False):
        model = dpll(clauses, {**assign, x: val})
        if model is not None:
            return model
    return None

def decode(V, model, k):
    return [(tuple((next(p for p in PCS if model.get(V("pc", i, p, t))),
                    bool(model.get(V("flag", i, t)))) for i in (0, 1)),
             None if t == k else int(bool(model.get(V("m", t)))))
            for t in range(k + 1)]

def replay(protocol, trace, bad):
    """Independent check: re-run the trace on the protocol table, not on the CNF."""
    table = {(p, g): (n, f) for p, g, n, f in protocol}
    state = trace[0][0]
    assert state == (("idle", False), ("idle", False))
    for (cur, who), (nxt, _) in zip(trace, trace[1:]):
        assert cur == state
        p, fl = state[who]
        n, f = table[(p, state[1 - who][1])]
        state = tuple((n, fl if f is None else f) if i == who else state[i] for i in (0, 1))
        assert state == nxt
    return all(state[i][0] == p for i, p in bad)

def shortest_counterexample(protocol, bad, max_k):
    for k in range(max_k + 1):
        V, cnf = encode(protocol, k, bad)
        model = dpll(cnf)
        if model is not None:
            trace = decode(V, model, k)
            assert replay(protocol, trace, bad)
            return k, trace
    return None

Worked example: a race and a deadlock

Protocol one, check-then-set, looks at the other flag, then raises its own and enters. With the bad state "both in crit", runs of k = 0 to 3 were UNSAT. At k = 4 the formula, with 44 variables and 198 clauses, was SAT, and the decoded trace replayed cleanly:

This is the classic race: both processes check before either one sets. Because k grows from 0, the first trace found is a shortest counterexample, which is the easiest kind to debug. Formula size grows linearly in k: 8 variables and 14 clauses at k = 0, and 9 variables and 46 clauses more per step.

Protocol two, set-then-check, raises its flag first. With "both in crit" as the bad state, all 13 runs from k = 0 to k = 12 were UNSAT, which took under half a minute with the toy DPLL. Swap in one more property, "both in mid", and it is SAT at k = 2. Each process raises its flag, then spins forever waiting for the other. That is a deadlock: the state never changes again, found with the same encoder by changing one line. An explicit-state breadth-first search of both protocols agreed with every result: check-then-set has 9 reachable states and first reaches "both in crit" at depth 4, and set-then-check has 8 reachable states, all within depth 3.

From bounded answers to proofs

UNSAT at k says "no bad run of exactly k steps", not "safe". Bounded results become proofs in two standard ways. The first is a completeness threshold. If every reachable state is reachable within d steps (the diameter), then UNSAT for every k up to d proves safety. For set-then-check, breadth-first search shows d = 3, so the UNSAT runs up to 12 prove mutual exclusion for this model. Computing d is as hard as the original problem in general, so this only works when you can bound it some other way.

The second is induction. k-induction (Sheeran, Singh and Stalmarck, 2000) also asks the solver whether any k consecutive good states can be followed by a bad one. If that is UNSAT too, safety holds for all lengths. IC3/PDR (Bradley, 2011) learns inductive invariants clause by clause. Production model checkers combine all three.

Operational guidance

• Keep a variable map. Vars records every name for every integer. Without it, an UNSAT core or a model is unreadable, and you will debug the encoding blind.
• Test the encoder against brute force on small instances. Enumerate states, or every assignment, for k up to 3 and compare. Most encoding bugs show up at tiny sizes.
• Use incremental solving for growing bounds. Real solvers accept assumptions, so you can add the step-k clauses and assert the bad-state literals only as assumptions, rather than re-encoding from scratch.
• Track formula size per instance (variables, clauses and literals). Size blow-ups, usually from pairwise at-most-one constraints on big domains, show up here before they show up as timeouts.
• Set time limits and treat UNKNOWN as its own outcome, distinct from UNSAT. A timeout that is reported as "safe" is the worst bug a pipeline like this can have.

Failure modes

• Missing frame axioms: drop the "other process is frozen" clauses and the solver will teleport the idle process into crit. That produces spurious counterexamples, and the replay check catches them.
• Over-constraining: an accidental extra clause removes real behaviours and turns bugs into UNSAT. Replay cannot catch this, because there is no trace to replay. Only brute-force comparison and deliberately seeded bugs can.
• Non-total or non-deterministic tables: the encoder asserts that every (pc, flag) pair has exactly one command, because a missing pair would silently become a deadlock.
• Reading UNSAT at k as a proof: see the previous section. State the bound in every report.

What to do next

1. Run shortest_counterexample(CHECK_THEN_SET, [(0, "crit"), (1, "crit")], 12) and confirm that it finds the 4-step race.
2. Add a DIMACS writer and solve the same formulas with CaDiCaL or Kissat, then compare the models after decoding.
3. Encode Peterson's algorithm, which adds a turn variable, and show UNSAT for both properties up to its diameter.
4. Seed a bug in the encoder (delete one frame clause) and check that replay rejects the trace it produces.
5. Pick one constraint problem from your own work, write its specification table first, and only then write the encoder.
6. Read the SAT solving deep dive for Tseitin, cardinality encodings and how CDCL behaves on formulas like these.