Z3 目前支持 DIMACS 格式的输入。有没有办法在解决之前为问题输出 DIMACS 格式?我的意思是将问题转换为系统 CNF 并以 DIMACS 格式输出。如果没有,任何朝着这个方向发展的想法都会很有帮助。
问问题
2564 次
2 回答
8
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
于 2012-10-25T00:29:07.973 回答
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(...)
。
于 2016-10-11T14:20:33.007 回答