prologboolean-logicclpb

Prolog SAT Solver

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).
Solution

  • 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.