摘要
采用冲突驱动回溯、两观察变量法等思想,静态分析和动态更新相结合的排序决策,鼓励冲突,尽早剪除不满足解空间,提高算法速度.根据变量正反文字出现次数的乘积进行初始排序,优先考虑正反文字出现次数较多变量的赋值;采用冲突驱动、动态更新变量顺序、优先考虑发生冲突子句中变量的赋值,尽可能避免当前冲突.实验结果表明:与采用其他决策策略的解决器相比,文中的解决器拥有一定的速度优势.
This paper proposes a propositional satisfiability problem （SAT） solver, which inherits the features such as conflict-driven learning and fast Boolean constraint propagation. It improves the decision making strategy by encouraging conflicts, thus pruning the search as early as possible. Variables are ordered according to f（x）×f（-x）, where f（x） is the number of literal x in all clauses. The unassigned variable with the largest value is chosen to assign. When conflicted, the activities of all literals in the conflict clauses are increased and the order is updated. Experimental results show that the proposed SAT solver obtains much performance improvement in comparison with other solvers.
出处
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2006年第10期1472-1477,共6页
Journal of Computer-Aided Design & Computer Graphics
基金
国家"八六三"高技术研究发展计划(2003AA1Z1120
2004AA1Z1050)
国家自然科学基金(90307017
60176017
90207002)
教育部跨世纪优秀人才培养计划基金
美国国家科学基金(CCR-0098275
CCR-0306298)
关键词
可满足性问题
DPLL
决策
冲突
propositional satisfiability problem
DPLL
decision making
conflict
