Counting the number of valuations via Quine algorithm in Prolog

Question

My logic teacher said in passing that Quines algorithm can be also used to count valuations. Unfortunately I cannot get my head around how this is done in Prolog?

The program would for example give, using
the syntax from the answer in Quines algorithm:

?- sat_count(X+Y, C).
C = 3

Since the truth table for the disjunction X+Y
has 3 rows that valuate to true:

X   Y   X+Y
0   0   0
0   1   1
1   0   1
1   1   1

Answer 1

Point of departure is Quines algorithm with its core predicate eval/2 which has the following specification. The source code of the Quine algorithm and the solution to the question can be found here.

/**
 * eval(A, R):
 * The predicate succeeds in R with a partial evaluated
 * Boolean formula. The predicate starts with the leaves
 * and calls simp after forming new nodes.
 */
% eval(+Formula, -Formula)

We first experimented with a labeling predicate, that will list all valuations without counting them. The predicate has a fast fail feature, if the partially evaluated formula is false (0) then labeling needs not to proceed, otherwise we simply probe the boolean values:

/**
 * labeling(L, A):
 * The predicate labels the variables from the list L in the formula A.
 */
% labeling(+List, +Formula)
labeling(_, A) :- A == 0, !, fail.
labeling([X|L], A) :- value(X), eval(A, B), labeling(L, B).
labeling([], A) :- A == 1.

Here is an example run:

?- labeling([X,Y], X+Y).
X = 0,
Y = 1 ;
X = 1,
Y = 0 ;
X = 1,
Y = 1

From the labeling predicate we derived a counting predicate using findall/3 from the ISO core standard. Instead of succeeding at the end we return 1, inbetween we sum the counts. This does the job and also profits from fast failing:

/**
 * count(L, A, N):
 * The predicate silently labels the variables from the list L in the
 * formula A and succeeds in N with the count of the solutions.
 */
% count(+List, +Formula, -Integer)
count(_, A, C) :- A == 0, !, C = 0.
count([X|L], A, D) :-
   findall(C, (value(X), eval(A, B), count(L, B, C)), R),
   sum(R, 0, D).
count([], A, 1) :- A == 1.

Here is an example run:

?- count([X,Y], X+Y, C).
C = 3

The implementation might profit from some optimizations that we didn't implement. For example assigning values to a variable that does not anymore occure in the formula could be optimized away.