Boolean satisfiability (SAT) asks whether some assignment of true and false to variables makes a formula true. This example writes the classic DPLL search in a few dozen lines of Prolog: assign a variable, prune as soon as a clause becomes impossible, and keep going.
Run it in the playground · Source
The formula is in conjunctive normal form (CNF): a list of clauses, each an “or” of literals, all of which must hold.
(a or b) (not a or c) (not b or c) (not c or d) (c or not d)
Four variables give 16 possible assignments. Which of them satisfy every clause, and can the search avoid looking at all 16?
variable_order([a, b, c, d]).
cnf_clause(c1, [pos(a), pos(b)]).
cnf_clause(c2, [neg(a), pos(c)]).
cnf_clause(c3, [neg(b), pos(c)]).
cnf_clause(c4, [neg(c), pos(d)]).
cnf_clause(c5, [pos(c), neg(d)]).
A literal is pos(Var) or neg(Var). A (partial) assignment is a list of
bind(Name, Bool) terms.
clause_impossible(Assignment, Clause_name) :-
cnf_clause(Clause_name, Literals),
\+ nonfalse_literal(Literals, Assignment).
dpll([], Assignment, Assignment) :- complete_model(Assignment).
dpll([Var | Rest], Partial, Model) :-
bool(Value),
partial_consistent([bind(Var, Value) | Partial]),
dpll(Rest, [bind(Var, Value) | Partial], Model).
A clause is impossible when every one of its literals is already false; an
unassigned literal keeps it alive. dpll/3 tries false, then true, for
each variable and abandons a branch the moment some clause becomes impossible.
That early pruning is the heart of DPLL.
eyeprolog examples/sat-solver-dpll.pl
satModel([bind(d, true), bind(c, true), bind(b, true), bind(a, false)]).
satValue(d, true).
satValue(c, true).
satValue(b, true).
satValue(a, false).
satClauseStatus(c1, satisfied).
Eleven answers in all: the model, its four values, the status of all five
clauses, and a one-line conclusion. The formula has three models (c and d
must be true, and at least one of a, b); aggregate_min/5 picks the one
with the smallest binary rank so the output is deterministic.
step(best_model([bind(d, true), bind(c, true), bind(b, true), bind(a, false)], 7),
rule(28),
['Model' = [bind(d, true), bind(c, true), bind(b, true), bind(a, false)], 'Rank' = 7],
[aggregate_min(Key, Value, (satisfying_model(Value), model_rank(Value, Key)), 7, [bind(d, true), bind(c, true), bind(b, true), bind(a, false)])]).
The chosen model has rank 7 (binary 0111 for a, b, c, d), and it is
the minimum over all satisfying models found by satisfying_model/1.
condition('C1', resolution, ok, 36).
condition('C5', re_decision, ok, 5).
obligation(builtin, theory_scoped, aggregate_min(A, B, (satisfying_model(B), model_rank(B, A)), 7, [bind(d, true), bind(c, true), bind(b, true), bind(a, false)])).
verdict(checked_with_obligations).
36 steps replay against the program and 5 library calls are recomputed. One step cannot be: “7 is the minimum rank” depends on every model the program could produce, and the checker never searches. It records that claim as an obligation, and the verdict says the proof holds given it.
cnf_clause(c6, [neg(b)]). The only model left is a true, b false,
c and d true.cnf_clause(c6, [neg(c)]). instead. The formula becomes unsatisfiable,
and the run prints nothing at all. Why is that the right outcome?variable_order/1 to [d, c, b, a]. Does the answer change? Does the
amount of search?Learn more in The Art of EyeProlog, Chapter 24.