在一个输出的逻辑电路中，如何得到产生一定输出的所有输入组合？（无蛮力）[已结束]

这最好使用 SAT/SMT 求解器来完成，例如 Microsoft 的 z3：https://github.com/Z3Prover

它可以从 python 编写脚本，您可以要求它查找为您提供所需输出的输入值。下面是一个非常简单的示例：

from z3 import *

in1, in2 = Bools("in1 in2")
out = Bool("out")

s = Solver()

# Encode your circuit here. We'll just do out = in1 \/ in2
s.add(out == Or(in1, in2))

# require output to be true.
# You could also set it to False, if that's what you're looking for.
s.add(out == True)

print(s.check())
print(s.model())

当我运行它时，我得到：

sat
[in1 = True, in2 = False, out = True]

第一行说，这意味着问题确实是可以解决的。（否则你会得到 。satunsat

第二行是用于获取此所需输出的赋值。您还可以通过编程来枚举所有可能的解决方案，当然，如果有很多解决方案，这可能会导致很长的运行循环。

有关如何对电路进行编码以使其适合此类分析的详细信息，您应该查找 Tseytin Encoding： https://en.wikipedia.org/wiki/Tseytin_transformation

我应该强调的是，如果你试图“逆向工程”一个单向函数（即，如果你的电路正在计算某种加密算法，如AES/DES，或者进行类似SHA的散列），所有这些都将是徒劳的。目前还没有SAT求解器（或任何其他工具）可以处理这类问题。我在这里谈论的电路类型是常规函数，例如算术或其他常规数据路径。你从来没有说过你正在处理什么样的电路，但请记住这一点。