## [MiniSat] An Extensible SAT-solver

SAT

MiniSat allows to construct your own solver in a very short time.

1 Main feature of MiniSat—extensibility. In 2002 they have implemented Satzoo and Satnik. MiniSat is based on the ideas of *conflict-driven backtracking*, *watched literals*, and *dynamic variable ordering*. 2 MiniSat is actually minimal SAT-solver with useful API (< 600 lines of C++ code). It includes an **incremental** SAT interface. 3 You can provide *assumptions* (set of literals that is true) to `solve()` method to get “SAT” or “UNSAT under assumptions”.

Conflict-driven SAT-solver: based on DPLL, backtracking by conflict analysis and clause recording (learning) [GRASP], Boolean constraint propagation using watched literals [Chaff].

Search: 4 make assumptions (heuristically, pick variables and assign values). Can we offer better assumptions based on high-level structures? MiniSat is extensible for *arbitrary constraints*.

Propagation. Clause: (*x* ∨ *y* ∨ *z*), unit clause: (*x*). Watcher queue: for each literal, a list of constraints (which *may* propagate unit information if literal becomes true) is kept. On backtracking, no adjustment to the watcher lists need to be done.

Learning: when a constraint becomes conflicting under current assignment, learning starts. As result, we get *learned clause* (set of variables that implies the confilict).

5 Search. It is a recursive procedure, but typically implemented iteratively: select unassigned variable *x* (decision variable), assume a value. Stack of assignments reffered to as trail. If the clause remains unit for several decision levels, it is advantageous to chose the lowest level (backjumping [GRASP]). 6 An important part of the procedure is the heuristic for `decide()`. Like Chaff, MiniSat uses dynamic variable order: priority to varialbes involved in recent conflicts. Variable ordering is a traditional target for improving SAT-solvers. Optimizations.

Each variable has an activity attached to it. Bumping: increasing activity when a variable occurs in a recorded conflict clause. Decaying: multiply activity of all the variables by a constant less than 1. MiniSat uses the same idea for clauses.

The constraint database is divided into two parts: the problem constraints and the learnt clauses. For performance, learned clauses can be periodically reduced.

### Implementation

8 MiniSat can handle arbitrary constraints over boolean variables. 10 Class `Constr` is an arbitrary constraint (not only clause). It is interface that must implement `remove()`, `propagate()`, `simplify()`, `undo()`, and `calcReason()` functions. They said, SAT-solver spends about 80 % of the time propagating. Can we use this fact? The propagation routine keeps propagation queue (a set of literals that is to be propagated). 11 `Clause` is a subclass of `Constr`. `Clause` has fields: `bool learnt`, `float activity`, and `Vec<lit> lits`.

13 Conflict-driven clause learning [GRASP]. Example. DB contains clause {*x*, *y*, *z*}: (*x* ∨ *y* ∨ *z*). It became usatisfied during propagation. This is a conflict. (¬*x* ∧ ¬*y* ∧ ¬*z*) is the reason of the conflict. We ask `calcReason()` for propagating ¬*x*. If result is (*u* ∧ ¬*v*) (what had implied ¬*x*), the learn conflict clause is {¬*u*, ¬*v*, *y*, *z*}.

14 In the terms of MiniSat, fact is a litera with reason.

Is there parallelization?

23 pages

Sergey Vartanov, 2007–2020