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

improve notebook 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent 362861de
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
+ 138
− 40
View file @ 27cb0832
%% Cell type:markdown id:9eb5530a tags: %% Cell type:markdown id:9eb5530a tags:
We can convert our Knights and Knaves puzzle to conjunctive normal form # 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 ⇔ 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 ∨ ¬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)
{A  B  C, B A, C A, B A, A B} {¬A ∨ ¬B ∨ ¬C, B ∨ A, C ∨ A, ¬B ∨ A, ¬A ∨ B}
``` ```
Below is an encoding of the cnf as a list of lists. 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.
%% Cell type:code id:964ebd52 tags: %% Cell type:code id:964ebd52 tags:
``` prolog ``` prolog
:- discontiguous problem/3. :- discontiguous problem/3.
:- dynamic problem/3. :- dynamic problem/3.
problem(1,'Knights & Knaves', problem(1,'Knights & Knaves',
[ [neg(a),neg(b),neg(c)], [ [neg(a),neg(b),neg(c)],
[pos(b),pos(a)], [pos(b),pos(a)],
[pos(c),pos(a)], [pos(c),pos(a)],
[neg(b),pos(a)], [neg(b),pos(a)],
[neg(a),pos(b)] ]). [neg(a),pos(b)] ]).
negate(pos(A),neg(A)). negate(pos(A),neg(A)).
negate(neg(A),pos(A)). negate(neg(A),pos(A)).
``` ```
%% Cell type:markdown id:fc6823ad tags: %% Cell type:markdown id:fc6823ad tags:
We can pick two clauses and resolve them as follows: We can pick two clauses and resolve them as follows:
%% Cell type:code id:152289b6 tags: %% Cell type:code id:152289b6 tags:
``` prolog ``` prolog
?- problem(1,_,Clauses), ?- problem(1,_,Clauses),
member(C1,Clauses), member(Lit1,C1). member(C1,Clauses), member(Lit1,C1).
``` ```
%% Output %% Output
%% Cell type:code id:2c3dd1bf tags: %% Cell type:code id:2c3dd1bf tags:
``` prolog ``` prolog
?- problem(1,_,Clauses), ?- problem(1,_,Clauses),
member(C1,Clauses), member(Lit1,C1), negate(Lit1,Lit2), member(C1,Clauses), member(Lit1,C1), negate(Lit1,Lit2),
member(C2,Clauses), member(Lit2,C2). member(C2,Clauses), member(Lit2,C2).
%comment. %comment.
``` ```
%% Output %% Output
%% Cell type:code id:33fc6271 tags: %% Cell type:code id:33fc6271 tags:
``` prolog ``` prolog
:- use_module(library(lists)). :- use_module(library(lists)).
resolve(Clause1,Clause2,Resolvent) :- resolve(Clause1,Clause2,Resolvent) :-
select(Lit1,Clause1,R1), negate(Lit1,NLit1), select(Lit1,Clause1,R1), negate(Lit1,NLit1),
select(NLit1,Clause2,R2), select(NLit1,Clause2,R2),
append(R1,R2,Resolvent). append(R1,R2,Resolvent).
``` ```
%% Cell type:code id:78163b60 tags: %% Cell type:code id:78163b60 tags:
``` prolog ``` prolog
?- problem(1,_,Clauses), ?- problem(1,_,Clauses),
member(C1,Clauses), member(C2,Clauses), member(C1,Clauses), member(C2,Clauses),
resolve(C1,C2,NewClause). resolve(C1,C2,NewClause).
``` ```
%% Output %% Output
%% Cell type:code id:9d3fbd1a tags: %% Cell type:code id:9d3fbd1a tags:
``` prolog ``` prolog
?- problem(1,_,Clauses), ?- problem(1,_,Clauses),
findall(NewClause,(member(C1,Clauses), member(C2,Clauses), findall(NewClause,(member(C1,Clauses), member(C2,Clauses),
resolve(C1,C2,NewClause)), NewClauses). resolve(C1,C2,NewClause)), NewClauses).
``` ```
%% Output %% Output
%% Cell type:markdown id:d32921c9 tags: %% Cell type:markdown id:d32921c9 tags:
### DPLL Algorithm ### DPLL Algorithm
We now present bit by bit the DPLL algorithm as a Prolog program We now present bit by bit the DPLL algorithm as a Prolog program
manipulating the above clause database. manipulating the above clause database.
%% Cell type:code id:26924712 tags: %% Cell type:code id:26924712 tags:
``` prolog ``` prolog
becomes_true(TrueLit,Clause) :- becomes_true(TrueLit,Clause) :-
member(TrueLit,Clause). member(TrueLit,Clause).
``` ```
%% Cell type:markdown id:17dd1525 tags: %% Cell type:markdown id:17dd1525 tags:
The above checks if making a given literal true makes the second argument, a clause, true: The above checks if making a given literal true makes the second argument, a clause, true:
%% Cell type:code id:7d90c4ad tags: %% Cell type:code id:7d90c4ad tags:
``` prolog ``` prolog
?- becomes_true(pos(b),[neg(a),pos(b)]). ?- becomes_true(pos(b),[neg(a),pos(b)]).
``` ```
%% Output %% Output
%% Cell type:code id:d4b4e71f tags: %% Cell type:code id:d4b4e71f tags:
``` prolog ``` prolog
?- becomes_true(neg(a),[neg(a),pos(b)]). ?- becomes_true(neg(a),[neg(a),pos(b)]).
``` ```
%% Output %% Output
%% Cell type:code id:3b9c87e4 tags: %% Cell type:code id:3b9c87e4 tags:
``` prolog ``` prolog
simplify(TrueLit,Clause,SimplifedClause) :- simplify(TrueLit,Clause,SimplifedClause) :-
negate(TrueLit,FalseLit), negate(TrueLit,FalseLit),
delete(Clause,FalseLit,SimplifedClause). % Resolution with TrueLit delete(Clause,FalseLit,SimplifedClause). % Resolution with TrueLit
``` ```
%% Cell type:code id:0abd90f6 tags: %% Cell type:code id:0abd90f6 tags:
``` prolog ``` prolog
?- simplify(pos(a),[neg(a),neg(b),neg(c)],R). ?- simplify(pos(a),[neg(a),neg(b),neg(c)],R).
``` ```
%% Output %% Output
%% Cell type:code id:cc81b404 tags: %% Cell type:code id:cc81b404 tags:
``` prolog ``` prolog
?- delete([a,b,c],a,R). ?- delete([a,b,c],a,R).
``` ```
%% Output %% Output
%% Cell type:markdown id:53d21e85 tags: %% Cell type:markdown id:53d21e85 tags:
The above code simplifies a clause by resolution: The above code simplifies a clause by resolution:
%% Cell type:code id:57df05f0 tags: %% Cell type:code id:57df05f0 tags:
``` prolog ``` prolog
?- simplify(pos(c),[pos(a),neg(c)],SC). ?- simplify(pos(c),[pos(a),neg(c)],SC).
``` ```
%% Output %% Output
%% Cell type:code id:a36a54a4 tags: %% Cell type:code id:a36a54a4 tags:
``` prolog ``` prolog
?- simplify(pos(b),[pos(a),neg(c)],SC). ?- simplify(pos(b),[pos(a),neg(c)],SC).
``` ```
%% Output %% Output
%% Cell type:code id:95fcf64b tags: %% Cell type:code id:95fcf64b tags:
``` prolog ``` prolog
set_literal(Lit,Clauses,NewClauses) :- set_literal(Lit,Clauses,NewClauses) :-
exclude(becomes_true(Lit),Clauses,Clauses2), exclude(becomes_true(Lit),Clauses,Clauses2),
maplist(simplify(Lit),Clauses2,NewClauses). maplist(simplify(Lit),Clauses2,NewClauses).
``` ```
%% Cell type:markdown id:f0a8731d tags: %% Cell type:markdown id:f0a8731d tags:
The above code sets a given literal ```Lit``` to true by removing The above code sets a given literal ```Lit``` to true by removing
all now redundant clauses and simplifying the remaining ones via resolution. all now redundant clauses and simplifying the remaining ones via resolution.
%% Cell type:code id:9c35b0b3 tags: %% Cell type:code id:9c35b0b3 tags:
``` prolog ``` prolog
?- exclude(becomes_true(pos(a)), [[neg(b)], [pos(a),pos(c)]],R). ?- exclude(becomes_true(pos(a)), [[neg(b)], [pos(a),pos(c)]],R).
``` ```
%% Output %% Output
%% Cell type:code id:8259d2d7 tags: %% Cell type:code id:8259d2d7 tags:
``` prolog ``` prolog
?- maplist(simplify(neg(c)), [[neg(b),pos(c)], [pos(a),pos(c)]],R). ?- maplist(simplify(neg(c)), [[neg(b),pos(c)], [pos(a),pos(c)]],R).
``` ```
%% Output %% Output
%% Cell type:code id:25b19d82 tags: %% Cell type:code id:25b19d82 tags:
``` prolog ``` prolog
?- set_literal(pos(a),[[neg(a),neg(b),neg(c)]],Res). ?- set_literal(pos(a),[[neg(a),neg(b),neg(c)]],Res).
``` ```
%% Output %% Output
%% Cell type:code id:5535384f tags: %% Cell type:code id:5535384f tags:
``` prolog ``` prolog
?- problem(1,T,C1), set_literal(pos(a),C1,C2). ?- problem(1,T,C1), set_literal(pos(a),C1,C2).
``` ```
%% Output %% Output
%% Cell type:code id:592fcdd9 tags: %% Cell type:code id:592fcdd9 tags:
``` prolog ``` prolog
?- problem(1,_,C1), set_literal(pos(a),C1,C2), set_literal(pos(b),C2,C3). ?- problem(1,_,C1), set_literal(pos(a),C1,C2), set_literal(pos(b),C2,C3).
``` ```
%% Output %% Output
%% Cell type:code id:b8cabba2 tags: %% Cell type:code id:b8cabba2 tags:
``` prolog ``` prolog
dpll(Clauses,[unit(Lit)|Stack]) :- dpll(Clauses,[unit(Lit)|Stack]) :-
select([Lit],Clauses,Clauses2), % unit clause found select([Lit],Clauses,Clauses2), % unit clause found
set_literal(Lit,Clauses2,Clauses3), set_literal(Lit,Clauses2,Clauses3),
dpll(Clauses3,Stack). dpll(Clauses3,Stack).
dpll([],Stack) :- !, Stack=[]. % SAT dpll([],Stack) :- !, Stack=[]. % SAT
dpll(Clauses,[branch(Lit)|Stack]) :- dpll(Clauses,[branch(Lit)|Stack]) :-
\+ member([],Clauses), % no inconsistency \+ member([],Clauses), % no inconsistency
choose_literal(Clauses,Lit), choose_literal(Clauses,Lit),
set_literal(Lit,Clauses,Clauses2), set_literal(Lit,Clauses,Clauses2),
dpll(Clauses2,Stack). dpll(Clauses2,Stack).
choose_literal([ [Lit|_] | _], Lit). choose_literal([ [Lit|_] | _], Lit).
choose_literal([ [Lit|_] | _], NegLit) :- choose_literal([ [Lit|_] | _], NegLit) :-
negate(Lit,NegLit). negate(Lit,NegLit).
``` ```
%% Cell type:code id:e369355c tags: %% Cell type:code id:e369355c tags:
``` prolog ``` prolog
?- problem(1,_,C1), dpll(C1,Stack). ?- problem(1,_,C1), dpll(C1,Stack).
``` ```
%% Output %% Output
%% Cell type:code id:78764141 tags: %% Cell type:code id:78764141 tags:
``` prolog ``` prolog
test(Nr) :- problem(Nr,Str,Clauses), test(Nr) :- problem(Nr,Str,Clauses),
format('Solving problem ~w : ~w~n',[Nr,Str]), format('Solving problem ~w : ~w~n',[Nr,Str]),
(dpll(Clauses,Stack) (dpll(Clauses,Stack)
-> format('SAT: Model found: ~w~n',[Stack]) -> format('SAT: Model found: ~w~n',[Stack])
; format('UNSAT: no model exists',[])). ; format('UNSAT: no model exists',[])).
``` ```
%% Cell type:code id:c51455cf tags: %% Cell type:code id:c51455cf tags:
``` prolog ``` prolog
?- test(1). ?- test(1).
``` ```
%% Output %% Output
%% Cell type:code id:b0466a5d tags: %% Cell type:code id:b0466a5d tags:
``` prolog ``` prolog
problem(2,'Knights & Knaves (Proof by contradiction)', problem(2,'Knights & Knaves (Proof by contradiction)',
[ [neg(a),neg(b),neg(c)], [ [neg(a),neg(b),neg(c)],
[pos(b),pos(a)], [pos(b),pos(a)],
[pos(c),pos(a)], [pos(c),pos(a)],
[neg(b),pos(a)], [neg(b),pos(a)],
[neg(a),pos(b)], [neg(a),pos(b)],
[neg(a),neg(b),pos(c)] ]). % <--- negated Query [neg(a),neg(b),pos(c)] ]). % <--- negated Query
problem(3,'Princess & Tiger', problem(3,'Princess & Tiger',
[[pos(t1),pos(z2),neg(t1)], [[pos(t1),pos(z2),neg(t1)],
[pos(t1),neg(z2)], [pos(t1),neg(z2)],
[neg(t1),neg(z2)], [neg(t1),neg(z2)],
[pos(t1),pos(z1),neg(t2)], [pos(t1),pos(z1),neg(t2)],
[pos(t2),neg(z1)], [pos(t2),neg(z1)],
[neg(t1),neg(z1)], [neg(t1),neg(z1)],
[pos(z1),pos(z2)], [pos(z1),pos(z2)],
[neg(z1),neg(z2)]]). [neg(z1),neg(z2)]]).
``` ```
%% Cell type:code id:2df16148 tags: %% Cell type:code id:2df16148 tags:
``` prolog ``` prolog
?- test(2). ?- test(2).
``` ```
%% Output %% Output
%% Cell type:code id:8d8cf76a tags: %% Cell type:code id:8d8cf76a tags:
``` prolog ``` prolog
?- test(3). ?- test(3).
``` ```
%% Output %% Output
%% Cell type:code id:31d1b945 tags: %% Cell type:code id:31d1b945 tags:
``` prolog ``` prolog
problem(4,'uf-20-02', problem(4,'uf-20-02',
[[ neg(x10) , neg(x16) , pos(x5) ] , [[ neg(x10) , neg(x16) , pos(x5) ] ,
[ pos(x16) , neg(x6) , pos(x5) ] , [ pos(x16) , neg(x6) , pos(x5) ] ,
[ neg(x17) , neg(x14) , neg(x18) ] , [ neg(x17) , neg(x14) , neg(x18) ] ,
[ neg(x10) , neg(x15) , pos(x19) ] , [ neg(x10) , neg(x15) , pos(x19) ] ,
[ neg(x1) , neg(x9) , neg(x18) ] , [ neg(x1) , neg(x9) , neg(x18) ] ,
[ pos(x3) , pos(x7) , neg(x6) ] , [ pos(x3) , pos(x7) , neg(x6) ] ,
[ neg(x13) , pos(x1) , pos(x6) ] , [ neg(x13) , pos(x1) , pos(x6) ] ,
[ neg(x2) , neg(x16) , neg(x20) ] , [ neg(x2) , neg(x16) , neg(x20) ] ,
[ pos(x7) , pos(x8) , pos(x18) ] , [ pos(x7) , pos(x8) , pos(x18) ] ,
[ neg(x7) , pos(x10) , neg(x20) ] , [ neg(x7) , pos(x10) , neg(x20) ] ,
[ pos(x2) , neg(x14) , neg(x17) ] , [ pos(x2) , neg(x14) , neg(x17) ] ,
[ pos(x2) , pos(x1) , pos(x19) ] , [ pos(x2) , pos(x1) , pos(x19) ] ,
[ pos(x7) , neg(x20) , neg(x1) ] , [ pos(x7) , neg(x20) , neg(x1) ] ,
[ neg(x11) , pos(x1) , neg(x17) ] , [ neg(x11) , pos(x1) , neg(x17) ] ,
[ pos(x3) , neg(x12) , pos(x19) ] , [ pos(x3) , neg(x12) , pos(x19) ] ,
[ neg(x3) , neg(x13) , pos(x6) ] , [ neg(x3) , neg(x13) , pos(x6) ] ,
[ neg(x13) , pos(x3) , neg(x12) ] , [ neg(x13) , pos(x3) , neg(x12) ] ,
[ pos(x5) , neg(x7) , neg(x12) ] , [ pos(x5) , neg(x7) , neg(x12) ] ,
[ pos(x20) , pos(x8) , neg(x16) ] , [ pos(x20) , pos(x8) , neg(x16) ] ,
[ neg(x13) , neg(x6) , pos(x19) ] , [ neg(x13) , neg(x6) , pos(x19) ] ,
[ neg(x5) , pos(x1) , pos(x14) ] , [ neg(x5) , pos(x1) , pos(x14) ] ,
[ pos(x9) , neg(x5) , pos(x18) ] , [ pos(x9) , neg(x5) , pos(x18) ] ,
[ neg(x12) , neg(x17) , neg(x1) ] , [ neg(x12) , neg(x17) , neg(x1) ] ,
[ neg(x20) , neg(x16) , pos(x19) ] , [ neg(x20) , neg(x16) , pos(x19) ] ,
[ pos(x12) , pos(x10) , neg(x11) ] , [ pos(x12) , pos(x10) , neg(x11) ] ,
[ pos(x6) , neg(x7) , neg(x2) ] , [ pos(x6) , neg(x7) , neg(x2) ] ,
[ pos(x13) , neg(x10) , pos(x17) ] , [ pos(x13) , neg(x10) , pos(x17) ] ,
[ neg(x20) , pos(x8) , neg(x16) ] , [ neg(x20) , pos(x8) , neg(x16) ] ,
[ neg(x10) , neg(x1) , neg(x8) ] , [ neg(x10) , neg(x1) , neg(x8) ] ,
[ neg(x7) , neg(x3) , pos(x19) ] , [ neg(x7) , neg(x3) , pos(x19) ] ,
[ pos(x19) , neg(x1) , neg(x6) ] , [ pos(x19) , neg(x1) , neg(x6) ] ,
[ pos(x19) , neg(x2) , pos(x13) ] , [ pos(x19) , neg(x2) , pos(x13) ] ,
[ neg(x2) , pos(x20) , neg(x9) ] , [ neg(x2) , pos(x20) , neg(x9) ] ,
[ neg(x8) , neg(x20) , pos(x16) ] , [ neg(x8) , neg(x20) , pos(x16) ] ,
[ neg(x13) , neg(x1) , pos(x11) ] , [ neg(x13) , neg(x1) , pos(x11) ] ,
[ pos(x15) , neg(x12) , neg(x6) ] , [ pos(x15) , neg(x12) , neg(x6) ] ,
[ neg(x17) , neg(x19) , pos(x9) ] , [ neg(x17) , neg(x19) , pos(x9) ] ,
[ pos(x19) , neg(x18) , pos(x16) ] , [ pos(x19) , neg(x18) , pos(x16) ] ,
[ pos(x7) , neg(x8) , neg(x19) ] , [ pos(x7) , neg(x8) , neg(x19) ] ,
[ neg(x3) , neg(x7) , neg(x1) ] , [ neg(x3) , neg(x7) , neg(x1) ] ,
[ pos(x7) , neg(x17) , neg(x16) ] , [ pos(x7) , neg(x17) , neg(x16) ] ,
[ neg(x2) , neg(x14) , pos(x1) ] , [ neg(x2) , neg(x14) , pos(x1) ] ,
[ neg(x18) , neg(x10) , neg(x8) ] , [ neg(x18) , neg(x10) , neg(x8) ] ,
[ neg(x16) , pos(x5) , pos(x8) ] , [ neg(x16) , pos(x5) , pos(x8) ] ,
[ pos(x4) , pos(x8) , pos(x10) ] , [ pos(x4) , pos(x8) , pos(x10) ] ,
[ neg(x20) , neg(x11) , neg(x19) ] , [ neg(x20) , neg(x11) , neg(x19) ] ,
[ pos(x8) , neg(x16) , neg(x6) ] , [ pos(x8) , neg(x16) , neg(x6) ] ,
[ pos(x18) , pos(x12) , pos(x8) ] , [ pos(x18) , pos(x12) , pos(x8) ] ,
[ neg(x5) , neg(x20) , neg(x10) ] , [ neg(x5) , neg(x20) , neg(x10) ] ,
[ pos(x16) , pos(x17) , pos(x3) ] , [ pos(x16) , pos(x17) , pos(x3) ] ,
[ pos(x7) , neg(x1) , neg(x17) ] , [ pos(x7) , neg(x1) , neg(x17) ] ,
[ pos(x17) , neg(x4) , pos(x7) ] , [ pos(x17) , neg(x4) , pos(x7) ] ,
[ pos(x20) , neg(x9) , neg(x13) ] , [ pos(x20) , neg(x9) , neg(x13) ] ,
[ pos(x13) , pos(x18) , pos(x16) ] , [ pos(x13) , pos(x18) , pos(x16) ] ,
[ neg(x16) , neg(x6) , pos(x5) ] , [ neg(x16) , neg(x6) , pos(x5) ] ,
[ pos(x5) , pos(x17) , pos(x7) ] , [ pos(x5) , pos(x17) , pos(x7) ] ,
[ neg(x12) , neg(x17) , neg(x6) ] , [ neg(x12) , neg(x17) , neg(x6) ] ,
[ neg(x20) , pos(x19) , neg(x5) ] , [ neg(x20) , pos(x19) , neg(x5) ] ,
[ pos(x9) , neg(x19) , pos(x16) ] , [ pos(x9) , neg(x19) , pos(x16) ] ,
[ neg(x13) , neg(x16) , pos(x11) ] , [ neg(x13) , neg(x16) , pos(x11) ] ,
[ neg(x4) , neg(x19) , neg(x18) ] , [ neg(x4) , neg(x19) , neg(x18) ] ,
[ neg(x13) , pos(x10) , neg(x15) ] , [ neg(x13) , pos(x10) , neg(x15) ] ,
[ pos(x16) , neg(x7) , neg(x14) ] , [ pos(x16) , neg(x7) , neg(x14) ] ,
[ neg(x19) , neg(x7) , neg(x18) ] , [ neg(x19) , neg(x7) , neg(x18) ] ,
[ neg(x20) , pos(x5) , pos(x13) ] , [ neg(x20) , pos(x5) , pos(x13) ] ,
[ pos(x12) , neg(x6) , pos(x4) ] , [ pos(x12) , neg(x6) , pos(x4) ] ,
[ pos(x7) , pos(x9) , neg(x13) ] , [ pos(x7) , pos(x9) , neg(x13) ] ,
[ pos(x16) , pos(x3) , pos(x7) ] , [ pos(x16) , pos(x3) , pos(x7) ] ,
[ pos(x9) , neg(x1) , pos(x12) ] , [ pos(x9) , neg(x1) , pos(x12) ] ,
[ neg(x3) , pos(x14) , pos(x7) ] , [ neg(x3) , pos(x14) , pos(x7) ] ,
[ pos(x1) , pos(x15) , pos(x14) ] , [ pos(x1) , pos(x15) , pos(x14) ] ,
[ neg(x8) , neg(x11) , pos(x18) ] , [ neg(x8) , neg(x11) , pos(x18) ] ,
[ pos(x19) , neg(x9) , pos(x7) ] , [ pos(x19) , neg(x9) , pos(x7) ] ,
[ neg(x10) , pos(x6) , pos(x2) ] , [ neg(x10) , pos(x6) , pos(x2) ] ,
[ pos(x14) , pos(x18) , neg(x11) ] , [ pos(x14) , pos(x18) , neg(x11) ] ,
[ neg(x9) , neg(x16) , pos(x14) ] , [ neg(x9) , neg(x16) , pos(x14) ] ,
[ pos(x1) , pos(x11) , neg(x20) ] , [ pos(x1) , pos(x11) , neg(x20) ] ,
[ pos(x11) , pos(x12) , neg(x4) ] , [ pos(x11) , pos(x12) , neg(x4) ] ,
[ pos(x13) , neg(x11) , neg(x14) ] , [ pos(x13) , neg(x11) , neg(x14) ] ,
[ pos(x17) , neg(x12) , pos(x9) ] , [ pos(x17) , neg(x12) , pos(x9) ] ,
[ pos(x14) , pos(x9) , pos(x1) ] , [ pos(x14) , pos(x9) , pos(x1) ] ,
[ pos(x8) , pos(x19) , pos(x4) ] , [ pos(x8) , pos(x19) , pos(x4) ] ,
[ pos(x6) , neg(x13) , neg(x20) ] , [ pos(x6) , neg(x13) , neg(x20) ] ,
[ neg(x2) , neg(x13) , pos(x11) ] , [ neg(x2) , neg(x13) , pos(x11) ] ,
[ pos(x14) , neg(x13) , pos(x17) ] , [ pos(x14) , neg(x13) , pos(x17) ] ,
[ pos(x9) , neg(x11) , pos(x18) ] , [ pos(x9) , neg(x11) , pos(x18) ] ,
[ neg(x13) , neg(x6) , pos(x5) ] , [ neg(x13) , neg(x6) , pos(x5) ] ,
[ pos(x5) , pos(x19) , neg(x18) ] , [ pos(x5) , pos(x19) , neg(x18) ] ,
[ neg(x4) , pos(x10) , pos(x11) ] , [ neg(x4) , pos(x10) , pos(x11) ] ,
[ neg(x18) , neg(x19) , neg(x20) ] , [ neg(x18) , neg(x19) , neg(x20) ] ,
[ pos(x3) , neg(x9) , pos(x8) ] [ pos(x3) , neg(x9) , pos(x8) ]
]). ]).
problem(5,'schaltung_a1.pl', problem(5,'schaltung_a1.pl',
[ [
%a. not_b. c. not_d. e. %a. not_b. c. not_d. e.
[pos(a)], [neg(b)], [pos(c)], [neg(d)], [pos(e)], [pos(a)], [neg(b)], [pos(c)], [neg(d)], [pos(e)],
% Schaltungen der ersten Ebene % Schaltungen der ersten Ebene
%and11 :- a,b. %and11 :- a,b.
[pos(and11),neg(a),neg(b)], [pos(and11),neg(a),neg(b)],
%or11 :- b. %or11 :- b.
[pos(or11),neg(b)], [pos(or11),neg(b)],
%or11 :- c. %or11 :- c.
[pos(or11),neg(b)], [pos(or11),neg(b)],
%and12 :- c,d. %and12 :- c,d.
[pos(and12),neg(c),neg(d)], [pos(and12),neg(c),neg(d)],
%not1 :- not_e. %not1 :- not_e.
[pos(not1),pos(e)], [pos(not1),pos(e)],
% Schaltungen der zweiten Ebene % Schaltungen der zweiten Ebene
%or21 :- and11. %or21 :- and11.
[pos(or21),neg(and11)], [pos(or21),neg(and11)],
%or21 :- not1. %or21 :- not1.
[pos(or21),neg(not1)], [pos(or21),neg(not1)],
%and2 :- or11, not1. %and2 :- or11, not1.
[pos(and2),neg(or11),neg(not1)], [pos(and2),neg(or11),neg(not1)],
%or22 :- and12. %or22 :- and12.
[pos(or22),neg(and12)], [pos(or22),neg(and12)],
%or22 :- not1. %or22 :- not1.
[pos(or22),neg(not1)], [pos(or22),neg(not1)],
%not2 :- e. % \+ not1. %not2 :- e. % \+ not1.
[pos(not2),neg(e)], [pos(not2),neg(e)],
% Schaltungen der dritten Ebene % Schaltungen der dritten Ebene
%and3 :- or21, and2. %and3 :- or21, and2.
[pos(and3),neg(or21),neg(and2)], [pos(and3),neg(or21),neg(and2)],
%or3 :- or22. %or3 :- or22.
[pos(or3),neg(or22)], [pos(or3),neg(or22)],
%or3 :- not2. %or3 :- not2.
[pos(or3),neg(not2)], [pos(or3),neg(not2)],
% Schaltungen der vierten Ebene % Schaltungen der vierten Ebene
%or4 :- and3. %or4 :- and3.
[pos(or4),neg(and3)], [pos(or4),neg(and3)],
%or4 :- or3. %or4 :- or3.
[pos(or4),neg(or3)], [pos(or4),neg(or3)],
%and4 :- or3, not2. %and4 :- or3, not2.
[pos(and4),neg(or3),neg(not2)], [pos(and4),neg(or3),neg(not2)],
% Letzte Ebene % Letzte Ebene
%and5 :- and4, or4. %and5 :- and4, or4.
[pos(and5),neg(and4),neg(or4)], [pos(and5),neg(and4),neg(or4)],
%output :- and5. %output :- and5.
[pos(output),neg(and5)], [pos(output),neg(and5)],
% ?- output. % ?- output.
[neg(output)] [neg(output)]
]). ]).
problem(6, 'doodle-wo-max1-constraint', problem(6, 'doodle-wo-max1-constraint',
[ [
[pos(x1),pos(x3)], [pos(x1),pos(x3)],
[neg(x3)], [neg(x3)],
[neg(x5)], [neg(x5)],
[pos(x4),pos(x5)] [pos(x4),pos(x5)]
]). ]).
problem(7, 'doodle-with-max1-constraint', problem(7, 'doodle-with-max1-constraint',
[ [
[pos(x1),pos(x3)], [pos(x1),pos(x3)],
[neg(x3)], [neg(x3)],
[neg(x5)], [neg(x5)],
[pos(x4),pos(x5)], [pos(x4),pos(x5)],
[neg(x1),neg(x2)], [neg(x1),neg(x3)], [neg(x1),neg(x4)], [neg(x1),neg(x2)], [neg(x1),neg(x3)], [neg(x1),neg(x4)],
[neg(x1),neg(x5)], [neg(x1),neg(x5)],
[neg(x2),neg(x3)], [neg(x2),neg(x4)],[neg(x2),neg(x5)], [neg(x2),neg(x3)], [neg(x2),neg(x4)],[neg(x2),neg(x5)],
[neg(x3),neg(x4)],[neg(x3),neg(x5)], [neg(x3),neg(x4)],[neg(x3),neg(x5)],
[neg(x4),neg(x5)] [neg(x4),neg(x5)]
]). ]).
``` ```
%% Cell type:code id:c51f1ce6 tags: %% Cell type:code id:c51f1ce6 tags:
``` prolog ``` prolog
?- test(4). ?- test(4).
``` ```
%% Output %% Output
%% Cell type:code id:bc767ce8 tags: %% Cell type:code id:39bb01e4 tags:
``` prolog
?-test(2).
```
%% Output
%% Cell type:markdown id:d3ec741b tags:
%% Cell type:code id:062d6089 tags:
``` prolog
jupyter:version.
```
%% Output
%% Cell type:code id:03d3fe70 tags:
``` prolog ``` prolog
jupyter:version(A,B,C,D)
``` ```
%% Output
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment