Brute-force Prolog SAT solver for boolean formulas

Question

I'm trying to write an algorithm that naively looks for models of a boolean formula (NNF, but not CNF).

The code I have can check an existing model, but it'll fail (or not finish) when asked to find models, seemingly because it generates infinitely many solutions for member(X, Y) along the lines of [X|_], [_,X|_], [_,_,X|_]...

What I have so far is this:

:- op(100, fy, ~).    
:- op(200, xfx, /\).  
:- op(200, xfx, \/).  
:- op(300, xfx, =>).  
:- op(300, xfx, <=>). 

formula(X) :- atom(X).
formula(~X) :- formula(X).
formula(X /\ Y) :- formula(X), formula(Y).
formula(X \/ Y) :- formula(X), formula(Y).
formula(X => Y) :- formula(X), formula(Y).
formula(X <=> Y) :- formula(X), formula(Y).

model(1, _).
model(X, F) :- atom(X), member([X, 1], F).
model(~X, F) :- atom(X), member([X, 0], F). % NNF
model(A /\ B, F) :- model(A, F), model(B, F).
model(A \/ B, F) :- (model(A, F); model(B, F)).
model(A => B, F) :- model(~A \/ B, F).
model(A <=> B, F) :- model((A => B) /\ (B => A), F).

sat(A) :- model(A, F), \+ (member([X, 1], F), member([X, 0], F)).


%%% examples:
% formula(~(~ (a /\ b) \/ (c => d))).
% model(a, [[a,1]]).

Is there a better data structure for F, or some other way the partially-instantiated lists can be cut off?

Edit: Added definitions and examples.

Answer 1

I solved it by writing a generate_model predicate that created a pre-defined list with exactly one element for each variable:

generate_model([], []).
generate_model([X|T], [[X,_]|T2]) :- generate_model(T, T2).

sat(A) :- 
  var_list(A, Vars),
  generate_model(Vars, F),
  model(A, F).

Answer 2

Use clpb!

:- use_module(library(clpb)).

Sample query using sat/1:

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

Some variables (A and B) already have been bound to exactly one Boolean value (in above query), but search is not yet complete (which is indicated by residual goals).

To trigger the smart brute-force enumeration of all solutions use labeling/1 like so:

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