How to Perform QSAT Count in Prolog

Question

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-Y-Z), nl, fail; true.
0-1-1
1-0-0
1-0-1
1-1-0
1-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?

question from:https://stackoverflow.com/questions/65853428/how-to-perform-qsat-count-in-prolog

Answer 1

Waitting for answers