Title :
Solving SAT problem with a revised hitting set algorithm
Author :
Xu, Youjun ; Ouyang, Dantong ; Ye, Yuxin ; He, Jialiang
Author_Institution :
Coll. of Comput. Sci. & Technol., Jilin Univ., Changchun, China
Abstract :
The satisfiability (SAT) problem is a core problem of artificial intelligence. Research findings in SAT are widely used in many areas. The main methods solving SAT problem are resolution principle, tableau calculus and extension rule. Besides methods mentioned above, we find that the SAT problem can be solved with hitting set algorithms. If a set of clause is satisfiable, there must be a hitting set of the clause set which containing no complementary pairs of literals. Algorithm NEWHS-tree is an efficient hitting set algorithm proposed by Ouyang. RNHST proposed in this paper is a revised algorithm in respect of NEWHS-tree. It judges the satisfiability of a clause set by confirming the existence of the set´s hitting set without complementary pairs of literals. The test result shows that RNHST is an efficient algorithm.
Keywords :
computability; set theory; trees (mathematics); NEWHS-tree algorithm; artificial intelligence; extension rule method; resolution principle method; revised hitting set algorithm; satisfiability problem; tableau calculus method; Artificial intelligence; Calculus; Computer science; Computer science education; Educational institutions; Educational technology; Knowledge engineering; Laboratories; NP-complete problem; Testing; NEWHS-tree; extension rule; hitting set; minimal hitting set; satisfiability problem;
Conference_Titel :
Future Computer and Communication (ICFCC), 2010 2nd International Conference on
Conference_Location :
Wuhan
Print_ISBN :
978-1-4244-5821-9
DOI :
10.1109/ICFCC.2010.5497565