Skip to content
Snippets Groups Projects
Commit d81c4d18 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

update notebook 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent ac48bfc7
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
logic_programming/4_DPLL.ipynb
+ 148
− 50
View file @ d81c4d18
%% Cell type:markdown id:9eb5530a tags:
# DPLL SAT Solving as a Prolog program
We take again our Knights and Knaves puzzle from Raymond Smullyan.
- A says: “B is a knave or C is a knave”
- B says: “A is a knight”
We can convert our Knights and Knaves puzzle to conjunctive normal form (CNF):
```
(A ⇔ ¬B ∨ ¬C) ∧ (B ⇔ A)
(A → ¬B ∨ ¬C) ∧ (¬B ∨ ¬C → A) ∧ (B → A)∧ (A → B)
(¬A ∨ ¬B ∨ ¬C) ∧ (¬(¬B ∨ ¬C) ∨ A) ∧ (¬B ∨ A)∧ (¬A ∨ B)
(¬A ∨ ¬B ∨ ¬C) ∧ ((B ∧ C) ∨ A) ∧ (¬B ∨ A)∧ (¬A ∨ B)
(¬A ∨ ¬B ∨ ¬C) ∧ (B ∨ A) ∧ (C ∨ A) ∧(¬B ∨ A)∧ (¬A ∨ B)
{¬A ∨ ¬B ∨ ¬C, B ∨ A, C ∨ A, ¬B ∨ A, ¬A ∨ B}
```
One can encode a clause as a set of literals, and one can encode the CNF as a set of clauses.
Implicitly, the literals in clause are disjoined, while all the clauses in a CNF are conjoined.
In Prolog, we can represent sets using lists.
Below is an encoding of the CNF as a list of lists.
For example, the clause ```¬A ∨ ¬B ∨ ¬C``` is represented as the list ```[neg(a),neg(b),neg(c)]```.
Every literal is of either the form ```neg(p)``` or ```pos(p)``` with ```p``` being a proposition.
%% Cell type:code id:964ebd52 tags:
``` prolog
:- discontiguous problem/3.
:- dynamic problem/3.
problem(1,'Knights & Knaves',
[ [neg(a),neg(b),neg(c)],
[pos(b),pos(a)],
[pos(c),pos(a)],
[neg(b),pos(a)],
[neg(a),pos(b)] ]).
negate(pos(A),neg(A)).
negate(neg(A),pos(A)).
```
%% Cell type:markdown id:a4dc903e tags:
We can negate literals as follows:
%% Cell type:code id:26e0221b tags:
``` prolog
?- negate(pos(a),NA), negate(neg(b),NB).
```
%% Output
%% Cell type:markdown id:fc6823ad tags:
We now show to perform resolution of two clauses.
First we can pick two clauses simply using ```member```:
%% Cell type:code id:152289b6 tags:
``` prolog
?- problem(1,_,Clauses),
member(C1,Clauses), member(Lit1,C1).
```
%% Output
%% Cell type:markdown id:68fd6059 tags:
We can now pick matching literals with opposing polarity as follows:
%% Cell type:code id:2c3dd1bf tags:
``` prolog
?- problem(1,_,Clauses),
member(C1,Clauses), member(Lit1,C1), negate(Lit1,Lit2),
member(C2,Clauses), member(Lit2,C2).
%comment.
```
%% Output
%% Cell type:markdown id:07785e91 tags:
We can now implement resolution of two particular clauses as follows:
%% Cell type:code id:33fc6271 tags:
``` prolog
:- use_module(library(lists)).
resolve(Clause1,Clause2,Resolvent) :-
select(Lit1,Clause1,R1), negate(Lit1,NLit1),
select(NLit1,Clause2,R2),
append(R1,R2,Resolvent).
```
%% Cell type:markdown id:1d426bb1 tags:
The above predicate uses the predicate ```select/3``` from ```library(lists)```, which can be used to select an element from a list and returns a modified list with the element removed:
%% Cell type:code id:f2a8b4a4 tags:
``` prolog
?- select(2,[1,2,3],Res1).
```
%% Output
%% Cell type:markdown id:cba18c66 tags:
The predicate ```resolve``` works as follows:
%% Cell type:code id:06aa608c tags:
``` prolog
?- resolve([neg(a),pos(b)],[neg(b),pos(c)],Resolvent).
```
%% Output
%% Cell type:code id:a76d8b5d tags:
``` prolog
?- resolve([pos(b)],[neg(b)],Resolvent).
```
%% Output
%% Cell type:code id:d7a0cc62 tags:
``` prolog
?- resolve([neg(a),neg(b)],[neg(b),pos(c)],Resolvent).
```
%% Output
%% Cell type:markdown id:2b2ea192 tags:
Let us now resolve two clauses from our puzzle:
%% Cell type:code id:78163b60 tags:
``` prolog
?- problem(1,_,Clauses),
member(C1,Clauses), member(C2,Clauses),
resolve(C1,C2,NewClause).
```
%% Output
%% Cell type:markdown id:a70dbafb tags:
Let us compute all direct resolvents:
%% Cell type:code id:9d3fbd1a tags:
``` prolog
?- problem(1,_,Clauses),
findall(NewClause,(member(C1,Clauses), member(C2,Clauses),
resolve(C1,C2,NewClause)
), NewClauses),
length(NewClauses,NrNew),
sort(NewClauses,SortedC), length(SortedC,NrNewUnique).
```
%% Output
%% Cell type:markdown id:6cdeade5 tags:
As you can see, the number of new clauses can grow considerably when applying resolution.
Below we study the DPLL algorithm to check satisfiability of a formula in CNF, using a simple form of resolution (where one clause is a single literal and the other clauses comes from the CNF of the problem).
%% Cell type:markdown id:d32921c9 tags:
### DPLL Algorithm
We now present bit by bit the DPLL algorithm as a Prolog program
manipulating the above clause database.
The algorithm works by selecting a literal and then making it true and checking whether this leads to a solution.
If not, the algorithm backtracks and makes the negated version of the literal true and tries to find a solution.
%% Cell type:code id:26924712 tags:
``` prolog
becomes_true(TrueLit,Clause) :-
member(TrueLit,Clause).
```
%% Cell type:markdown id:17dd1525 tags:
The above checks if making a given literal true makes the second argument, a clause, true (i.e., the clause is satisfied):
%% Cell type:code id:7d90c4ad tags:
``` prolog
?- becomes_true(pos(b),[neg(a),pos(b)]).
```
%% Output
%% Cell type:code id:d4b4e71f tags:
``` prolog
?- becomes_true(neg(a),[neg(a),pos(b)]).
```
%% Output
%% Cell type:markdown id:62e13b8d tags:
The code below simplifies a clause given a literal ```TrueLit``` that has just become true.
This is done using resolution:
%% Cell type:code id:3b9c87e4 tags:
``` prolog
simplify(TrueLit,Clause,SimplifedClause) :-
negate(TrueLit,FalseLit),
delete(Clause,FalseLit,SimplifedClause). % Resolution with TrueLit if possible
```
%% Cell type:markdown id:e8cee74e tags:
The code uses the ```delete/3``` predicate from ```library(lists)```. Unlike select it also succeeds when the element is not in the list:
%% Cell type:code id:0abd90f6 tags:
``` prolog
?- delete([a,b,c],d,R).
```
%% Output
%% Cell type:code id:cc81b404 tags:
``` prolog
?- delete([a,b,c],a,R).
```
%% Output
%% Cell type:markdown id:53d21e85 tags:
The above code simplifies a clause by resolution:
%% Cell type:code id:57df05f0 tags:
``` prolog
?- simplify(pos(c),[pos(a),neg(c)],SC).
```
%% Output
%% Cell type:markdown id:4c3eae55 tags:
If no resolution is possible the clause is returned unchanged:
%% Cell type:code id:a36a54a4 tags:
``` prolog
?- simplify(pos(b),[pos(a),neg(c)],SC).
```
%% Output
%% Cell type:markdown id:441c4145 tags:
We can now define the whole procedure to set a literal ```Lit``` to true (```Clauses|{Lit}```) by
- removing all clauses which have become true (and no longer need to be checked)
- simplifying the remaining clauses with resolution if possible.
%% Cell type:code id:95fcf64b tags:
``` prolog
set_literal(Lit,Clauses,NewClauses) :-
exclude(becomes_true(Lit),Clauses,Clauses2),
maplist(simplify(Lit),Clauses2,NewClauses).
```
%% Cell type:markdown id:f0a8731d tags:
The predicate ```exclude/3``` from ```library(lists)``` is a higher-order predicate. It maps its first argument (a predicate) over the second argument (a list) and excludes all elements where the predicate succeeds.
%% Cell type:code id:9c35b0b3 tags:
``` prolog
?- exclude(becomes_true(pos(a)), [[neg(b)], [pos(a),pos(c)]],R).
```
%% Output
%% Cell type:markdown id:1b1f2fe8 tags:
```exclude``` will perform these two calls and hence remove the second clause and keep the first one:
%% Cell type:code id:56175b0d tags:
``` prolog
?- becomes_true(pos(a),[neg(b)]).
?- becomes_true(pos(a),[pos(a),pos(c)]).
```
%% Output
%% Cell type:markdown id:52063b72 tags:
The predicate ```maplist/3``` from ```library(lists)``` is another higher-order predicate. It maps its first argument (a predicate) over the elements in the second and third arguments (both lists).
%% Cell type:code id:8259d2d7 tags:
``` prolog
?- maplist(simplify(neg(c)), [[neg(b),pos(c)], [pos(a),pos(c)]],R).
```
%% Output
%% Cell type:markdown id:44d0ef2e tags:
```maplist``` will perform these two calls and put ```R1``` and ```R2``` into the result list ```R``` above:
%% Cell type:code id:9e0d83d0 tags:
``` prolog
?- simplify(neg(c),[neg(b),pos(c)],R1),
simplify(neg(c),[pos(a),pos(c)],R2).
```
%% Output
%% Cell type:markdown id:007b118b tags:
The predicate ```set_literal``` can now be called as follows:
%% Cell type:code id:25b19d82 tags:
``` prolog
?- set_literal(pos(a),[[neg(a),neg(b),neg(c)]],Res).
```
%% Output
%% Cell type:code id:75a52c4f tags:
``` prolog
?- set_literal(neg(a),[[neg(a),neg(b),neg(c)]],Res).
```
%% Output
%% Cell type:markdown id:04b0de71 tags:
In the call above we have found a model: all clauses have been satisfied.
In the next call we have found a contradiction, as the resulting list contains the empty clause (aka the obvious contradiction).
%% Cell type:code id:d8876a92 tags:
``` prolog
?- set_literal(neg(a),[[neg(a),neg(b),neg(c)],[pos(a)]],Res).
```
%% Output
%% Cell type:markdown id:ee321f62 tags:
Let us now use this code on our puzzle:
%% Cell type:code id:5535384f tags:
``` prolog
?- problem(1,T,C1), set_literal(pos(a),C1,C2).
```
%% Output
%% Cell type:code id:592fcdd9 tags:
``` prolog
?- problem(1,_,C1), set_literal(pos(a),C1,C2), set_literal(pos(b),C2,C3).
```
%% Output
%% Cell type:markdown id:800c4415 tags:
This is now the top-level of the DPLL algorithm.
It first tries to find unit clauses, to deterministically find forced assignments.
It then checks if all clauses have now been satisfied.
If not, it checks for inconsistency.
If there is no inconsistency, then a literal is chosen and forced to one and then if required the other value.
%% Cell type:code id:b8cabba2 tags:
``` prolog
dpll(Clauses,[unit(Lit)|Stack]) :-
select([Lit],Clauses,Clauses2), % unit clause found
set_literal(Lit,Clauses2,Clauses3),
dpll(Clauses3,Stack).
dpll([],Stack) :- !, Stack=[]. % SAT
dpll(Clauses,[branch(Lit)|Stack]) :-
\+ member([],Clauses), % no inconsistency
choose_literal(Clauses,Lit), % this selects one literal and returns it first in original then in negated form
set_literal(Lit,Clauses,Clauses2),
dpll(Clauses2,Stack).
choose_literal([ [Lit|_] | _], Lit).
choose_literal([ [Lit|_] | _], NegLit) :-
negate(Lit,NegLit).
```
%% Cell type:code id:e369355c tags:
``` prolog
?- problem(1,_,C1), dpll(C1,Stack).
```
%% Output
%% Cell type:code id:78764141 tags:
``` prolog
test(Nr) :- problem(Nr,Str,Clauses),
format('Solving problem ~w : ~w~n',[Nr,Str]),
(dpll(Clauses,Stack)
-> format('SAT: Model found: ~w~n',[Stack])
; format('UNSAT: no model exists',[])).
```
%% Cell type:code id:c51455cf tags:
``` prolog
?- test(1).
```
%% Output
%% Cell type:code id:b0466a5d tags:
``` prolog
problem(2,'Knights & Knaves (Proof by contradiction)',
[ [neg(a),neg(b),neg(c)],
[pos(b),pos(a)],
[pos(c),pos(a)],
[neg(b),pos(a)],
[neg(a),pos(b)],
[neg(a),neg(b),pos(c)] ]). % <--- negated Query
problem(3,'Princess & Tiger',
[[pos(t1),pos(z2),neg(t1)],
[pos(t1),neg(z2)],
[neg(t1),neg(z2)],
[pos(t1),pos(z1),neg(t2)],
[pos(t2),neg(z1)],
[neg(t1),neg(z1)],
[pos(z1),pos(z2)],
[neg(z1),neg(z2)]]).
```
%% Cell type:code id:2df16148 tags:
``` prolog
?- test(2).
```
%% Output
%% Cell type:code id:8d8cf76a tags:
``` prolog
?- test(3).
```
%% Output
%% Cell type:code id:31d1b945 tags:
``` prolog
problem(4,'uf-20-02',
[[ neg(x10) , neg(x16) , pos(x5) ] ,
[ pos(x16) , neg(x6) , pos(x5) ] ,
[ neg(x17) , neg(x14) , neg(x18) ] ,
[ neg(x10) , neg(x15) , pos(x19) ] ,
[ neg(x1) , neg(x9) , neg(x18) ] ,
[ pos(x3) , pos(x7) , neg(x6) ] ,
[ neg(x13) , pos(x1) , pos(x6) ] ,
[ neg(x2) , neg(x16) , neg(x20) ] ,
[ pos(x7) , pos(x8) , pos(x18) ] ,
[ neg(x7) , pos(x10) , neg(x20) ] ,
[ pos(x2) , neg(x14) , neg(x17) ] ,
[ pos(x2) , pos(x1) , pos(x19) ] ,
[ pos(x7) , neg(x20) , neg(x1) ] ,
[ neg(x11) , pos(x1) , neg(x17) ] ,
[ pos(x3) , neg(x12) , pos(x19) ] ,
[ neg(x3) , neg(x13) , pos(x6) ] ,
[ neg(x13) , pos(x3) , neg(x12) ] ,
[ pos(x5) , neg(x7) , neg(x12) ] ,
[ pos(x20) , pos(x8) , neg(x16) ] ,
[ neg(x13) , neg(x6) , pos(x19) ] ,
[ neg(x5) , pos(x1) , pos(x14) ] ,
[ pos(x9) , neg(x5) , pos(x18) ] ,
[ neg(x12) , neg(x17) , neg(x1) ] ,
[ neg(x20) , neg(x16) , pos(x19) ] ,
[ pos(x12) , pos(x10) , neg(x11) ] ,
[ pos(x6) , neg(x7) , neg(x2) ] ,
[ pos(x13) , neg(x10) , pos(x17) ] ,
[ neg(x20) , pos(x8) , neg(x16) ] ,
[ neg(x10) , neg(x1) , neg(x8) ] ,
[ neg(x7) , neg(x3) , pos(x19) ] ,
[ pos(x19) , neg(x1) , neg(x6) ] ,
[ pos(x19) , neg(x2) , pos(x13) ] ,
[ neg(x2) , pos(x20) , neg(x9) ] ,
[ neg(x8) , neg(x20) , pos(x16) ] ,
[ neg(x13) , neg(x1) , pos(x11) ] ,
[ pos(x15) , neg(x12) , neg(x6) ] ,
[ neg(x17) , neg(x19) , pos(x9) ] ,
[ pos(x19) , neg(x18) , pos(x16) ] ,
[ pos(x7) , neg(x8) , neg(x19) ] ,
[ neg(x3) , neg(x7) , neg(x1) ] ,
[ pos(x7) , neg(x17) , neg(x16) ] ,
[ neg(x2) , neg(x14) , pos(x1) ] ,
[ neg(x18) , neg(x10) , neg(x8) ] ,
[ neg(x16) , pos(x5) , pos(x8) ] ,
[ pos(x4) , pos(x8) , pos(x10) ] ,
[ neg(x20) , neg(x11) , neg(x19) ] ,
[ pos(x8) , neg(x16) , neg(x6) ] ,
[ pos(x18) , pos(x12) , pos(x8) ] ,
[ neg(x5) , neg(x20) , neg(x10) ] ,
[ pos(x16) , pos(x17) , pos(x3) ] ,
[ pos(x7) , neg(x1) , neg(x17) ] ,
[ pos(x17) , neg(x4) , pos(x7) ] ,
[ pos(x20) , neg(x9) , neg(x13) ] ,
[ pos(x13) , pos(x18) , pos(x16) ] ,
[ neg(x16) , neg(x6) , pos(x5) ] ,
[ pos(x5) , pos(x17) , pos(x7) ] ,
[ neg(x12) , neg(x17) , neg(x6) ] ,
[ neg(x20) , pos(x19) , neg(x5) ] ,
[ pos(x9) , neg(x19) , pos(x16) ] ,
[ neg(x13) , neg(x16) , pos(x11) ] ,
[ neg(x4) , neg(x19) , neg(x18) ] ,
[ neg(x13) , pos(x10) , neg(x15) ] ,
[ pos(x16) , neg(x7) , neg(x14) ] ,
[ neg(x19) , neg(x7) , neg(x18) ] ,
[ neg(x20) , pos(x5) , pos(x13) ] ,
[ pos(x12) , neg(x6) , pos(x4) ] ,
[ pos(x7) , pos(x9) , neg(x13) ] ,
[ pos(x16) , pos(x3) , pos(x7) ] ,
[ pos(x9) , neg(x1) , pos(x12) ] ,
[ neg(x3) , pos(x14) , pos(x7) ] ,
[ pos(x1) , pos(x15) , pos(x14) ] ,
[ neg(x8) , neg(x11) , pos(x18) ] ,
[ pos(x19) , neg(x9) , pos(x7) ] ,
[ neg(x10) , pos(x6) , pos(x2) ] ,
[ pos(x14) , pos(x18) , neg(x11) ] ,
[ neg(x9) , neg(x16) , pos(x14) ] ,
[ pos(x1) , pos(x11) , neg(x20) ] ,
[ pos(x11) , pos(x12) , neg(x4) ] ,
[ pos(x13) , neg(x11) , neg(x14) ] ,
[ pos(x17) , neg(x12) , pos(x9) ] ,
[ pos(x14) , pos(x9) , pos(x1) ] ,
[ pos(x8) , pos(x19) , pos(x4) ] ,
[ pos(x6) , neg(x13) , neg(x20) ] ,
[ neg(x2) , neg(x13) , pos(x11) ] ,
[ pos(x14) , neg(x13) , pos(x17) ] ,
[ pos(x9) , neg(x11) , pos(x18) ] ,
[ neg(x13) , neg(x6) , pos(x5) ] ,
[ pos(x5) , pos(x19) , neg(x18) ] ,
[ neg(x4) , pos(x10) , pos(x11) ] ,
[ neg(x18) , neg(x19) , neg(x20) ] ,
[ pos(x3) , neg(x9) , pos(x8) ]
]).
problem(5,'schaltung_a1.pl',
[
%a. not_b. c. not_d. e.
[pos(a)], [neg(b)], [pos(c)], [neg(d)], [pos(e)],
% Schaltungen der ersten Ebene
%and11 :- a,b.
[pos(and11),neg(a),neg(b)],
%or11 :- b.
[pos(or11),neg(b)],
%or11 :- c.
[pos(or11),neg(b)],
%and12 :- c,d.
[pos(and12),neg(c),neg(d)],
%not1 :- not_e.
[pos(not1),pos(e)],
% Schaltungen der zweiten Ebene
%or21 :- and11.
[pos(or21),neg(and11)],
%or21 :- not1.
[pos(or21),neg(not1)],
%and2 :- or11, not1.
[pos(and2),neg(or11),neg(not1)],
%or22 :- and12.
[pos(or22),neg(and12)],
%or22 :- not1.
[pos(or22),neg(not1)],
%not2 :- e. % \+ not1.
[pos(not2),neg(e)],
% Schaltungen der dritten Ebene
%and3 :- or21, and2.
[pos(and3),neg(or21),neg(and2)],
%or3 :- or22.
[pos(or3),neg(or22)],
%or3 :- not2.
[pos(or3),neg(not2)],
% Schaltungen der vierten Ebene
%or4 :- and3.
[pos(or4),neg(and3)],
%or4 :- or3.
[pos(or4),neg(or3)],
%and4 :- or3, not2.
[pos(and4),neg(or3),neg(not2)],
% Letzte Ebene
%and5 :- and4, or4.
[pos(and5),neg(and4),neg(or4)],
%output :- and5.
[pos(output),neg(and5)],
% ?- output.
[neg(output)]
]).
problem(6, 'doodle-wo-max1-constraint',
[
[pos(x1),pos(x3)],
[neg(x3)],
[neg(x5)],
[pos(x4),pos(x5)]
]).
problem(7, 'doodle-with-max1-constraint',
[
[pos(x1),pos(x3)],
[neg(x3)],
[neg(x5)],
[pos(x4),pos(x5)],
[neg(x1),neg(x2)], [neg(x1),neg(x3)], [neg(x1),neg(x4)],
[neg(x1),neg(x5)],
[neg(x2),neg(x3)], [neg(x2),neg(x4)],[neg(x2),neg(x5)],
[neg(x3),neg(x4)],[neg(x3),neg(x5)],
[neg(x4),neg(x5)]
]).
```
%% Cell type:code id:c51f1ce6 tags:
``` prolog
?- test(4).
```
%% Output
%% Cell type:code id:39bb01e4 tags:
``` prolog
?-test(2).
```
%% Output
%% Cell type:markdown id:d3ec741b tags:
Below we show another version of the DPLL algorithm which returns the full decision tree.
It is for education purposes, e.g., to visualise the choices made by the algorithm:
%% Cell type:code id:062d6089 tags:
``` prolog
jupyter:version.
dpll_tree(Clauses,unit(Lit,Tree),Res) :-
select([Lit],Clauses,Clauses2), % unit clause found
!,
set_literal(Lit,Clauses2,Clauses3),
dpll_tree(Clauses3,Tree,Res).
dpll_tree([],Tree,Res) :- !, Tree=[], Res=sat. % SAT
dpll_tree(Clauses,Tree,Res) :- member([],Clauses),!, Tree=unsat,Res=unsat.
dpll_tree(Clauses,branch(Lit,TreePos,TreeNeg),Res) :-
choose_literal(Clauses,Lit),
!,
set_literal(Lit,Clauses,Clauses1),
dpll_tree(Clauses1,TreePos,Res1),
(Res1=sat
-> TreeNeg=unexplored, Res=sat
; negate(Lit,NegLit),
set_literal(NegLit,Clauses,Clauses2),
dpll_tree(Clauses2,TreeNeg,Res)
).
```
%% Cell type:code id:03d3fe70 tags:
``` prolog
?- problem(1,Str,Clauses), dpll_tree(Clauses,Tree,Res).
```
%% Output
%% Cell type:code id:5c82bfa1 tags:
%% Cell type:code id:03d3fe70 tags:
``` prolog
?- print($Tree),nl.
```
%% Output
%% Cell type:code id:d614588e tags:
``` prolog
jupyter:version(A,B,C,D)
show_term($Tree)
```
%% Output
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment