An algorithm based on resolution for the satisfiability problem

The satisfiability problem is the core problem in artificial intelligence. 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.