Sciweavers

ECAI
2008
Springer

Justification-Based Non-Clausal Local Search for SAT

14 years 20 days ago
Justification-Based Non-Clausal Local Search for SAT
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.
Matti Järvisalo, Tommi A. Junttila, Ilkka Nie
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where ECAI
Authors Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä
Comments (0)