|||
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
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2025-1-8 19:45
Powered by ScienceNet.cn
Copyright © 2007-2025 中国科学报社