@techreport{BelovJarvisalo:HIIT2010, author = {Anton Belov and Matti J\"arvisalo}, title = {Depth-Based Local Search Heuristics for {B}oolean Circuit Satisfiability}, type = {HIIT Technical Reports}, number = {2010-2}, institution = {Helsinki Institute for Information Technology HIIT}, address = {Helsinki, Finland}, year = {2010}, note = {{ISBN} 978-952-60-3415-7}, } Abstract: We propose a structure-exploiting heuristic for the justification-based stochastic local search (SLS) method CRSat for Boolean circuit satisfiability. Experimental evaluation shows that the proposed depth-based heuristic significantly improved the performance of CRSat on structural instances arising from industrial applications. A proof of probabilistically approximate completeness (PAC) of CRSat relies on the same kind of variable ordering as the one imposed by the depth-based heuristic, and hence provides a theoretical motivation for the heuristic. Furthermore, we compare the behavior of (depth-based) CRSat to that of the justification-based SLS method BC SLS driven by justification frontiers.