0

我有一组任意约束。例如：

A, B, C and D are 8-bit integers.

A + B + C + D = 50
(A + B) = 25
(C + D) = 30
A < 10

我可以将其转换为可以通过 picosat 解决的 SAT 问题（我无法让 minisat 在我的 Mac 上编译），或者转换为可以通过CVC4解决的 SMT 问题。为此，我需要：

  1. 将这些方程映射到布尔电路中。
  2. 将 Tseitin 变换应用于电路并将其转换为 DIMACS 格式。

我的问题：

  1. 我用什么工具来转换电路？
  2. 电路的文件格式有哪些，常用的有哪些？
  3. 我使用什么工具将电路转换为 DIMACS 格式？
4

3 回答 3

2

概念上

建立一个电路，然后应用 Tseitin 变换。

您需要将加法和比较运算符表示为布尔逻辑。有标准方法可以构建用于二进制补码加法和二进制补码比较的电路。

然后，使用 Tseitin 的转换将其转换为 SAT 实例。

在实践中

使用 SAT 前端将为您完成此转换。Z3 会为您解决这个问题。STP 也是如此。（这种转换有时被称为“位爆破”。）

于 2017-05-20T05:29:53.063 回答
1

在MiniZinc中，你可以只写一个约束编程模型：

set of int: I8 = 0..255;

var I8: A;
var I8: B;
var I8: C;
var I8: D;

constraint A + B + C + D == 50;

constraint (A + B) = 25;

constraint (C + D) = 30;

constraint A < 10;

solve satisfy;

示例约束不能满足，因为25 + 30 > 50.

Z3的 Python 接口将允许以下操作：

from z3 import *
A, B, C, D = Ints('A B C D')
s = Solver()
s.add(A >= 0, A < 256)
s.add(B >= 0, B < 256)
s.add(C >= 0, C < 256)
s.add(A+B+C+D == 50)
s.add((A+B) == 25)
s.add((C+D) == 30)
s.add(A < 10)
print(s.check())
print(s.model())
于 2018-11-18T23:32:26.790 回答
0

所以我有一个答案。有一个程序叫做Sugar：一个基于 SAT 的约束求解器，它将一系列约束作为 S 表达式，将整个事物转换为 DIMACS 文件，运行 SAT 求解器，然后将 SAT 求解器的结果转换回结果你的限制。

Sugar 由 Naoyuki Tamura 开发，用于解决数独难题等数学难题。我发现它使编写复杂约束的代码和运行它们变得非常简单。

例如，要找到 625 的平方根，可以这样做：

(int X 0 625)
(= (* X X) 625)

第一行说 X 的范围是 0 到 625。第二行说 X*X 是 625。

这可能不像 Z3 那样简单优雅，但它确实很好用。

于 2018-11-20T01:15:59.803 回答