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.
Use clpb!
Sample query using
sat/1
:Some variables (
A
andB
) 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: