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
2005-01-01
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 wellFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.