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 well
File 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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/2378
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact