Structure-Based Local Search Heuristics for Circuit-Level Boolean
  Satisfiability
  This work focuses on improving state-of-the-art in stochastic local search
(SLS) for solving Boolean satisfiability (SAT) instances arising from
real-world industrial SAT application domains. The recently introduced SLS
method CRSat has been shown to noticeably improve on previously suggested SLS
techniques in solving such real-world instances by combining
justification-based local search with limited Boolean constraint propagation on
the non-clausal formula representation form of Boolean circuits. In this work,
we study possibilities of further improving the performance of CRSat by
exploiting circuit-level structural knowledge for developing new search
heuristics for CRSat. To this end, we introduce and experimentally evaluate a
variety of search heuristics, many of which are motivated by circuit-level
heuristics originally developed in completely different contexts, e.g., for
electronic design automation applications. To the best of our knowledge, most
of the heuristics are novel in the context of SLS for SAT and, more generally,
SLS for constraint satisfaction problems.
