Z3和DIMACS输出

Question

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

Answer 1

DIMACS格式非常原始,它只支持布尔变量.Z3并没有将每个问题都减少为SAT.使用命题SAT求解器解决了一些问题,但这不是规则.这通常仅在输入仅包含布尔和/或位向量变量时才会发生.此外,即使输入问题仅包含布尔和位向量变量,也无法保证Z3将使用纯SAT求解器来解决它.

话虽这么说,你可以使用战术框架来控制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