@inproceedings{
    JarvisaloJN:ECAI08,
    editor = "Ghallab, Malik and Spyropoulos, Constantine D. and Fanotakis, Nikos and Avoukis, Nikos",
    author = {J{\"a}rvisalo, Matti and Junttila, Tommi and Niemel\"a, Ilkka},
    publisher = "IOS Press",
    title = "Justification-Based Non-Clausal Local Search for {SAT}",
    url = "http://www.tcs.tkk.fi/~mjj/publications.shtml",
    series = "Frontiers in Artificial Intelligence and Applications",
    booktitle = "Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 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.",
    volume = "178",
    flags = "MCM public",
    year = "2008",
    pages = "535--539"
}