Solving SAT Problem with Boolean Algebra

The satisfiability (SAT) problem is an important problem of automated reasoning. In the past decades, many methods of SAT are proposed, such as method based on resolution, method based on tableau and method based on extension rule. Based on the study of extension rule, we find that the SAT problem can be solved with hitting set algorithms. If we can find a hitting set of a clause set, and if there is not any pair of complementary literals in the hitting set, the clause set is satisfiable. Algorithm BHS based on Boolean algebra proposed by Jiang is an efficient hitting set algorithm. SSBF proposed in this paper is a revised algorithm of BHS that can be used to judge the satisfiability of a clause set. The test result shows that SSBF is an efficient algorithm.