Improving Diversification in Local Search for Propositional Satisfiability
Thach-Thao Nguyen Duong · Griffith Research Online · 2014
In recent years, the Propositional Satisfiability (SAT) has become standard for encoding real world complex constrained problems. SAT has significant impacts on various research fields in Artificial Intelligence (AI) and Constraint Programming (CP). SAT algorithms have also been successfully used in solving many practical and industrial applications that include electronic design automation, default reasoning, diagnosis, planning, scheduling, image interpretation, circuit design, and hardware and software verification. The most common representation of a SAT formula is the Conjunctive Normal Form (CNF). A CNF formula is a conjunction of clauses where each clause is a disjunction of Boolean literals. A SAT formula is satisfiable if there is a truth assignment for each variable such that all clauses in the formula are satisfied. Solving a SAT problem is to determine a truth assignment that satisfies a CNF formula. SAT is the first problem proved to be NP-complete [20]. There are many algorithmic methodologies to solve SAT. The most obvious one is systematic search; however another popular and successful approach is stochastic local search (SLS). Systematic search is usually referred to as complete search or backtrack-style search. In contrast, SLS is a method to explore the search space by randomisation and perturbation operations. Although SLS is an incomplete search method, it is able to find the solutions effectively by using limited time and resources. Moreover, some SLS solvers can solve hard SAT problems in a few minutes while these problems could be beyond the capacity of systematic search solvers.