Prolog SAT Local Algorithm for Boolean Formulas

Question

I am trying to write an algorithm that naively searches for Boolean formula models (NNF, but not CNF).

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

What I still know:

 :- 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 in some other way partially edited lists can be trimmed?

Edit: Added definitions and examples.

Answer 1

Use clpb !

<Preview>: use_module ( library (clpb) ).

Example request using sat/1 :

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

Some variables ( A and B ) are already tied to one Boolean value (in the previous query), but the search has not yet been completed (which is indicated by residual goals).

To start enumerating smart iterators of all solutions, use labeling/1 like this:

<Preview>? - 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.

Answer 2

I solved this by writing the generate_model predicate, which created a predefined 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 3

I understand that you are satisfied with one model. You do not need marking or sat_count. Here is an alternative model search that is similar to yours but will only return consistent models.

Since it finds counter models, you need to provide a negation of the formula to search for the model. The predicate labyrinth / 3 was designed as a negative realization of the positive evidence for predicate / 2:

 % Find a counter model. % maze(+Norm,+List,-List) maze(or(A,_),L,_) :- member(A,L), !, fail. maze(or(A,B),L,R) :- !, inv(A,C), maze(B,[C|L],R). maze(and(A,_),L,R) :- maze(A,L,R), !. maze(and(_,B),L,R) :- !, maze(B,L,R). maze(A,L,_) :- member(A,L), !, fail. maze(A,L,M) :- oneof(L,B,R), connective(B), !, inv(A,C), inv(B,D), maze(D,[C|R],M). maze(A,L,[B|L]) :- inv(A,B). 

He can find counter models for all of the following errors:

 Affirming a Disjunct: (pvq) & p => ~q. Affirming the Consequent: (p => q) & q => p. Commutation of Conditionals: (p => q) => (q => p). Denying a Conjunct: ~(p & q) & ~p => q. Denying the Antecedent: (p => q) & ~p => ~q. Improper Transposition: (p => q) => (~p => ~q). 

Here is an example of execution:

 Jekejeke Prolog 2, Runtime Library 1.2.5 (c) 1985-2017, XLOG Technologies GmbH, Switzerland ?- negcase(_,N,F), norm(F,G), maze(G,[],L), write(N), write(': '), sort(L,R), write(R), nl, fail; true. Affirming a Disjunct: [pos(p),pos(q)] Affirming the Consequent: [neg(p),pos(q)] Commutation of Conditionals: [neg(p),pos(q)] Denying a Conjunct: [neg(p),neg(q)] Denying the Antecedent: [neg(p),pos(q)] Improper Transposition: [neg(p),pos(q)] 

Interestingly, things are much faster than CLP (B). Here are some timings that perform the same problem in CLP (B) and with a maze:

 ?- time((between(1,1000,_), negcaseclp(_,N,F,L), sat(~F), once(labeling(L)), fail; true)). % Up 296 ms, GC 3 ms, Thread Cpu 250 ms (Current 01/27/18 00:34:20) Yes ?- time((between(1,1000,_), negcase(_,_,F), norm(F,G), maze(G,[],_), fail; true)). % Up 82 ms, GC 0 ms, Thread Cpu 78 ms (Current 01/27/18 00:30:21) Yes