Using SMT-LIB to count the number of modules using a formula

Question

I am not sure that this is possible using SMT-LIB, if it is not possible does an alternative solver exist that can do it?

Consider the equations

• a < 10 and a > 5
• b < 5 and b > 0
• b < c < a
• with a, b and c integers

The values for a and b where the maximum number of model exist that satisfy the equations when a=9 and b=1.

Do SMT-LIB support the following: For each values of a and b count the number of models that satisfy the formulas and give the value for a and b that maximize the count.

Answer 1

Let's break down your goals:

• You want to enumerate all possible ways in which a and b (...and more) can be assigned
• For each combination, you want to count the number of satisfiable models

In general, this is not possible, as the domain of some variables in the problem might contain an infinite number of elements.

Even when one can safely assume that the domain of every other variable contains a finite number of elements, it is still highly inefficient. For instance, if you had only Boolean variables in your problem, you would still have an exponential number of combination of values --and therefore candidate models-- to consider along the search.

However, it is also possible that your actual application is not that complex in practice, and therefore it can be handled by an SMT Solver.

The general idea could be to use some SMT Solver API and proceed as follows:

• assert the whole formula
• repeat until finish combinations of values:
  • push a back-track point
  • assert one specific combination of values, e.g. a = 8 and b = 2
  • repeat forever:
    • check for a solution
    • if UNSAT, exit the inner-most loop
    • if SAT, increase counter of models for the given combination of values of a and b
    • take the model value of any other variable, e.g. c = 5 and d = 6
    • assert a new constraint requesting that at least one of the "other" variables changes its value, e.g. c != 5 or d != 6
  • pop backtrack point

Alternatively, you may enumerate the possible assignments over a and b implicitly rather than explicitly. The idea would be as follows:

• assert the whole formula
• repeat forver:
  • check for a solution
  • if UNSAT, exit loop
  • if SAT, take the combination of values of your control variables from the model (e.g. a = 8 and b = 2), check in an internal map if you encountered this combination before, if not set the counter to 1, otherwise increase the counter by 1.
  • take the model value of any other variable, e.g. c = 5 and d = 6
  • assert a new constraint requesting for a new solution, e.g. a != 8 or b != 2 or c != 5 or d != 6

---

In the case that you are in doubt on which SMT Solver to pick, I would advice you to start solving your task with pysmt, which allows one to choose among several SMT engines with ease.

---

If for your application an explicit enumeration of models is too slow to be practical, then I would advice you to look at the vast literature on Counting Solutions of CSPs, where this problem has already been tackled and there seem to exist several ways to approximately estimate the number of solutions of CSPs.