5

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.

repeat
  • 18,496
  • 4
  • 54
  • 166
Christoph Burschka
  • 4,467
  • 3
  • 16
  • 31
  • 1
    Please make your code self-contained, so that others can actually try it. – mat Dec 17 '15 at 20:44
  • Sorry, I edited in the rest of the code. – Christoph Burschka Dec 17 '15 at 23:17
  • 3
    One comment about the representation: You know that each such list has exactly 2 elements. In such cases, it is better to use terms like `x=0`, `x=1` to represent the bindings more compactly: `[x,0]` is `.(x, .(0, [])`, wasting space for one additional functor `./2` and one atom `[]` for each such structure. In contrast, `x=0` is `=(x,0)`, i.e., just one functor and its two arguments. As others have said though, you can actually delegate the binding to Prolog easily by using actual logical variables instead. You can store a symbol/variable correspondence instead of a variable/value one! – mat Dec 18 '15 at 07:41

3 Answers3

3

Use !

:- 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.
repeat
  • 18,496
  • 4
  • 54
  • 166
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).
Christoph Burschka
  • 4,467
  • 3
  • 16
  • 31
  • 2
    I feel like `generate_model/2` resembles [`term_variables/2`](http://www.swi-prolog.org/pldoc/man?predicate=term_variables/2) a lot, am I missing something? – Daniel Lyons Dec 17 '15 at 20:39
  • 1
    @DanielLyons. I concur. It does. `term_variables/2` plus some suitable `maplist/3`... Directly using logical variables would be more idiomatic (and quite likely a lot faster). Also, it would safeguard against using `F` like `[[x,0],[x,1],...]` (which is bad!) – repeat Dec 17 '15 at 22:07
  • Oooh, that's neat! Though in this specific case the formula itself doesn't contain real Prolog variables - each "variable" is represented by an atomic term (usually a string). My `var_list` predicate then lists unique atoms the same way that `term_variables` lists variables. – Christoph Burschka Dec 17 '15 at 22:17
  • 1
    And yeah, I guess logical variables would be better in this case - but most of the stuff we're doing is symbol manipulation and not evaluation. I needed this to automatically check equisatisfiability to verify the correctness of some Tseytin implementations. – Christoph Burschka Dec 17 '15 at 22:27
  • 4
    If your semantics are similar enough to Prolog's, you could allow it to do the lifting for you though. :) – Daniel Lyons Dec 17 '15 at 23:16
-1

Do I understand you, that you are happy with a single model. You don't need labeling or sat_count. Here is an alternative model finder, that is similar to yours, but will only return consistent models.

Since it finds counter models, you need to supply the negation of the formula to find a model. The predicate maze/3 was developed as a negative implementation of the positive predicate proof/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).

It can find counter models to all of the following fallacies:

Affirming a Disjunct: (p v q) & 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 run:

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 the thing is much faster than CLP(B). Here are some timings running the same problem in CLP(B) and with 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