Abstract Conflict Driven Learning

作者：D'Silva Vijay^*; Haller Leopold; Kroening Daniel

来源：ACM Sigplan Notices, 2013, 48(1): 143-154.

DOI：10.1145/2480359.2429087

• Satisfiability
• Conflict Driven Clause Learning
• Lattices

Modern satisfiability solvers implement an algorithm, called Conflict Driven Clause Learning, which combines search for a model with analysis of conflicts. We show that this algorithm can be generalised 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 operate over non-distributive lattices to reason about properties that require disjunction.

• 出版日期2013-1