sat-solvers

3热度

2回答

我正在使用Z3 Python接口为我的实验创建公式。然后我将这个公式发送给Z3解算器。如果我是正确的Z3使用它自己的求解器！如何在Z3py中使用不同的SAT/SMT解算器？我在CBMC（C有界模型检查器）中使用它的方式：运行程序并吐出中间DIMAC表示（在文件中），然后将该文件用作其他SAT求解器的输入。我可以在Z3做类似的事情吗？谢谢。

0热度

1回答

关于sat4j，如何使用sat4j来解决伪布尔问题？

我有伪布尔问题，我需要用sat4j来解决它。有人可以帮助我吗？这里是我的问题：我有一个名为的变量列表：A，B，C，d，E，F 而且我所代表的值的列表：＃ 1，＃2，＃3 ..... H（A，＃1）是指分配＃1到我有一些实施例C onstraints： h(a,#1)=1 h(a,#1)+h(b,#1)+h(c,#1)=1 h(a,#1)+h(a,#5)>=1 h(b,#2)+h(b,

0热度

1回答

/usr/bin/ld：找不到-lcplex

我试图从这个git repo设置MaxHS SAT求解器 - https://github.com/fbacchus/MaxHS。我得到一个错误，说'/ usr/bin/ld：can not find -lcplex'。任何人都可以指导我什么是lcplex库和如何解决这个问题？我的控制台看起来像这样.. install -d /mnt/c/Akhil/Abhyas/CQA/maxhs_ins

2热度

1回答

MiniSat中的非决策变量的语义是什么？

当使用MiniSat作为C++库时，每个新变量都可以创建为决策变量或非决策变量。我对此的粗略理解是，当解算器决定在分支期间使用下一个变量时，不考虑非决策变量。然而，在我的项目中，当非决策变量位于蕴含的左侧时，我遇到了麻烦，而不是等价关系，因为求解器返回了SAT，即使公式实际上是UNSAT。进一步的实验表明，只有当非决策变量在一个长于2个变量的公式中时才会出现这种情况（我认为2变量公式路径是解算

1热度

1回答

从CNF转换为喇叭形式

如何使用Prolog将CNF子句转换为喇叭形式？我正在尝试创建一个将CNF作为输入的SAT求解器，这将需要转换为喇叭形式。

1热度

1回答

在Z3中将函数作为属性的数据类型Python

我正在使用Z3的Python绑定，并尝试创建属性为函数的Z3数据类型。例如，我可以执行以下命令： Foo = Datatype('Foo') Foo.declare('foo', [('my_function', Function('f', IntSort(), BoolSort()))]) Foo.create() 这是试图建立一个数据类型Foo与属性my_function，在那里我将能

4热度

1回答

增量式SMT解算器具有降低特定约束的能力

是否有增量式SMT解算器或某些增量式SMT解算器的API，我可以在其中增量添加约束，我可以通过某些标签/名称唯一标识每个约束？我想唯一标识约束的原因是我可以稍后通过指定该标签/名称来放弃它们。需要放弃约束是因为我早先的约束与时间无关。我看到，与Z3我不能使用基于推/弹出的增量方法，因为它遵循基于堆栈的想法，而我的要求是放弃特定的早期/旧约束。随着Z3基于假设的其他增量方法，我将不得不执行格

1热度

1回答

使用Z3和c＃

获取不稳定的核心示例我想在C＃实现中使用Z3坐标解算器。此代码非常接近Microsoft本身在“http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs”中给出的示例。我的代码是： using (Context ctx = new Context(new Dictionary<string, string>() {

1热度

2回答

用多种假设求解

假设我有一个变量(a,b,c,d,e,f,g)的CNF表达式。考虑到{a,b,c,g} = {1,0,0,1}和{a,b,c,g} = {1,1,1,1}，如何使用SAT解算器找到(d,e,f)的作业？如果这是一个假设，那么调用坐标求解器来寻找{d,e,f}的分配将是直接的（例如，通过向CNF添加单位子句）。但是如果我有多重假设呢？这可能吗？

1热度

1回答

使用命题逻辑求解方程

我正在寻找关于如何将数学方程式编码为cnf-sat形式的想法，以便他们可以通过像MiniSat这样的开源SAT求解器来解决。所以，我怎么转换是这样的： 3X + 4Y - Z = 14 -2x - 4Z < = -6 X - 3Y + Z> = 15 成为可以通过使用SAT求解器求解的命题式。任何建议，因为我很难过？