计算布尔可满足性时，是否包含隐式约束？

Question

比方说，你有一个布尔函数，它接受两个数字（二进制​​），并返回true，如果他们平等16：

01000 + 01000 = 10000 
    8 + 8 = 16 -> true 


00110 + 01000 = 01110 
    6 + 8 = 14 -> false 

在这个例子中，该功能需要十分投入，让我们称他们为ABCDE + FGHIJ。

引擎盖下，它直接仿照门逻辑，并使用两个加法器和一些XNOR门，以检查等价于二进制串10000

我们再喂此二元函数为一个布尔可满足性算法来寻找一组输入产生一个真正的输出（例如上面的第一个例子）。

我的问题是：如果我们要明确观察到的约束，SAT算法会更快地找到解决方案吗？

“观察到的约束”是什么意思？那么，一个观察到的约束可能是“如果任何一个数大于16，那么就不要执行加法并返回错误”。

你可能会包含此约束，像这样：

（一^ ^¬b^¬c^¬d¬e）^（F^^¬g^¬h^¬i¬j）^（中功能你以前）

另一个约束可能是“如果一个数字是偶数，而另一个是奇数，则返回false”。

（（E ^¬j）V（¬e^ j）的）^（你之前所具有的功能）

这些布尔函数是在正确性等效的，但在门逻辑，后者将（可能）效率更高。将问题模型化为SAT减少的唯一问题，还是有助于包含这些观察到的约束？

我意识到这不是一个很好的例子，但希望它解释我在问什么。

预先感谢

Answer 1

你的样本函数的结果为true，2^10 = 1024个可能的输入组合17。

这可以被实施为多级逻辑电路是这样的：

SAT solvers的是当不能枚举所有输入组合可行问题的主要区域。 10个输入是相当适中的大小。 SAT求解器通常不得不应对数百，甚至数百万个输入变量。在PC上评估几个100.000输入组合（~20个输入）非常容易。但如果不是几十亿个组合以后不可能实现的话，那就变得不切实际了。

通常的方法是首先在Conjunctive Normal Form（CNF）中编码问题，然后让SAT求解器找到一个解决方案或发现问题不可满足。大多数SAT求解者都很难找到全部的解决方案。

如果您有问题的布尔表达式，您首先必须将此公式转换为CNF或解算器能够处理的格式。合适的工具包括bc2cnf。像Z3支持SMT 2.0和除CNF之外的其他格式（又名DIMACS）等更一般的求解器。

除了列举真值表或询问像Cryptominisat 2这样的SAT解算器外，您还可以使用约束驱动求解器。其他要求谷歌的条款包括“Answer set programming”。