Skip to content

PicoSAT

A small SAT solver.

https://fmv.jku.at/picosat

The DIMACS Format

Standard input format for SAT solvers.

c This is a comment
p cnf [#variables] [#clauses]
-1 -2 0 [Each clause ends with 0]
-1 3 0 [negation -]
......

One line for each clause

Negate literals are negative

Each line is terminated by 0

Certified UNSAT

If a formula is UNSAT, most solver can produce a certificate.

A SAT instance is UNSAT if no total assignment satisfies all clauses.

UNSAT Cores

A UNSAT core is a subset of the original clauses that is itself UNSAT. If the original formula \(F\) is UNSAT, and \(S\) is a subset of \(F\) that is UNSAT, then \(S\) is an UNSAT core of \(F\).

Applications:

  • Counterexample-guided refinement
  • Debugging
  • Model checking

Definition:

  • Minimal core: removing any clause makes it SAT
  • Minimum core: smallest minimal core

Properties:

  • Finding a minimal core is easy
  • Finding the minimum core is NP-hard

CDCL gives non-minimal cores by default.

A Example In Practice

Given a SAT formula

p cnf 5 6
1 2 0 #line 1
-1 2 0 #line 2
-2 3 0 #line 3
-2 -3 0 #line 4
4 -4 0 #line 5
5 0 #line 6

The UNSAT core trace:

1 1 2 0 0
2 -1 2 0 0
3 -2 3 0 0
4 -2 -3 0 0
7 -2 0 3 4 0
8 -1 0 7 2 0
9 0 7 1 8 0

From line 1 to 4, they are clauses from SAT formula.

Line 7 shows that line 3 and 4 derive -2

Line 8 shows that line 7 and 2 derive -1

Line 9 shows that line 7, 1, and 8 derive a conflict.

Application of SAT solver

Sudoku 9×9 (can be extended to arbitrarily n×n)

We encode the puzzle into SAT formula, where each variable \(x_{ijk}\) represents put number \(k\) on position \((i,j)\).

For each line, each row, and each 3 by 3 cell, we have constraints as clauses.

Each number already on the table is encoded to a clause with a single variable.