Блог

Я пытаюсь использовать Z3 через его интерфейс Python, чтобы вывести выполнимость простых линейных формул. Кажется, он довольно медленный даже для простых формул, таких как следующие (состоящие из 10 предложений по 10 терминов в каждом), которые я записываю в формате smt2:

 (declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(declare-fun x6 () Int)
(declare-fun x7 () Int)
(declare-fun x8 () Int)
(declare-fun x9 () Int)
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* 84 x0)) (* 48 x1)) (* 55 x2)) (* -46 x3)) (* -8 x4)) (* -12 x5)) (* 34 x6)) (* 35 x7)) (* -36 x8)) (* 99 x9)) 77))
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* -66 x0)) (* -13 x1)) (* -81 x2)) (* -88 x3)) (* -42 x4)) (* 57 x5)) (* 46 x6)) (* -9 x7)) (* -39 x8)) (* 18 x9)) 4))
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* -18 x0)) (* 93 x1)) (* 23 x2)) (* 25 x3)) (* 63 x4)) (* 47 x5)) (* -68 x6)) (* -25 x7)) (* 49 x8)) (* 14 x9)) 78))
(assert (<= (  (  (  (  (  (  (  (  (  (  0 (* -44 x0)) (* -89 x1)) (* -48 x2)) (* -25 x3)) (* 40 x4)) (* 84 x5)) (* 40 x6)) (* 52 x7)) (* -8 x8)) (* 66 x9)) 5))
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* 30 x0)) (* 29 x1)) (* 64 x2)) (* 18 x3)) (* 63 x4)) (* -94 x5)) (* 20 x6)) (* -30 x7)) (* 60 x8)) (* -35 x9)) 72))
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* 97 x0)) (* -90 x1)) (* 74 x2)) (* -51 x3)) (* 70 x4)) (* 41 x5)) (* 31 x6)) (* 99 x7)) (* -34 x8)) (* 36 x9)) 60))
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* 38 x0)) (* -11 x1)) (* -82 x2)) (* -59 x3)) (* 93 x4)) (* 2 x5)) (* 69 x6)) (* 86 x7)) (* -83 x8)) (* 49 x9)) 14))
(assert (<= (  (  (  (  (  (  (  (  (  (  0 (* -55 x0)) (* 50 x1)) (* -48 x2)) (* -27 x3)) (* -7 x4)) (* 86 x5)) (* -15 x6)) (* 96 x7)) (* -46 x8)) (* 11 x9)) 56))
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* 50 x0)) (* -51 x1)) (* -32 x2)) (* -23 x3)) (* -75 x4)) (* 24 x5)) (* 39 x6)) (* -89 x7)) (* 8 x8)) (* 23 x9)) 36))
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* -50 x0)) (* 98 x1)) (* 62 x2)) (* -39 x3)) (* -90 x4)) (* 19 x5)) (* -10 x6)) (* 32 x7)) (* -51 x8)) (* 52 x9)) 24))
(check-sat)
  

Я генерирую эти формулы динамически, используя следующий блок кода:
(Обратите внимание: формула — это список предложений; предложение — это список терминов, знак сравнения и свободный коэффициент; термин — это пара переменная-идентификатор (целое число), коэффициент переменной (целое число)).

 import z3
from pyCloSE.formula import LE, SAT, UNSAT, UNKNOWN

context = z3.Context()
solver = z3.SolverFor("QF_LIA", context)

# Define all variables as integers.
definitions = dict()
for variable in formula.getVariables():
    definitions[variable] = z3.Int("x{}".format(variable), context) 

# Create assertions.
constraints = []
for clause in formula.getClauses(): 
    terms = [term.getCoefficient() * definitions[term.getIndex()] for term in clause.getTerms()]
    sumOfTerms = reduce(lambda a,b: a b, terms)

    if clause.getComparison() == LE:
        constraints.append(sumOfTerms <= clause.getFreeCoefficient())
    else:
        constraints.append(sumOfTerms != clause.getFreeCoefficient())

solver.add(*constraints)
result = solver.check()
return result
  

Проблема, с которой я сталкиваюсь, заключается в том, что Z3 застрял на такой формуле. Похоже, он тоже застрял, когда я сохраняю его в файл с именем formula.smt2 и пытаюсь решить его с помощью команды bash Z3.

Версия решателя, который я использую, такова: Z3 версии 4.3.2

Является ли формат, который я использую, неудобным или это связано с Z3? Есть ли какой-нибудь трюк, который я мог бы использовать для ускорения процесса решения?

Как предположил Хуан Оспина, я попытался выяснить, какая часть формулы была сложной для решателя. Кажется, это следующее:

 (declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(declare-fun x6 () Int)
(declare-fun x7 () Int)
(declare-fun x8 () Int)
(declare-fun x9 () Int)
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* -18 x0)) (* 93 x1)) (* 23 x2)) (* 25 x3)) (* 63 x4)) (* 47 x5)) (* -68 x6)) (* -25 x7)) (* 49 x8)) (* 14 x9)) 78)) 
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* 30 x0)) (* 29 x1)) (* 64 x2)) (* 18 x3)) (* 63 x4)) (* -94 x5)) (* 20 x6)) (* -30 x7)) (* 60 x8)) (* -35 x9)) 72)) 
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* 97 x0)) (* -90 x1)) (* 74 x2)) (* -51 x3)) (* 70 x4)) (* 41 x5)) (* 31 x6)) (* 99 x7)) (* -34 x8)) (* 36 x9)) 60)) 
(assert (<= (  (  (  (  (  (  (  (  (  (  0 (* -55 x0)) (* 50 x1)) (* -48 x2)) (* -27 x3)) (* -7 x4)) (* 86 x5)) (* -15 x6)) (* 96 x7)) (* -46 x8)) (* 11 x9)) 56)) 
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* 50 x0)) (* -51 x1)) (* -32 x2)) (* -23 x3)) (* -75 x4)) (* 24 x5)) (* 39 x6)) (* -89 x7)) (* 8 x8)) (* 23 x9)) 36))
(assert (distinct (  (  (  (  (  (  (  (  (  (  0 (* -50 x0)) (* 98 x1)) (* 62 x2)) (* -39 x3)) (* -90 x4)) (* 19 x5)) (* -10 x6)) (* 32 x7)) (* -51 x8)) (* 52 x9)) 24))
  

На самом деле, если вы удалите какое-либо предложение из этой формулы, решатель сможет ответить менее чем за секунду, в то время как, если вы передадите ему всю формулу, у него закончится время.

Почему это происходит? Нормально ли, что Z3 считает эту формулу настолько сложной для решения?

С наилучшими пожеланиями, Андреа