Challenging CLP(B) Once More: A maze/3 Predicate

[burs...@gmail.com]

Dear All,

CLP(B) seems to be clever for labeling and sat_count.
But what if we are just happy with a single counter model?

Here is such a test case:

?- listing(negcaseclp/4).

negcaseclp('1', 'Affirming a Disjunct', (P+Q)*P=< ~Q, [P,Q]).
negcaseclp('2', 'Affirming the Consequent', (P=<Q)*Q=<P, [P,Q]).
negcaseclp('3', 'Commutation of Conditionals', (P=<Q)=<(Q=<P), [P,Q]).
negcaseclp('4', 'Denying a Conjunct', ~ (P*Q)* ~P=<Q, [P,Q]).
negcaseclp('5', 'Denying the Antecedent', (P=<Q)* ~P=< ~Q, [P,Q]).
negcaseclp('6', 'Improper Transposition', (P=<Q)=<(~P=< ~Q), [P,Q]).

And here are some measurements with different CLP(B) libraries.
To find counter models for all of the above fallacies. The tests
were done on the same maschine:

With Jekejeke Prolog and its Minlog Extension:

Jekejeke Prolog 2, Runtime Library 1.2.5
(c) 1985-2017, XLOG Technologies GmbH, Switzerland

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

With SWI-Prolog:

Welcome to SWI-Prolog (threaded, 64 bits, version 7.7.8)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

?- time((between(1,1000,_), negcaseclp(_,N,F,L),
sat(~F), once(labeling(L)), fail; true)).
% 7,461,001 inferences, 0.750 CPU in 0.772 seconds (97% CPU, 9948001 Lips)
true.

Are these timings good? Not at all. Here is a new
approach, a maze finder. Inspired by Son of BirdBrain II
https://www.cs.unm.edu/~mccune/sobb2/ .

We get the following timing:

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

https://stackoverflow.com/a/48470870/502187

Unfortunately we only have started testing today. Not
yet sure whether this scales to more variables, etc..

Also it would be possible to implement a maze/2 predicate
without showing the found counter model, just saying yes/no.

[Mostowski Collapse]

Interestingly some CLP(B) library use the (^)/2 operator for
existential quantifier. But the existential quantifier does not
get consideration it would deserve in sat_count/2.

Take these two examples:

?- sat(X+Y*Z), labeling([X,Y,Z]), write(X-Z), nl, fail; true.
0-1
1-0
1-1
1-0
1-1
?- sat(Y^(X+Y*Z)), labeling([X,Z]), write(X-Z), nl, fail; true.
0-1
1-0
1-1

The counts are 5 and 3. For the later count, I only get the correct
result by correcting the result of sat_count/2 via a division by two:

?- sat_count(X+Y*Z, N).
N = 5.
?- sat_count(Y^(X+Y*Z), N), M is N//2.
N = 6,
M = 3.

Are there CLP(B) implementations around that behave differently?

[Mostowski Collapse]

Corr.:

?- sat(X+Y*Z), labeling([X,Y,Z]), write(X-Y-Z), nl, fail; true.
0-1-1
1-0-0
1-0-1
1-1-0
1-1-1