使用 SMT-LIB 使用公式计算模块数量 [英] Using SMT-LIB to count the number of modules using a formula

问题描述

我不确定使用 SMT-LIB 是否可行，如果不可能，是否存在可以做到的替代求解器?

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?

考虑方程

• a <10 和 a >5
• b <5 和 b >0
• b <＜一个
• 使用a、b 和c 整数

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

a 和 b 的值，其中存在最大模型数，满足 a=9 和 b 时的方程=1.

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

SMT-LIB 是否支持以下内容:对于 a 和 b 的每个值，计算满足公式的模型数量并给出 a 的值 和 b 使计数最大化.

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.

推荐答案

让我们分解你的目标:

• 您想列举所有可能的方式来分配 a 和 b (...and more)
• 对于每个组合，您要计算可满足模型的数量

一般来说，这是不可能的，因为问题中某些变量的域可能包含无限多个元素.

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.

但是，也有可能您的实际应用在实践中并不那么复杂，因此它可以由 SMT Solver 处理.

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.

总体思路可能是使用一些SMT Solver API并按以下步骤进行:

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

• assert 整个公式
• 重复直到完成值的组合:
  • push一个回溯点
  • assert 一种特定的值组合，例如a = 8 和 b = 2
  • 永远重复:
    • 检查解决方案
    • 如果UNSAT，退出最内层循环
    • 如果SAT，增加给定a和b
    值组合的模型计数器
    • 取任何其他变量的模型值，例如c = 5 和 d = 6
    • assert 一个新的约束，要求至少一个 "other" 变量改变它的值，例如c != 5 或 d != 6
    • 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

        或者，您可以隐式地而不是显式地枚举 a 和 b 上可能的赋值.思路如下:

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

        • assert 整个公式
        • 永远重复:
          • 检查寻找解决方案
          • 如果UNSAT，退出循环
          • 如果SAT，从模型中获取控制变量值的组合(例如a = 8 and b = 2)，如果你之前遇到过这个组合，如果没有将计数器设置为1，否则将计数器增加1.
          • 取任何其他变量的模型值，例如c = 5 和 d = 6
          • assert 请求新解决方案的新约束，例如a != 8 or b != 2 or c != 5 or d != 6
          • 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

            如果您不确定选择哪个 SMT Solver，我建议您开始使用 pysmt，它允许您轻松地在多个SMT 引擎中进行选择.

            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.

            如果对于您的应用程序，模型的显式枚举太慢而无法实用，那么我建议您查看关于CSP 计数解决方案的大量文献，该问题已经得到解决并且似乎有几种方法可以近似估计 CSP 的解数.

            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.

            这篇关于使用 SMT-LIB 使用公式计算模块数量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！