Incremental Compilation-to-SAT Procedures

We focus on incremental compilation-to-SAT procedures(iCTS), a promising way to push the standard CTS approaches beyond their limits. We propose the first comprehensive framework that encompasses all the aspects of an incremental decision procedure , from the encoding to the incremental solver. We apply our guidelines to a real-world CTS approach (Bounded Model Checking ) and show how to modify both the generation mechanism of a real BMC tool (NuSMV) and the solving engine of a public-domain SAT solver (SIM). Related approaches and experimental results are discussed as well.