Problems while implementing DPLL algorithm

[Crafts]

I’m using: SWI-Prolog version 7.6.4

Im trying to write a SAT Solver with DPLL algorithm. Its based on this pseudo code:

In general I have the following problems:

• How to implement the second case “if ({} ∈ F) return false”. I can not return “false”. How far I understand, Prolog is returning false when no other clause is true. So I made a check “+has_empty_clause(Clauses)” inside the other functions to make them false in that case. But I’m not sure if thats the right way of doing it.

• Inside the “else choose Lit ∈ atom(F)” case there is this return: “return DPLL(F’) || DPLL(F’’)”.
  I’m not sure how to implement this “or”.

• I’m unsure about the cuts I used here

Here I have some part of my code (the dpll functions, I will add the rest of the code when needed):

% if (F == {}) return true.
dpll([]).

% if ({Lit} ∈ F)
dpll(Clauses) :-
    % Check condition: if ({} ∈ F) return false.
    \+has_empty_clause(Clauses),
    % Get clause with only one literal
    clause_with_only_one_literal(Clauses, [Lit]),
    % F' is Clauses_N here
    set_literal(Lit, Clauses, Clauses_N),
    % Call with new Clause
    dpll(Clauses_N), !.

% else choose Lit ∈ atom(F)
dpll(Clauses) :-
    % Check condition if ({} ∈ F) return false. When there is an empty clause its always false
    \+has_empty_clause(Clauses),
    % select value
    choose_literal(Clauses, Lit),
    negate(Lit, NegLit),
    (dpll([[Lit]|Clauses]) ; dpll([[NegLit]|Clauses])), !.

Here are some example calls:
?- sat_solver:dpll([[a], [not(b)], [c]]).
true.

?- sat_solver:dpll([[a,b], [a], [b,not(e),[d]], [b,e,d], [b, not(a)]]).
true.

?- sat_solver:dpll([[a],[not(a)]]).
Ends in an infinite loop, but should return false.

[EricGT]

Not a direct answer to your question but are you aware of library(clpb): CLP(B): Constraint Logic Programming over Boolean Variables?

?- use_module(library(clpb)).
true.

?- sat(A * ~B * C).
A = C, C = 1,
B = 0.

?- sat(A * ~A).
false.

If you question is for a homework exercise, then at least you can use this to cross check your work.

---

References:

Computability and Logic 5th Edition
by George S. Boolos, John P. Burgess and Richard C. Jeffrey
(PDF) (WorldCat)

Machine Program for Theorem-Proving

Automated Reasoning: satisfiability Coursera video

Satisfiability (Wikipedia)

From: Computability and Logic 5th Edition

A set of sentences L is unsatisfiable if no interpretation makes L true (and is satisfiable if some interpretation does).

DPLL (Wikipedia) (Wikipedia Talk)

Unit propagation (Wikipedia)

DPLL(T ) as a goal-directed proof-search mechanism

---

Examples using SWI-Prolog clpb to demonstrate satisfiable.

P

?- sat(P).
P = 1.

P
0
1

---

~P

?- sat(~P).
P = 0.

P	~P
0	1
1	0

---

P AND Q

?- sat(P*Q).
P = Q, Q = 1

P	Q	P AND Q
0	0	0
0	1	0
1	0	0
1	1	1

---

P OR Q

NB clpb will simplify a formula, however for these examples the values are needed so labeling must be used for this example.

?- sat(P+Q),labeling([P,Q]).
P = 0, Q = 1 ;
P = 1, Q = 0 ;
P = Q, Q = 1

P	Q	P OR Q
0	0	0
0	1	1
1	0	1
1	1	1

---

Note: clpb needs a space with some operators (I don’t know the exact rules for such), e.g.

?- sat(P*~P).
ERROR: Syntax error: Operator expected
ERROR: sat(
ERROR: ** here **
ERROR: P*~P) . 

?- sat(P * ~P).
false.

P	NOT P	P AND NOT P
0	1	0
1	0	0

Since P AND NOT P is always false, it is not satisfiable.

---

Example from Wikipedia Unit Propagation

NB This is in CNF - a conjunction of one or more clauses, where a clause is a disjunction of literals;

(A OR B) AND (NOT A OR C) AND (NOT C OR D) AND A

?- sat((A + B) * (~A + C) * (~C + D) * A).
A = C, C = D, D = 1,
sat(B=:=B).

?- sat((A + B) * (~A + C) * (~C + D) * A), labeling([A,B,C,D]).
A = C, C = D, D = 1, B = 0 ;
A = B, B = C, C = D, D = 1.

A	B	C	D	A OR B	NOT A OR C	NOT C OR D	A	(A OR B) AND (NOT A OR C) AND (NOT C OR D) AND A
0	0	0	0	0	1	1	0	0
0	0	0	1	0	1	1	0	0
0	0	1	0	0	1	0	0	0
0	0	1	1	0	1	1	0	0
0	1	0	0	1	1	1	0	0
0	1	0	1	1	1	1	0	0
0	1	1	0	1	1	0	0	0
0	1	1	1	1	1	1	0	0
1	0	0	0	1	0	1	1	0
1	0	0	1	1	0	1	1	0
1	0	1	0	1	1	0	1	0
1	0	1	1	1	1	1	1	1
1	1	0	0	1	0	1	1	0
1	1	0	1	1	0	1	1	0
1	1	1	0	1	1	0	1	0
1	1	1	1	1	1	1	1	1

---

Note: The clpb source code does not have any test cases, or at least that I could find, so here are some for demonstration purposes.

:- begin_tests(clpb).

% Logical not
test(001) :-
    findall([P],(sat(~P),labeling([P])),Solutions),
    assertion( Solutions == [[0]] ).

% Logical and
test(002) :-
    findall([P,Q],(sat(P * Q),labeling([P,Q])),Solutions),
    assertion( Solutions == [[1,1]] ).

% Logical or
test(003) :-
    findall([P,Q],(sat(P + Q),labeling([P,Q])),Solutions),
    assertion( Solutions == [[0,1],[1,0],[1,1]] ).

% Logical exclusive or
test(004) :-
    findall([P,Q],(sat(P # Q),labeling([P,Q])),Solutions),
    assertion( Solutions == [[0,1],[1,0]] ).

% http://profs.sci.univr.it/~farinelli/courses/ar/slides/DPLL.pdf

% Example 1 - Showing how to test a satisfication that fails using the Prolog unit test ability to check for failure.
test(101,[fail]) :-
    sat((P + Q + ~R) * (P + ~Q) * ~P * R * U).

% Example 1 - Showing how to test a satisfication that fails using labeling/1 with assertion/1 for failure.
test(102) :-
    findall([P,Q,R,U],(sat((P + Q + ~R) * (P + ~Q) * ~P * R * U),labeling([P,Q,R,U])),Solutions),
    assertion( Solutions == [] ).

% Example 2
test(103) :-
    findall([P,Q,R],(sat((P + Q) * ~Q * (~P + Q + ~R)),labeling([P,Q,R])),Solutions),
    assertion( Solutions == [[1,0,0]] ).

% Example 3
test(104) :-
    findall([P,Q,R],(sat((P + Q) * (P + ~Q) * (~P + Q) * (~P + ~R)),labeling([P,Q,R])),Solutions),
    assertion( Solutions == [[1,1,0]] ).

% Example 4
test(105) :-
    findall([P,Q,R],(sat((P + ~Q) * (~P + R) * Q),labeling([P,Q,R])),Solutions),
    assertion( Solutions == [[1,1,1]] ).

% Exercise 1
test(106) :-
    findall([P,Q,R],(sat((P + Q) * (~P + Q) * (~R + ~Q) * (R + ~Q)),labeling([P,Q,R])),Solutions),
    assertion( Solutions == [] ).

% Exercise 2
test(107) :-
    findall([P,Q,R],(sat((P + Q + R) * (~P + ~Q + ~R) * (~P + Q + R) * (~Q + R) * (Q + ~R)),labeling([P,Q,R])),Solutions),
    assertion( Solutions == [[0,1,1]] ).

% Exercise 3
test(108) :-
    findall([P,Q,R],(sat((~Q + P) * (~P  + ~Q) * (Q + R) * (~Q + ~R) * (~P + ~R) * (P + ~R)),labeling([P,Q,R])),Solutions),
    assertion( Solutions == [] ).

:- end_tests(clpb).

[Crafts]

@EricGT

Not a direct answer to your question but are you aware of library(clpb): CLP(B): Constraint Logic Programming over Boolean Variables?

I didn’t know about it yet, thanks for the advise. Part of the exercise is also to find true/false values for Variables to make the given CNF true.
My implementation Currently only handles literals like a,b,c so far. Later it should be possible to let it solve CNFs like [[X,Y], [true,X],[Z]].
I’m trying to implement it with literals and without the unification of true/false first and then customize it after. But so far I’m already failing at this stage.

[EricGT]

I take it you know Python (because of def) and are translating that to Prolog. Is there a requirement that you use that variation of DPLL? I found this variation in Prolog but haven’t checked it. Could that be used instead?

Also I find that test case are helpful. Are you aware Prolog has unit test?

Also can you show all of the code. Some of your predicates are missing, e.g. has_empty_clause/1, choose_literal/2

[Crafts]

Its not required to use this specific algorithm on the picture, but its from a tutorial video where everything was complained step by step which helped me to understand the algorithm.
The one of my course script is much harder to understand, but seems to be the same in general. Thats why I decided to implement it instead. I write some unit tests for my code and I also have some unit tests as part of the exercise.

This is one of my tests (currently its testing primary the functions used in my dpll functions):

test(tsc_set_literal5,[nondet]) :-
    set_literal(b, [[b], [not(b)]], R), !, R ==  [[]].

And this is one of the tests from the exercise:

test(sat2, [nondet,true(X == true)]) :-
    to_cnf(or(lit(X),and(lit(true),lit(false))), CNF),
    solve(CNF).

[EricGT]

@Crafts

a tutorial video

Can you provide a link to the video. Then we can try an fix your code so you understand it.

Also I really do need all of your current code to see where the problem is. Without it there is no sense in me trying to find the bug in your code or show you how to fix it.

[Crafts]

Unfortunately the tutorial video is in German:

The complete code:

:- module(sat_solver,[]).

negate(not(X),X) :- !.
negate(X,not(X)) :- !.
    
clause_with_only_one_literal([H|_],H) :-
    length(H, 1),
    !.
clause_with_only_one_literal([_|T],R) :-
    clause_with_only_one_literal(T,R).
    
disjunktion_becomes_true(TrueLit, Clause) :-
    % Check if element is in list
    member(TrueLit, Clause).

simplify_dpll(FalseLit, Clause, Simplified) :-
    % delete given element (FalseLit) from given list and return list without element
    delete(Clause, FalseLit, Simplified).
    
set_literal(Lit, Clauses, NewClauses) :-
    % Remove the clauses (disjunktions) where the lit is true, because they are true anyway (disjunktions)
    % ?- exclude(sat_solver:disjunktion_becomes_true(a),[ [a,b], [b] ], R ).
    % R = [[b]].
    exclude(disjunktion_becomes_true(Lit), Clauses, Clauses2),
    % Negate lit
    negate(Lit, NegLit),
    % Remove the false lit (negated lit) in all clauses, because they don't affect if the Clauses(disjunktions) are true 
    maplist(simplify_dpll(NegLit), Clauses2, NewClauses).


has_empty_clause(Clauses) :-
    member([], Clauses), !.

choose_literal([[Lit|_]|_], Lit).

% https://www.youtube.com/watch?v=keILzTb0Soo
% DPLL(F)
% F are all Clauses (List of Clauses)
% if (F == {}) return true.
% dpll([]).
dpll([]).
% if ({Lit} ∈ F) (there is a clause existing with only one element inside for example {a} in {{a,b} ,{a}})  
%   F' = {Clause ∈ F mit Lit,¬Lit ∉ K}∪{Clause\{¬Lit} ∈ F}     (set_literal)
%   return DPLL(F')
dpll(Clauses) :-
    % Check condition if ({} ∈ F) return false. When there is an empty clause its always false
    \+has_empty_clause(Clauses),
    % Get clause with only one literal
    clause_with_only_one_literal(Clauses, [Lit]),
    % F' is Clauses_N here
    set_literal(Lit, Clauses, Clauses_N),
    % Call with new Clause
    dpll(Clauses_N), !.

% else choose Lit ∈ atom(F) (any value from clause)
%   F' = F ∪ {{Lit}}
%   F''= F ∪ {{¬Lit}}
%   return DPLL(F') || DPLL(F'')
dpll(Clauses) :-
    % Check condition if ({} ∈ F) return false. When there is an empty clause its always false
    \+has_empty_clause(Clauses),
    % select value
    choose_literal(Clauses, Lit),
    negate(Lit, NegLit),
    (dpll([[Lit]|Clauses]) ; dpll([[NegLit]|Clauses])), !.

Tests:

:- begin_tests(tsc).

test(tsc_set_literal1,[nondet]) :-
    set_literal(a, [[a,b], [a], [b,not(c),[d]], [b,c,d], [b, not(a)]], R), !, R ==  [[b, not(c), [d]], [b, c, d], [b]].
    
test(tsc_set_literal2,[nondet]) :-
    set_literal(a, [[a,b], [a], [b,not(a),d], [b,c,d]], R), !, R ==  [[b, d], [b, c, d]].
    
test(tsc_set_literal3,[nondet]) :-
    set_literal(z, [[z],[z,not(z)]], R), !, R ==  [].
    
test(tsc_set_literal4,[nondet]) :-
    set_literal(z, [[not(z)],[z,not(z)]], R), !, R ==  [[]].
    
test(tsc_set_literal5,[nondet]) :-
    set_literal(b, [[b], [not(b)]], R), !, R ==  [[]].

:- end_tests(tsc).

[EricGT]

Thanks for the link to the video. You are correct that I don’t know German and I could not find an easy way to translate the spoken German to English. However DPLL is common enough in examples that there is a good change I can find the same algorithm explained in English somewhere else if I need it. For now I will forgo trying to find more details about this specific implementation and work with just your code.

The first thing I am doing is to write test cases for every one of your predicates so that I understand how they work. This will take some time.

[EricGT]

@Crafts

Inside the “else choose Lit ∈ atom(F)” case there is this return: “return DPLL(F’) || DPLL(F’’)”.
I’m not sure how to implement this “or”.

I am still working on the unit tests, but in checking for your problems wanted to note that in Prolog , is logical and and ; is logical or.

?- true,true.
true.

?- true,false.
false.

?- true;true.
true ;
true.

?- true;false.
true ;
false.

See: Control Predicates

[Crafts]

Thank you for your help.

I was adding some prints to my function to check where exactly it’s getting infinite.
I have this call
sat_solver:dpll([[a], [not(a)]]).
The result should be false, because there is no solution for this formula, but its getting infinite instead.

First I land in “if ({Lit} ∈ F)” because there is a clause with only one literal.
Inside the clause [a] gets removed and the not(a) inside the other clause get also removed, so what lefts is [[]].
Usually the programm should stop now and return false because they was no solution. But instead the program continue and calls:
“else choose Lit ∈ atom(F)” with the original Clauses “[[a],[not(a)]]”.
It shouldn’t call this case, because the condition “if ({Lit} ∈ F)” was already true for the formula. Now its adding a clause with single literal so we get “[[a],[a],[not(a)]]” and its repeating this again and again:
[[a],[a],[a],[not(a)]]
[[a],[a],[a],[a],[not(a)]]
[[a],[a],[a],[a],[a],[not(a)]]
because its always ending in this case.

So now I added " +clause_with_only_one_literal(Clauses, _)" to the “else choose Lit ∈ atom(F)” case:

% else choose Lit ∈ atom(F) (irgendeinen Wert aus den Klauseln)
%   F' = F ∪ {{Lit}}
%   F''= F ∪ {{¬Lit}}
dpll(Clauses) :-
    % Check condition if ({} ∈ F) return false. When there is an empty clause its always false
    \+has_empty_clause(Clauses),
    \+clause_with_only_one_literal(Clauses, _), % Added this which is false when there is no clause with one literal
    % select value
    choose_literal(Clauses, Lit),
    negate(Lit, NegLit),
    (dpll([[Lit]|Clauses]) ; dpll([[NegLit]|Clauses])), !.

It seems to work now:

?- sat_solver:dpll([[a], [not(a)]]).
false.

But I don’t understand why this is nessecary. I was thinking the cut “!” at the end of the clauses is preventig prolog from checking the other clauses?

[peter.ludemann]

@Crafts

I can not return “false”. How far I understand, Prolog is returning false when no other clause is true.

Prolog doesn’t return “false” from a predicate – it fails. There’s a difference.

And, if you want, you can return a true/false value instead of using success/failure.

Suppose you have this functional program (in Python):

def is_even(x):
    if x % 2 == 0:
      return True
    else
      return False

then you can write the equivalent in Prolog, where the 1st argument is the value being tested and the 2nd argument is unified with true or false, depending on whether x is even or odd:

is_even(X, true)  :- 0 =:= X mod 2.
is_even(X, false) :- 1 =:= X mod 2. % test can be removed using "cut" in 1st clause

or, if you have a predicate that uses success/failure, you can transform it to return a true/false value by:

is_even(X) :- 0 =:= X mod 2. % succeeds if X is even; fails if X is odd

is_even(X, true)  :- is_even(X),
is_even(X, false) :- \+ is_even(X). % test can be removed using "cut" in 1st clause

or

is_even(X, Result) :-
    (  is_even(X)
    -> Result = true
    ;  Result = false
    ).

It’s more verbose to pass around true and false values (which have no special meaning in Prolog, of course), so it’s usually not done; and you can always turn a succeed/failure into a true/false if you need to. (There are some subtleties … the if-then-else is a kind of “cut”, which gives only a single result; so if there are uninstantiated variables in the if part, you need to be careful.)