可满足性问题的异或约束提取方法研究

　　可满足性问题(Propositional Satisfiability Problem，SAT)是第一个非确定多项式(Non-deterministic P0lynomial，NP)问题。这就意味着，如果NP≠P，在最坏情况下，我们必须要花费指数时间才能求解它。换句话说，用现代计算机是无法在合理的时间内找到它的解。事实上，目前还没有找到一个多项式时间有效的SAT求解