Z3 和 DIMACS 输出 [英] Z3 and DIMACS output

问题描述

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

Z3 currently supports the DIMACS format for input. Is there any way to output the DIMACS format for the problem before solution? I mean converting the problem to a system CNFs and output it in a DIMACS format. If not, any ideas towards this direction would be more than helpful.

推荐答案

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

The DIMACS format is very primitive, it supports only Boolean variables. Z3 does not reduce every problem into SAT. Some problems are solved using a propositional SAT solver, but this is not the rule. This usually only happens if the input contains only Boolean and/or Bit-vector variables. Moreover, even if the input problem contains only Boolean and Bit-vector variables, there is no guarantee that Z3 will use a pure SAT solver to solve it.

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

That being said, you can use the tactic framework to control Z3. For example, for Bit-vector problems, the following tactic will convert it into a propositional formula in CNF format. It should be straightforward to convert it into DIMACS. Here is the example. You can try it online at: 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

这篇关于Z3 和 DIMACS 输出的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！