%0 Journal Article %T 利用逻辑演绎求解SAT问题的启发式完全算法<br>Heuristic Complete Algorithm for SAT Problem by Using Logical Deduction %A 陈青山 %A 徐扬 %A 何星星< %A br> %A CHEN Qingshan %A XU Yang %A HE Xingxing %J 西南交通大学学报 %D 2017 %R 10.3969/j.issn.0258-2724.2017.06.025 %X 为解决可满足性（satisfiability problem，SAT）问题求解过程中分支决策效率不高的问题，提出了一种基于逻辑演绎分组（logical deduction group，LDG）的启发式完全算法.该算法通过选择剩余未满足子句参与逻辑演绎，得到一组局部可满足赋值序列，并引导求解器优先搜索赋值序列所在解空间；对于可满足问题，可以通过迭代调用演绎过程，将局部可满足解成组地扩充为全局可满足解，对于不可满足问题，如果演绎结果出现空子句，则可以直接判定.采用SAT国际竞赛的实例，与具有代表性的指数级变元状态独立下降和（exponential variable state independent decaying sum，EVSIDS）变量决策算法进行了对比测试，结果表明：在求解总问题数方面，LDG比EVSIDS多出42个；在求解速度方面，LDG对可满足问题的求解时间相较EVSIDS平均减少了22.8%，对不可满足问题的求解时间平均减少了17.8%，总平均时间减少了20.1%.<br>：In order to address the issue of branch decision-making inefficiency in solving the satisfiability problem (SAT), a heuristic complete algorithm based on logical deduction group (LDG) is proposed. Specifically, the proposed algorithm chooses the remaining unsolved clauses to make the logical deduction such that an assignment sequence of partial satisfiability is obtained, further guiding the solver to first search its solution space. For the satisfiable problem, the partial assignment can be extended group by group to a complete assignment by iteratively utilizing the deductive process. For the unsatisfiable problem, it can be straightforward to judge whether there exists an empty clause. The international competition instance in SAT is adopted for comparison with the typical exponential variable state independent decaying sum (EVSIDS) decision heuristic. The experimental results demonstrate that LDG can solve 42 more problems than EVSIDS, and achieve 22.8% and 17.8% reductions in average solution time for the satisfiable and unsatisfiable problems, respectively, as well as a 20.1% reduction in total average time %K SAT问题 %K 启发式算法 %K 搜索算法 %K 变量决策 %K 演绎推理 %K < %K br> %K satisfiability problem %K heuristic algorithms %K searching algorithms %K decision making %K deductive reasoning %U http://manu19.magtech.com.cn/Jweb_xnjd/CN/abstract/abstract12524.shtml