An Algorithm Based on Resolution for the Satisfiability Problem

摘要：

The satisfiability problem is the core problem in artificial intellgence. The algorithm directional resolution(DR) is a well known method based on resolution for satisfiability problem. But the number of clauses has great impact on the efficiency of the method. In this paper, an algorithm SRDR is proposed to solve the problem. SRDR is based on algorithm DR and splitting rule. By using splitting rule, the number of clauses can be reduced obviously. Furthermore, the strategy MO is designed for SRDR. With the strategy, we can get a better order of variables and the efficiency of SRDR is improved. The experimental data shows that SRDR is more efficient that DR.

关键词： satisfiability problem directional resolution splitting rule SRDR strategy MO

作者: Youjun Xu Dantong Ouyang Yuxin Ye

作者单位: College of Computer Science and Technology Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education Jilin University Changchun China

会议类型: 国际会议

会议名称: The 2nd IEEE International Conference on Advanced Computer Control(第二届先进计算机控制国际会议 ICACC 2010)

会议地点: 沈阳

会议语种:英文

页码: 420-423

在线出版日期: 2010-03-27（万方平台首次上网日期，不代表论文的发表时间）