欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
采用冲突驱动回溯、两观察变量法等思想,静态分析和动态更新相结合的排序决策,鼓励冲突,尽早剪除不满足解空间,提高算法速度.根据变量正反文字出现次数的乘积进行初始排序,优先考虑正反文字出现次数较多变量的赋值;采用冲突驱动、动态更新变量顺序、优先考虑发生冲突子句中变量的赋值,尽可能避免当前冲突.实验结果表明：与采用其他决策策略的解决器相比,文中的解决器拥有一定的速度优势.
英文摘要：
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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：