Abstract conflict driven learning

Modern satisfiability solvers implement an algorithm, called Con-flict Driven Clause Learning, which combines search for a model with analysis of conflicts. We show that this algorithm can be gen-eralised to solve the lattice-theoretic problem of determining if an additive transformer on a Boolean lattice is always bottom. Our generalised procedure combines overapproximations of greatest fixed points with underapproximations of least fixed points to obtain more precise results than computing fixed points in isolation. We generalise implication graphs used in satisfiability solvers to derive underapproximate transformers from overapproximate ones. Our generalisation provides a new method for static analyzers that op-erate over non-distributive lattices to reason about properties that require disjunction