Search code examples
prologclpclpb

Count solutions in a CSP

I'm using prolog and I have this code:

:- use_module(library(clpb)).

fun(A, B, C, D, E) :-
  sat(A + B + C + D),
  sat(E),
  labeling([A, B, C, D, E]).

If I want count all the solutions how can I do it? I've read about sat_count(+Expr, -Count) used in clpb but I'm not able to implement it without errors

Solution

  • Brute-force approach

    A straight-forward way to count the number of solutions is to generate them, and see how many there are.

    For example, with the program you posted, we can use findall/3 as follows to obtain the answer:

    ?- findall(., fun(A, B, C, D, E), Ls),
   length(Ls, L).
Ls = ['.', '.', '.', '.', '.', '.', '.', '.', '.'|...],
L = 15.

    Of course, this scales rather badly, and quickly becomes infeasible in more complex cases. Still, in this example, this strategy suffices.

    Alternative: sat_count/2

    With CLP(B), we have sat_count/2 that you have already discovered.

    The key advantage of sat_count/2 is that we can count the number of solutions without enumerating them. This is of course extremely handy when there are very many solutions.

    The trick for using sat_count/2 is to avoid labeling/1, and write your core relation in such a way that it only posts the constraints.

    For example:

    fun(A, B, C, D, E) :-
   sat(A + B + C + D),
   sat(E).

    This has several advantages. First of all, we can now query:

    ?- fun(A, B, C, D, E).
E = 1,
sat(A=\= ... # ... # B#B*C#B*C*D#B*D#C#C*D#D).

    This answer shows that E is necessarily 1! If we had used labeling/1, this would have been somewhat harder to see.

    Moreover, after posting the relevant constraints, we can use sat_count/2, by providing as the first argument a CLP(B) expression that must evaluate to truth.

    In our case, we do not want to put further constraints on the solution, so we specify as the first argument a tautology that contains the variables we are interested in. A suitable idiom for this is +[1|Vs].

    So, we can use:

    ?- fun(A, B, C, D, E),
   sat_count(+[1,A,B,C,D,E], Count).
E = 1,
Count = 15,
sat(A=\= ... # ... # B#B*C#B*C*D#B*D#C#C*D#D).

    Summary

    In this specific case, the number of solutions is so small that there is barely a difference between the two approaches.

    Still, I would like to stress an important general principle when writing constraint logic programs:

    It is good practice to separate the core relation from the actual search for solutions (labeling/1 and similar predicates, both built-in and manually written).

    If you honor this principle, you can study termination and propagation of the constraints in isolation.

    Moreover, this allows you to try out different search strategies without recompiling your program!