SAT无满足解的充分必要条件

姜咏江

本人发明的子句消去法，是快速求出SAT满足解的方法。该方法无疑在电子电路设计的化简和优化中会起到十分重要的作用。关于子句消去法的原理和方法，请参阅：http://blog.sciencenet.cn/blog-340399-961507.html。

SAT的满足解是由n元逻辑变量的一组值构成的，这组由数码0和1构成的数组带入SAT表达式，会使SAT表达式的值为1。在子句消去法中，SAT满足解体现为所有的子句都能在值为1的情况下消去，最终没有剩余子句。

不论SAT还是k-SAT一般情况下常有多解，因而研究它们的无解情况甚至比有解都要重要。本文主要给出SAT无满足解的充分必要条件。

基本定理：SAT无满足解的充分必要条件是子句块或动态块无解。

子句块由共同变量的子句构成，而动态块是由设定一些变量值后的具有共同变量的剩余子句构成。因而容易理解子句块或动态块无解，肯定SAT无满足解。

证明：【充分性】依据子句消去法，当有子句块或动态子句块无解时，就会有子句不能消去。可见充分性成立。

       【必要性】若SAT任意子句块或动态子句块都有解，则知所有的变量都有确定的值可一起构成SAT满足解。必要性成立。

2016-3-27