Z3和DIMACS输出(Z3 and DIMACS output)

Z3目前支持的输入格式DIMACS。 有没有什么办法来输出解决之前的问题DIMACS格式？ 我的意思是这个问题转变为系统的CNF并输出在DIMACS格式。 如果没有，朝着这个方向的任何想法将多于帮助。

Answer 1:

该DIMACS格式是非常原始的，它仅支持布尔变量。 Z3并没有减少每一个问题到周六 有些问题用的是命题求解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

Answer 2:

由于莱昂纳多的答案，我想出了这个代码，将你想要做什么：

private static void Output(Context ctx,Solver slv)
{
    var goal = ctx.MkGoal();
    goal.Add(slv.Assertions);
    var applyResult = ctx.Then(ctx.MkTactic("simplify"),
        ctx.MkTactic("bit-blast"),
        ctx.MkTactic("tseitin-cnf")).Apply(goal);

    Debug.Assert(applyResult.Subgoals.Length==1);

    var map = new Dictionary<BoolExpr,int>();
    foreach (var f in applyResult.Subgoals[0].Formulas)
    {
        Debug.Assert(f.IsOr);
        foreach (var e in f.Args)
            if (e.IsNot)
            {
                Debug.Assert(e.Args.Length==1);
                Debug.Assert(e.Args[0].IsConst);
                map[(BoolExpr)e.Args[0]] = 0;
            }
            else
            {
                Debug.Assert(e.IsConst);
                map[(BoolExpr)e] = 0;
            }
    }

    var id = 1;
    foreach (var key in map.Keys.ToArray())
        map[key] = id++;

    using (var fos = File.CreateText("problem.cnf"))
    {
        fos.WriteLine("c DIMACS file format");
        fos.WriteLine($"p cnf {map.Count} {applyResult.Subgoals[0].Formulas.Length}");
        foreach(var f in applyResult.Subgoals[0].Formulas)
        {
            foreach (var e in f.Args)
                if (e.IsNot)
                    fos.Write($"{map[(BoolExpr)e.Args[0]]} ");
                else
                    fos.Write($"-{map[(BoolExpr)e]} ");

            fos.WriteLine("0");
        }
    }
}

它的工作，你应该所有的约束添加到直接求解器，通过调用slv.Assert(...)

文章来源: Z3 and DIMACS output