分支启发的变元的赋值优化算法、布尔可满足性验证算法

摘要

本发明公开了一种分支启发的变元的赋值优化算法、布尔可满足性验证算法。其中分支启发的变元的赋值优化算法，至少一个变元采用以下赋值步骤进行赋值：对待赋值的变元进行第一次赋值；计算赋值以后所述待赋值的变元在分支启发中发生n次冲突的第一时间；将第一次赋值的值进行取反并以取反后的值对待赋值的变元进行第二次赋值；计算赋值以后所述待赋值的变元在分支启发中发生n次冲突的第二时间；比较第一时间和第二时间，选择时间短的那次赋值的值对待赋值的变元进行赋值。本发明可以加快分支启发算法的计算时间。