找出哪些值满足布尔公式

Question

我有以下布尔表达式 x > 5 和 y > 10

C:\>python Python 3.6.1 (v3.6.1:69c0db5, Mar 21 2017, 18:41:36)Type "help", "copyright", "credits" or "license" for more information.
>>> x = 3
>>> y = 11
>>> eval("x>5 and y > 10") False
>>> x = 6
>>> eval("x>5 and y > 10") True
>>>

当 x > 5 且 y > 10 时，计算公式计算为 "true"。

当 x == 6 且 y == 5 时，公式计算结果为 "false"，因为 y < 10。

想知道有没有library/software（以python为例，语言不是问题）可以回答调用者哪些值满足公式。

Answer 1

SMT 求解器很适合这个要求。这是使用 Python 绑定到 z3 编码的问题：

from z3 import *

def getResult (s):
  r = s.check()
  if r == sat:
     print True
     print s.model()
  elif r == unsat:
     print False
  elif r == unknown:
     print "Solver said unknown!"
  else:
     print "Unexpected result!"
     print r

x, y = Ints('x y')

s1 = Solver()
s1.add(x == 3)
s1.add(y == 11)
s1.add (x > 5)
s1.add (y > 10)
getResult(s1)

s2 = Solver()
s2.add (x == 6)
s2.add (y == 11)
s2.add (x > 5)
s2.add (y > 10)
getResult (s2)

当运行时，打印：

False
True
[y = 11, x = 6]

当然，这是一个相当愚蠢的例子；您根本不必指定 x 和 y 的值；如果你不这样做，z3 会给你一些满足约束的值。

在此处阅读有关 z3 的更多信息：https://rise4fun.com/z3/tutorial

在此处阅读有关 SMT 求解的更多信息：http://smtlib.cs.uiowa.edu/

z3 是开源的，下载地址：https://github.com/Z3Prover/z3

z3 可以用多种语言编写脚本； SMTLib/C/C++/Java/Python/Scala 甚至 Haskell。一般来说，语言越高级，界面越容易使用。

找出哪些值满足布尔公式

find which values satisfy a boolean formula

python

boolean-expression

sat