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.

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