Z3 中带乘法的 Horn 子句

Question

我刚刚开始深入研究 Z3 的定点求解器，并且编写了一个示例，该示例在使用乘法时挂起，但在将乘法定义为一系列加法时完成。由于我刚开始使用 Horn 子句，所以这里可能有些地方我没有弄明白。 "native" 乘法如此缓慢，而定义为一系列加法的乘法在合理的时间范围内产生令人满意的结果，这是有原因的吗？谢谢！

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）。

我不完全确定定点引擎在这里是如何发挥作用的，但以上内容适用于一般查询；我猜同样的推理也适用。

话虽如此，Z3 确实有一个非线性算术求解器，称为 nlsat。你可能想试一试，但我不会屏住呼吸。请参阅有关如何触发它的问题：

NB. 我不确定是否可以通过 Python 使用 FixedPoint 引擎中的 nlsat 引擎，所以你可能有做一些挖掘，找出正确的咒语是什么，如果可以的话。

Z3 中带乘法的 Horn 子句

Horn clauses with multiplication in Z3

z3

z3py

fixed-point-iteration

z3-fixedpoint