DPLL in Prolog

Logic programming was built for this. Unification searches the space; backtracking is free.

01

Represent a clause as a list of literals — positive literals are atoms, negative literals are wrapped in not/1. The whole formula is a list of clauses.
```
% (a ∨ ¬b) ∧ (b ∨ c) ∧ (¬a ∨ ¬c)
formula([[a, not(b)], [b, c], [not(a), not(c)]]).
```
02

A literal is satisfied if its variable is bound to the right value in the assignment list. Member/2 walks the assignment until it finds a match — or fails, triggering backtracking.
```
sat_lit(not(V), A) :- member(V=false, A), !.
sat_lit(V, A)      :- atom(V), member(V=true, A), !.

clause_sat(C, A) :- member(L, C), sat_lit(L, A).
```
03

DPLL — pick an unbound variable, try true, then false. The disjunction (;)/2 hands the second branch to Prolog's backtracker for free; we only describe the relation, not the procedure.
```
dpll([], _).
dpll(Cs, A) :-
  pick_var(Cs, A, V),
  ( solve(Cs, [V=true |A])
  ; solve(Cs, [V=false|A]) ).

solve(Cs, A) :- maplist([C]>>clause_sat(C,A), Cs).
```
04

Run it. SWI-Prolog returns the first satisfying assignment, or false if the formula is UNSAT. The whole solver is twenty lines because the language is a backtracking search engine — you write the spec; the runtime does the searching.
```
?- formula(F), dpll(F, A).
A = [a=true, b=false, c=true].
```

Grammar — Prolog

Prolog is a database of facts and rules, plus an engine that takes a query and searches for variable bindings that make the query true. The conventions below cover almost everything on the previous page.

a, b, true: an atom — a lowercase identifier, treated as a constant symbol.
V, A, Cs: a variable — capitalized or starts with underscore. First mention binds; later mentions must match.
not(V): a compound term: a functor named "not" wrapping its argument. Prolog gives it no special meaning — we use it as a tag for "negated literal."
[a, b, c]: a list, the universal collection. `[H|T]` pattern-matches head and tail.
:-: "is true if" — separates the head of a rule from its body.
,: AND between goals in a body. Every goal must succeed.
;: OR between alternatives. Try the first; on failure, try the second.
!: cut. Commits to the current branch and disables backtracking past it.
?- Goal.: a query. Ask the engine to find a substitution making Goal true.

Now take the SAT clause (a ∨ ¬b) — "a or not b." Prolog has no infix ∨ or ¬, so we encode the clause as a list of literals: positive literals are atoms, negative literals get wrapped in not/1. The list itself doesn't perform the OR — the OR happens when we walk the list, succeeding the moment any literal in it is satisfied.

% the clause (a ∨ ¬b), encoded:
Clause = [a, not(b)].

% disjunction is realized by member/2 picking any element:
?- member(L, [a, not(b)]).
L = a ;          % first solution
L = not(b).      % on backtracking, the next one

% so "is some literal in this clause true?" reads:
clause_sat(C, A) :- member(L, C), sat_lit(L, A).

SWISH — try Prolog in your browser →