Research Publications

Despite significant improvements over the last two decades, local search techniques still struggle to compete with the best systematic methods when solving highly structured real-world satisfiability (SAT) problems. Recent work has successfully employed a dependency lattice structure to represent dependent variables within a local search architecture, producing the first local search technique able to consistently solve the well-known 32-bit parity problem within 24 hours. However, these results are still many times slower than those obtained by the best systematic solvers. In this paper we propose a new local search hybrid platform that splits a conjunctive normal form (CNF) formula into three sub-components: i) a minimal dependency lattice (representing the core connections between logic gates), ii) a conjunction of equivalence clauses, and iii) the remaining clauses. In addition, we adopt a new hierarchical cost function that focuses on solving the core components of the problem first. In an experimental study using hard industrial benchmarks, we show that our hybrid platform significantly outperforms the original dependency lattice approach and delivers performance that is now competitive with the best modern systematic solvers.