Justification-Based Non-Clausal Local Search for SAT

Reference:

Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Justification-based non-clausal local search for SAT. In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fanotakis, and Nikos Avoukis, editors, Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008), volume 178 of Frontiers in Artificial Intelligence and Applications, pages 535–539. IOS Press, 2008.

Abstract:

While stochastic local search (SLS) techniques are very efficient in solving hard randomly generated propositional satisfiability (SAT) problem instances, a major challenge is to improve SLS on structured problems. Motivated by heuristics applied in complete circuit-level SAT solvers in electronic design automation, we develop novel SLS techniques by harnessing the concept of justification frontiers. This leads to SLS heuristics which concentrate the search into relevant parts of instances, exploit observability don't cares and allow for an early stopping criterion. Experiments with a prototype implementation of the framework presented in this paper show up to a four orders of magnitude decrease in the number of moves on real-world bounded model checking instances when compared to WalkSAT on the standard CNF encodings of the instances.

Suggested BibTeX entry:

@inproceedings{JarvisaloJN:ECAI08,
    author = {Matti J{\"a}rvisalo and Tommi Junttila and Ilkka Niemel\"a},
    booktitle = {Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008)},
    editor = {Malik Ghallab and Constantine D. Spyropoulos and Nikos Fanotakis and Nikos Avoukis},
    pages = {535--539},
    publisher = {IOS Press},
    series = {Frontiers in Artificial Intelligence and Applications},
    title = {Justification-Based Non-Clausal Local Search for {SAT}},
    volume = {178},
    year = {2008},
}