Hybrid Satisfiability Techniques

Satisfiability Techniques helps in deciding if there is a truth assignment for the symbols that appear in a Boolean function such that it assigns the value true to the Boolean Function. However satisfiability can be proved using Truth Tables, but design of truth table for a Boolean function of large number of variables is trivial. SAT algorithms have to handle hundreds of thousands of millions of variables and clauses. One of the major problems in the area of computer science is to have higher productivity or developing algorithms that are efficiently utilizing the power of computers. Researchers are doing a lot of research and hence developing various techniques and algorithms to reduce the required computation time to minimum. Most of the satisfiability techniques are based on the search algorithms given by Martin Davis, George Logemann and Donald Loveland which performs a branching search with backtracking. In order to combine the powers of both local search and DPLL-based search, the previous approaches mainly tried to embed the local search result into a DPLL-based SAT solver to guide the decision order. In such approaches, the local search is invoked at each DPLL decision step to supply the information for the next decision. On the contrary, in this approach, the local search portion is used to identify a subset of clauses, which are passed to a DPLL-based incremental SAT solver. Furthermore, the solution obtained by the incremental DPLL solver on the subset of clauses is fed back to the local search solver to jump over the locally optimal points encountered in the previous iteration to continue the search.