Роговые предложения с умножением в Z3

Question

Я только начал копаться в решателе с фиксированной запятой в Z3 и подготовил пример, который зависает при использовании умножения, но завершается при определении умножения как серии дополнений. Поскольку я новичок в работе с клаузлами Хорна, может быть что-то, чего я здесь не понимаю. Есть ли причина, по которой "собственное" умножение является таким медленным, тогда как умножение, определенное как серия сложений, дает удовлетворительный результат в разумные сроки? Спасибо!

def test_mseq_hangs():
  mul = Function('mul', IntSort(), IntSort(), IntSort(), BoolSort())
  mc = Function('mc', IntSort(), IntSort(), BoolSort())
  n, m, p = Ints('m n p')

  fp = Fixedpoint()

  fp.declare_var(n,m,p)
  fp.register_relation(mc, mul)

  fp.fact(mul(m, n, m * n))
  fp.rule(mc(m, 1), m <= 1)
  fp.rule(mc(m, n), [m > 1 , mc(m-1, p), mul(m, p, n)])

  assert fp.query(And(mc(m,n),n < 1)) == unsat
  assert fp.query(And(mc(m,n),n < 2)) == sat
  assert fp.query(And(mc(m,n),n > 100 )) == sat
  assert fp.query(mc(5,120)) == sat
  assert fp.query(mc(5,24)) == unsat

def test_mseq():
  mul = Function('mul', IntSort(), IntSort(), IntSort(), BoolSort())
  add = Function('add', IntSort(), IntSort(), IntSort(), BoolSort())
  neg = Function('neg', IntSort(), IntSort(), BoolSort())
  mc = Function('mc', IntSort(), IntSort(), BoolSort())
  n, m, p, o = Ints('m n p o')

  fp = Fixedpoint()

  fp.declare_var(n,m,p,o)
  fp.register_relation(mc, add, mul, neg)

  fp.fact(add(m, n, m + n))
  fp.fact(neg(m, -m))
  fp.rule(mul(m, n, 0), n == 0)
  fp.rule(mul(m, n, m), n == 1)
  fp.rule(mul(m, n, o), [n < 0, mul(m,n,p), neg(p,o)])
  fp.rule(mul(m, n, o), [n > 1, mul(m,n-1,p), add(m,p,o)])
  fp.rule(mc(m, 1), m <= 1)
  fp.rule(mc(m, n), [m > 1 , mc(m-1, p), mul(m, p, n)])

  assert fp.query(And(mc(m,n),n < 1)) == unsat
  assert fp.query(And(mc(m,n),n < 2)) == sat
  assert fp.query(And(mc(m,n),n > 100 )) == sat
  assert fp.query(mc(5,120)) == sat
  assert fp.query(mc(5,24)) == unsat

Answer 1

Это не очень удивительно, поскольку умножение переменных приводит к нелинейной арифметике, в то время как повторное сложение оставляет ее в линейном фрагменте. Нелинейная арифметика не разрешима, в то время как существуют эффективные процедуры принятия решения (такие как Presburger) для линейного фрагмента.

Я не совсем уверен, как движок Fixed-Point вступает в игру здесь, но вышеизложенное относится и к общим запросам; Я предполагаю, что те же самые рассуждения применимы.

Сказав это, Z3 имеет нелинейный арифметический решатель, называемый nlsat, Возможно, вы захотите попробовать, хотя я не задерживаю дыхание. Посмотрите этот вопрос о том, как его вызвать: (check-sat) затем (check-sat-using qfnra-nlsat)

NB. Я не уверен, возможно ли использовать nlsat Тем не менее, движок от FixedPoint через Python, поэтому вам, возможно, придется покопаться, чтобы узнать, каким будет правильное заклинание, если возможно начать с него.