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.

Answer 2

I don't think you can do this in general; that is, when you can have arbitrary constraints over arbitrary theories. You are asking a "meta"-question: "Maximize the number of models" is not a question about the problem itself, but rather about the models of the problem; something SMTLib cannot deal with.

Having said that, however, I think it should be possible to code it for specific problems. In the example you gave, the model space is maximized when a - b is the greatest; so you can simply write:

(set-option :produce-models true)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

(assert (< 5 a 10))
(assert (< 0 b  5))
(assert (< b c  a))

(maximize (- a b))
(check-sat)
(get-value (a b))

To which z3 responds:

sat
((a 9)
 (b 1))

as desired. Or, you can use the Python bindings:

from z3 import *

a, b, c = Ints('a b c')
o = Optimize()
o.add(And(5 < a, a < 10, 0 < b, b < 5, b < c, c < a))
o.maximize(a - b)

if o.check() == sat:
    m = o.model()
    print "a = %s, b = %s" % (m[a], m[b])
else:
    print "unsatisfiable or unknown"

which prints:

a = 9, b = 1

There are also bindings for C/C++/Java/Scala/Haskell etc. that let you do more or less the same from those hosts as well.

But the crucial point here is that we had to manually come up with the goal that maximizing a - b would solve the problem here. That step is something that needs human intervention as it applies to whatever your current problem is. (Imagine you're working with the theory of floats, or arbitrary data-types; coming up with such a measure might be impossible.) I don't think that part can be automated magically using traditional SMT solving. (Unless Patrick comes up with a clever encoding, he's quite clever that way!)