Найти, какие значения удовлетворяют булевой формуле

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, оценка является формулой, оцениваемой как "истина".

Когда x == 6 и y == 5 формула оценивается как "ложная", потому что y < 10.

Я хотел бы знать, есть ли библиотека / программное обеспечение (в качестве примера используется 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. Чем выше уровень языка, тем проще использовать интерфейс.