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
Incremental Compilation-to-SAT Procedures / Benedetti, Marco; Bernardini, Sara. - 3542:(2005), pp. 205-213. (Intervento presentato al convegno Theory and Applications of Satisfiability Testing. Revised Selected Papers of the 7th International Conference, SAT 2004 tenutosi a Vancouver, Canada).
Incremental Compilation-to-SAT Procedures
Benedetti, Marco;Bernardini, Sara
2005
Abstract
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 wellI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
