Lib.rs

cnfgen-nand-opt

此程序可以生成CNF（合取范式）以检查基于NAND或NOR门构建的电路是否能从表中返回给定值。

警告：对于某些更大的示例，此程序可以生成超过1GB的CNF。

此程序可以从文件中读取问题。如果没有指定文件，则程序从标准输入读取问题。输入格式为TOML格式。

gate = "Nand"
layers = 5
max_gates = 18
table = [ 6, 62, 11, 17, 26, 47, 53, 35 ]

gate字段是门类型 - 可以是Nand或Nor。layers定义电路中的计算层数（步骤）。max_gates定义最大门数。table是电路应返回的值的表。

命令列表

• generate - 生成CNF文件并将其打印到标准输出。
• execute - 生成CNF文件并将其传递给SAT求解器，检查并打印结果。必须设置SAT_SOLVER环境变量以指向SAT求解器可执行文件的路径。
• check - 检查并打印SAT输出的结果。命令后的第二个参数或第一个文件没有给出时，SAT输出文件。
• help - 打印帮助信息。

示例输出

Number of gates for layers: [8, 11, 12, 6, 12, 6]
Layer 1:
  (0, 0) 0
  (0, 0) 0
  (0, 2) 2
  (0, 2) 2
....
Output:
  (6, 1) 167
  (6, 2) 168
  (6, 0) 166
  (5, 7) 159

返回电路结构。在层列表中是门输入，其中括号中的第一个数字是层的编号（0 - 索引输入）和输出编号。