Temporal induction by incremental SAT solving

By Niklas Eén, Niklas Sörensson. BMC@CAV, 2003

460 citations recorded by the source corpus.

We show how a very modest modification to a typical modern SAT-solver enables it to solve a series of related SAT-instances efficiently. We apply this idea to checking safety properties by means of temporal induction, a technique strongly related to bounded model checking. We further give a more efficient way of constraining the extended induction hypothesis to so called loop-free paths. We have also performed the first comprehensive experimental evaluation of induction methods for safety-checking.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/720e16d2f7ce64f19520a69289cc9cee3903e785

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Software

Citations in the corpus

Extending SAT Solvers to Cryptographic Problems (2009, background): “s[63] s[96] s[102] s[103] s[60] s[100] s[99] calc_s[7] - s[76] calc_s[28] - s[74] guess”
SAT-Based Encodings for Optimal Decision Trees with Explicit Paths (2020, methodology): “A cube describing a topology template can either be encoded into assumptions to enable incremental SAT solving [7] or appended as a set of unit clauses.”
RC2: an Efficient MaxSAT Solver (2019, methodology): “1 SAT Solver Interface RC2 makes use of the standard MiniSat-like incremental interface [8] to a SAT oracle, i.”
SAT-Based Model Checking without Unrolling (2011, background): “While this functionality can be simulated in more recent solvers [15], each push/pop iteration requires a new literal.”
Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction (2013, methodology): “bounded model checking [7], extraction of a minimal unsatisfiable set [8] .”
Conflict-driven answer set solving: From theory to practice (2012, methodology): “Finally, several systems implement elaborate features on top of clasp: disjunctive ASP solver claspD [31] internally couples two clasp engines, clingcon [60] embeds the gecode constraint library18 into clasp’s propagation routine to deal with non-Boolean variables, iclingo [46] exploits clasp’s incr”
An Extensible SAT-solver (2003, methodology): “For an example of the use if unit assumptions, see [ ES03 ].”
Potassco: The Potsdam Answer Set Solving Collection (2011, unknown): “Also, they allow for solving under assumptions [26], an important feature that is, for example, used in our parallel ASP solver claspar ([28]; cf.”
Multi-shot ASP solving with clingo (2017, background): “The term assumption traces back to (Eén and Sörensson 2003; Gebser et al. 2008). the state unaffected and outputs a single stable model containing b(1).”
PySAT: A Python Toolkit for Prototyping with SAT Oracles (2018, methodology): “Each SAT solver can be used in the MiniSat-like incremental fashion [14], i.”
Discovering Cyclic Causal Models with Latent Variables: A General SAT-Based Procedure (2013, methodology): “Our implementation is based on the MiniSAT solver (E´en and S¨orensson, 2004, 2003).”