基于线性规划的布尔可满足性判定方法

摘要

本发明为基于线性规划的布尔可满足性判定方法，属于逻辑电路领域，包括如下步骤：S1提取布尔命题逻辑公式；S2：转换为等可满足的CNF布尔逻辑公式；S3：转化为CNF形式的3‑SAT问题；S4：转化为1‑in‑3‑SAT问题；S5：等效转化为一个线性规划的最优值大小问题；S6：对线性规划的最优值求解问题进行求解精度设定；S7：求解线性规划问题的最优值，并根据最优值大小来判定布尔命题逻辑公式的可满足性；S8：对于可满足的布尔命题逻辑公式，递归地对线性规划问题添加约束并进行求解，得到可满足问题的一个解答。本发明实现了在多项式时间复杂度下的快速判定，能够判定的提高效率，节约能源。