Prolog SAT Solver

Question

I'm trying to build a simple Prolog SAT solver. My idea is that the user should enter the boolean formula to be solved in CNF (Conjuctive Normal Form) using Prolog lists, for example (A or B) and (B or C) should be presented as sat([[A, B], [B, C]]) and Prolog procedes to find the values for A, B, C.

My following code is not working and I'm not understanding why. On this line of the trace Call: (7) sat([[true, true]]) ? I was expecting start_solve_clause([_G609, _G612]]).

Disclaimer: Sorry for the crappy code I didn't even know about Prolog or the SAT problem a few days ago.

P.S.: Advice on solving the SAT is welcome.

Trace

sat([[X, Y, Z], [X, Y]]).
Call: (6) sat([[_G609, _G612, _G615], [_G609, _G612]]) ? creep
Call: (7) start_solve_clause([_G609, _G612, _G615]) ? creep
Call: (8) solve_clause([_G615], _G726) ? creep
Call: (9) or(_G725, _G615, true) ? creep
Exit: (9) or(true, true, true) ? creep
Exit: (8) solve_clause([true], true) ? creep
Call: (8) or(_G609, _G612, true) ? creep
Exit: (8) or(true, true, true) ? creep
Exit: (7) start_solve_clause([true, true, true]) ? creep
Call: (7) sat([[true, true]]) ?

Prolog Source

% Knowledge base
or(true, true, true).
or(false, false, false).
or(true, false, true).
or(false, true, true).

or(not(true), true, true).
or(not(false), false, true).
or(not(true), false, false).
or(not(false), true, true).

or(true, not(true), true).
or(false, not(false), true).
or(true, not(false), true).
or(false, not(true), false).

% SAT solver
sat([]).
sat([Clause | Tail]) :- start_solve_clause(Clause), sat(Tail).

% Clause solver
start_solve_clause([Var1, Var2 | Tail]) :- solve_clause(Tail, Result), or(Var1, Var2, Result).

solve_clause([X | []], Result) :- or(Result, X, true).
solve_clause([X | Tail], Result) :- solve_clause(Tail, Result2), or(Result, X, Result2).

score 6 · Answer 1 · answered Feb 12 '11 at 13:17

There is a wonderful paper by Howe and King about SAT Solving in (SICStus) Prolog (see http://www.soi.city.ac.uk/~jacob/solver/index.html).

sat(Clauses, Vars) :- 
    problem_setup(Clauses), elim_var(Vars). 

elim_var([]). 
elim_var([Var | Vars]) :- 
    elim_var(Vars), (Var = true; Var = false). 

problem_setup([]). 
problem_setup([Clause | Clauses]) :- 
    clause_setup(Clause), 
    problem_setup(Clauses). 

clause_setup([Pol-Var | Pairs]) :- set_watch(Pairs, Var, Pol). 

set_watch([], Var, Pol) :- Var = Pol. 
set_watch([Pol2-Var2 | Pairs], Var1, Pol1):- 
    watch(Var1, Pol1, Var2, Pol2, Pairs). 

:- block watch(-, ?, -, ?, ?). 
watch(Var1, Pol1, Var2, Pol2, Pairs) :- 
    nonvar(Var1) -> 
        update_watch(Var1, Pol1, Var2, Pol2, Pairs); 
        update_watch(Var2, Pol2, Var1, Pol1, Pairs). 

update_watch(Var1, Pol1, Var2, Pol2, Pairs) :- 
    Var1 == Pol1 -> true; set_watch(Pairs, Var2, Pol2).

The clauses are given in CNF like this:

| ?- sat([[true-X,false-Y],[false-X,false-Y],[true-X,true-Z]],[X,Y,Z]).
 X = true,
 Y = false,
 Z = true ? ;
 X = false,
 Y = false,
 Z = true ? ;
 X = true,
 Y = false,
 Z = false ? ;
no

score 4 · Answer 2 · 2013-09-08T20:29:43.610

One can use CLP(FD) to solve SAT. Just start with a CNF and then observe that a clause:

x1 v .. v xn

Can be represented as a constraint:

x1 + .. + xn #> 0

Further for a negative literal:

~x

Simply use:

1-x

You need to restrict the variables to the domain 0..1 and invoke labeling. As soon as labeling returns some value for the variables, you know that your original formula is satisfiable.

Here is an example run, running the test of Joe Lehmann:

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 6.5.2)
Copyright (c) 1990-2013 University of Amsterdam, VU Amsterdam

?- use_module(library(clpfd)).

?- L = [X,Y,Z], L ins 0..1, X+1-Y #> 0, 1-X+1-Y #> 0, X+Z #> 0, label(L).
X = Y, Y = 0,
Z = 1 ;
X = 1,
Y = Z, Z = 0 ;
X = Z, Z = 1,
Y = 0.

Bye

Constraint Logic Programming over Finite Domains
http://www.swi-prolog.org/man/clpfd.html

Perhaps [`clpb`](http://www.swi-prolog.org/pldoc/man?section=clpb) can be helpful here? — Daniel Lyons, Dec 15 '15 at 21:37

score 3 · Answer 3 · 2013-09-10T14:48:56.070

Sometimes the following coding is found. Clauses are
represented by assigning distinct positive non-zero
integers to propositional variables:

x1 v .. v xn --> [x1, .. , xn]
~x           --> -x

It seems that the following Prolog code works quite well:

% mem(+Elem, +List)
mem(X, [X|_]).
mem(X, [_|Y]) :-
    mem(X, Y).

% sel(+Elem, +List, -List)
sel(X, [X|Y], Y).
sel(X, [Y|Z], [Y|T]) :-
    sel(X, Z, T).

% filter(+ListOfList, +Elem, +Elem, -ListOfList)
filter([], _, _, []).
filter([K|F], L, M, [J|G]) :-
    sel(M, K, J), !,
    J \== [],
    filter(F, L, M, G).
filter([K|F], L, M, G) :-
    mem(L, K), !,
    filter(F, L, M, G).
filter([K|F], L, M, [K|G]) :-
    filter(F, L, M, G).

% sat(+ListOfLists, +List, -List)
sat([[L|_]|F], [L|V]):-
    M is -L,
    filter(F, L, M, G),
    sat(G, V).
sat([[L|K]|F], [M|V]):-
    K \== [],
    M is -L,
    filter(F, M, L, G),
    sat([K|G], V).
sat([], []).

Here is an example run for Joe Lehmanns test case:

?- sat([[1,-2],[-1,-2],[1,3]], X).
X = [1,-2] ;
X = [-1,-2,3] ;
No

Code inspired by https://gist.github.com/rla/4634264 .
I guess it is a variant of the DPLL algorithm now.

DaveEdelstein · Accepted Answer · 2011-02-10T15:17:15.430

1

i wish i had my prolog interpreter in front of me... but why cant you write a rule like

sat(Stmt) :-
  call(Stmt).

and then you would invoke your example by doing (btw ; is or)

?- sat(((A ; B), (B ; C))).

maybe you need something to constrain that they are either true or false so add these rules...

is_bool(true).
is_bool(false).

and querying

?- is_bool(A), is_bool(B), is_bool(C), sat(((A ; B), (B ; C))).

BTW -- this impl simply would simply be doing a DFS to find satisfying terms. no smart heuristic or anything.

edited Feb 10 '11 at 15:17

answered Feb 10 '11 at 15:02

DaveEdelstein

1,256
8
14

1

Instead of `sat(Stmt) :- call(Stmt).` you can just do `sat(Stmt) :- Stmt`. Using a variable as a goal is equivalent to `call/1` with the variable as the argument. – arnsholt Feb 10 '11 at 17:00
@arnsholt -- ahhh, i dont know why i didn't think to do that. that whole `sat/1` rule was superfluous anyway, i think it was just so it had a nice name. – DaveEdelstein Feb 10 '11 at 18:00
2

Very good suggestion! You can also directly map SAT instances to constraint problems over integers and use for example library(clpfd) in SICStus, SWI and YAP (and built-in constraints in other systems like GNU Prolog and B-Prolog) to solve them. The constraint solvers will generally be able to deduce more values and perform faster than such a simple (I do not mean that negatively!) search. SICStus also has a dedicated SAT constraint solver, library(clpb). – mat Feb 10 '11 at 18:18
@DaveEdelstein This solution works, and I've playing with it. I've been working to simplify the querying. I think the "is_bool(VAR), ..., is_bool(AnotherVar), sat((Clause);(AnotherClause))" querying gets very long with formulas that have many variables. So I'm using sat([ListOfVars], Stmnt) for querying, then the prolog algorithm goes trough the list of variables asigning a bool value shortening the querying and still mantaining the simplicity of your idea. – Diego Allen Feb 11 '11 at 18:13
@DavidEdelstein Another thing I noticed about this solution is that it repeats the same answer several times. For example, when querying **is_bool(X), is_bool(Y), is_bool(Z), sat(((X ; Y), (Y ; Z))).** it gives **X=true, Y=true, Z=true** four times before giving another solution. – Diego Allen Feb 11 '11 at 18:27
@dallen Not sure why its doing that. if you ran just this query: `is_bool(X), is_bool(Y), is_bool(Z)` and evaluated all its possibilities, it would show you 2^3=8 combos of X,Y,Z... – DaveEdelstein Feb 11 '11 at 21:39

Prolog SAT Solver

4 Answers4

Linked