pythonz3smtz3pypysmt

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


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

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.


Solution

  • Let's break down your goals:

    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:

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


    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.