Solving SAT problem with a revised hitting set algorithm

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.