Output details

Abstract conflict driven learning

<07>

Modern SAT solvers have demonstrated impressive improvements in scalability over the last decade. We show that the core algorithm for propositional satisfiability can be generalised to search for solutions within a generalised lattice, enabling applications of abstract interpretation within satisfiability solvers over richer domains, and at the same time enabling applications of SAT-technology to increase the precision of program analysers. In particular, our generalisation provides a new method for static analyzers that operate over non-distributive lattices to reason about properties that require disjunction. This paper introduces a new framework, with instances, among others, for bit-accurate reasoning for difficult numerical software.