z3 - 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