Research On Several SAT Issues Based On Extension Rule

Automated reasoning is the central field of computer science. Since Robinson proposed the principle of resolution, research on automated reasoning has always been the focus. Methods based on resolution and methods based on tableau are main methods for automated reasoning. They have different virtue and are used in different field.Method based on extension rule proposed by Lin has drawn more and more attention of researchers. And the method develops rapidly in recent years. It's a different method from the methods mentioned above. Methods based on resolution try to get empty clause from resolution, and prove the unsatisfiability of clause set by this way. However, methods based on extension rule prove the unsatisfiability of clause set by a different way. When judging the satisfiability of a clause set, methods based on extension rule don't really extend all clauses. They calculate the number with inclusion-exclusion principle. Methods need to compute less terms when the complementary factor is big, because many terms'values are zero. So, methods based on extension rule have better time efficiency when the complementary factor is big.Time is the key when solving a satisfiability(SAT) problem. So, researchers focus on how to improve the efficiency of algorithms. Because methods based on extension rule have better time efficiency when the complementary factor is big, we choose it to solve SAT problem. And our work focuses on improving the efficiency of methods based on extension rule:(1)Improve the efficiency of methods based on extension rule with DPLL rules. Though there is difference between methods based on resolution and methods based on extension rule, work on resolution is worth taking into account. Algorithm DPLL is most famous in methods based on resolution. Especially, single literal rule, pure literal rule and splitting rule are used widely.Because methods based on extension rule judging clause set's satisfiability by calculating the number of maximum terms, the number of clauses has great effect on the efficiency. Thus, we must consider how to reduce the clause number. Algorithm IER construct a subproblem by filtrating a clause set with a clause. If the algorithm could not get a solution from the subproblem, it will turn to the original clause set.With the idea of algorithm IER, we proposed the algorithm CIER. Algorithm CIER split a clause set into several small sets. Each small set contain less clauses than original clause set. If one of these small sets is satisfialbe, the original set is satisfiable. Or else, the original clause set is unsatisfiable. In order to get smaller clause set as possible, we proposed the strategy MOAMD. Literals with more occurrences would be chosen for splitting. The test result shows that CIER is more efficient than algorithm IER, without increasing of space complexity.(2)We proposed methods based on hitting set for SAT problems, and the methods have no relativity with complemantary factor. Methods based on extension rule judge a clause set's satisfiability by calculating the number of clauses. Only when the clause set could extend all maximum terms, it is unsatisfiable. If there exist a maximum term could not be extended from the clause set, the clause set is satisfiable.As a result, if we could find a maximum term couldn't be extended, the clause set is satisfiable. If a maximum term could be extended from a clause, the maximum term contain all literals occur in the clause. If a maximum term could not be extended from a clause, there must be a literal in the clause and the literal don't occur in the maximum term. It is to say that there are a couple of complementary literals in the clause and the maximum term. Thus, the maximum term which could not be extended from the clause set must contain complementary literals to each clause in the clause set. If replacing each literal in the maximum term with a complementary literal, we will get a hitting set of the clause set. We could draw the conclusion that the clause set is satisfiable if the hitting set exists. So, the SAT problem becomes an existence problem of a hitting set.Now, existing complete hitting set algorithms calculate all minimum hitting set. And incomplete hitting set algorithms could not be used to judge a clause set's satisfiability. So, a new algorithm judging the existence of a hitting set needs to be designed. We proposed algorithm CBHST and RNHST to judge the existence of a hitting set. Algorithm DR based on resolution is chosen to compare with them. Time efficiency of CBHST and RNHST are better than DR, which is shown in the test result. When clause length is big, RNHST is more efficient than CBHST. CBHST is the better algorithm if clause length is small. CBHST and RNHST have no relativity with complemantary factor, because they needn't judge satisfiability with inclusion-exclusion principle.Otherwise, we proposed algorithm SSBF. Because SSBF calculate with Boolean algebra, it is a fitter algorithm for SAT problem of Boolean formula.(3) We proposed model counting algorithm MCEHST based on hitting set and extension rule. Each maximum term extended from a hitting set is also a hitting set. We could construct a model of the clause set by assign each literal's value is true in the maximum term. And each model could be used to construct a maximum term which is obviously a hitting set of the clause set.So, we proposed model counting algorithm MCEHST which used extension rule indirectly. The algorithm first calculates all minimum hitting set. Then extends these hitting set into maximum terms and compute the number of maximum terms, i.e. number of models.The time efficiency of this algorithm is limited by the number of minimum hitting set. So, only when clauses are short and the number of clauses is big, the time efficiency will show its merits. We choose algorithm CDP based on resolution and algorithm CER based on extension rule to comare with algorithm MCEHST. All of these algorithms could calculate the number of models accurately. The test result shows that the time efficiency of MCEHST is the best when clauses are short and the number of clauses is big. And with the rising of clause number, the time comsumed by MCEHST increases slower than CDP and CER.For #SAT problem of Boolean formula, we proposed algorithm MCBE. MCBE calculate minimal hitting sets of Boolean formula with Boolean algebra. So, it's a fitter algorithm for #S AT problem of Boolean formula. And the test result shows that MCBE has high time efficiency when terms in formula are short and many.