假设我有一个黑匣子电路，有N个输入和1个输出。
我想固定M输入的值，并找到电路满足的其余输入(N-M(的值。如果我手动修复 verilog RTL 中的 M 输入，并将其转换为 CNF(使用 abc(，这会产生正确的结果吗？这是解决此类问题的正确方法吗？
问题的原始搜索空间包含2^N条目。通过固定M输入，搜索空间减少了2^M倍，并且具有2^(N-M)条目。
根据您选择的固定M输入值，您可以简化搜索或减少过多搜索空间，最终没有解决方案。
您的黑匣子是一个组合电路，其中输出仅取决于输入的当前状态？在RTL(寄存器传输级别/语言(设置中，您还可以描述顺序机制，其中输出还取决于以前的输入。
考虑固定输入称为布尔约束传播。这基本上简化了您的电路，因为可以移除具有预定输出的所有元件。示例：具有一个或多个错误输入的AND具有错误输出。具有一个或多个真输入的OR具有真输出，依此类推。其他简化包括消除双否定和XOR/XNOR门的反相输入对。
你可以看看bc2cnf，一个从布尔网表格式到SAT求解器可消化DIMACS/CNF文件的转换器。与ABC类似，bc2cnf将传播恒定输入并提供相当优化的CNF。