Z3 和 DIMACS 输出

Question

Z3 目前支持 DIMACS 格式的输入。有没有办法在解决之前输出问题的DIMACS格式？我的意思是将问题转换为系统 CNF 并以 DIMACS 格式输出。
如果没有，任何朝这个方向发展的想法都会很有帮助。

Answer 1

DIMACS 格式非常原始，它只支持 bool 变量。 Z3 不会将所有问题都简化为 SAT。有些问题是使用命题 SAT 求解器解决的，但这不是规则。这通常仅在输入仅包含 bool 和/或位向量变量时才会发生。而且，即使输入问题只包含 bool 和位向量变量，也不能保证 Z3 会使用纯 SAT 求解器来解决它。

话虽如此，您可以使用 tactic framework控制Z3。例如，对于位向量问题，以下策略会将其转换为 CNF 格式的命题公式。将其转换为 DIMACS 应该很简单。这是示例。您可以在线试用:http://rise4fun.com/Z3Py/E1s

x, y, z = BitVecs('x y z', 16)
g = Goal()
g.add(x == y, z > If(x < 0, x, -x))
print g
# t is a tactic that reduces a Bit-vector problem into propositional CNF
t = Then('simplify', 'bit-blast', 'tseitin-cnf')
subgoal = t(g)
assert len(subgoal) == 1
# Traverse each clause of the first subgoal
for c in subgoal[0]:
  print c