Paper Info
Title
Satisfiability solvers are static analysers
Abstract
This paper shows that several propositional satisfiability algorithms compute approximations of fixed points using lattice-based abstractions. The Boolean Constraint Propagation algorithm (bcp) is a greatest fixed point computation over a lattice of partial assignments. The original algorithm of Davis, Logemann and Loveland refines bcp by computing a set of greatest fixed points. The Conflict Driven Clause Learning algorithm alternates between overapproximate deduction with bcp, and underapproximate abduction, with conflict analysis. Thus, in a precise sense, satisfiability solvers are abstract interpreters. Our work is the first step towards a uniform framework for the design and implementation of satisfiability algorithms, static analysers and their combination.
Year
DOI
Venue
2012
10.1007/978-3-642-33125-1_22
SAS
Keywords
Field
DocType
fixed point,satisfiability solvers,boolean constraint propagation algorithm,static analysers,algorithm alternate,satisfiability algorithm,greatest fixed point,loveland refines bcp,propositional satisfiability algorithm,greatest fixed point computation,original algorithm
Conflict-Driven Clause Learning,Lattice (order),Abstract interpretation,Computer science,Satisfiability,Algorithm,Truth table,Theoretical computer science,Unit propagation,Fixed point,Conflict analysis
Conference
Volume
ISSN
Citations 
7460
0302-9743
9
PageRank 
References 
Authors
0.50
23
3
Name
Order
Citations
PageRank
Vijay D'Silva123914.07
Leopold Haller21276.93
Daniel Kroening33084187.60