cryptography - 恒定输入如何影响问题的 SAT 公式？

Question

假设我有一个带有 N 个输入和 1 个输出的黑盒电路。

我想固定 M 个输入的值并找到电路可满足的其余输入 (NM) 的值。如果我手动修复verilog RTL中的M个输入，并将其转换为CNF（使用abc），这会产生正确的结果吗？这是解决这类问题的正确方法吗？

Answer 1

您问题的原始搜索空间有2^N条目。通过固定M输入，搜索空间减少了一个因子2^M并具有2^(N-M)条目。

根据您对固定M输入值的选择，您可以简化搜索，也可以过多地减少搜索空间，最终没有解决方案。

您的黑匣子是一个组合电路，其输出仅取决于输入的当前状态？在RTL（寄存器传输级别/语言）设置中，您还可以描述顺序机制，其中输出还取决于先前的输入。

考虑固定输入称为布尔约束传播。这基本上简化了您的电路，因为可以移除所有具有预定输出的元件。示例：AND具有一个或多个错误输入的一个具有错误输出。具有OR一个或多个真实输入的一个具有一个真实输出，依此类推。其他简化包括去除双重否定和门的反向输入对XOR/XNOR。

您可以查看bc2cnf，它是从布尔网表格式到 SAT 求解器可消化DIMACS/CNF文件的转换器。与ABC类似，bc2cnf将传播恒定输入并提供相当优化的CNF。