An algorithm based on resolution for the satisfiability problem

Author

Xu, Youjun ; Ouyang, Dantong ; Ye, Yuxin

Volume

4

fYear

2010

fDate

27-29 March 2010

Firstpage

420

Lastpage

423

Abstract

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.

Keywords

artificial intelligence; computability; algorithm directional resolution; artificial intelligence; satisfiability problem; splitting rule; Appropriate technology; Artificial intelligence; Computer science; Computer science education; Computer vision; Databases; Educational institutions; Educational technology; Knowledge engineering; Laboratories; SRDR; directional resolution; satisfiability problem; splitting rule; strategy MO;

fLanguage

English

Publisher

ieee

Conference_Titel

Advanced Computer Control (ICACC), 2010 2nd International Conference on

Conference_Location

Shenyang

Print_ISBN

978-1-4244-5845-5

Type

conf

DOI

10.1109/ICACC.2010.5486890

Filename

5486890