We describe a new SMT procedure integrating a Boolean Stochastic Local Search (SLS) algorithm with a T-solver by lazy approach. The SLS-based SMT solver uses the SLS solver to explore the set of assignments in order to find an optimal truth assignment for the Boolean abstraction of the input formula. Then it invokes the T-solver to find conflicts which are used for guiding the SLS search process. We also implemented a group of techniques in order to improve the effictiveness of our SMT procedure.
Stochastic Local Search for SMT / Tomasi, Silvia. - ELETTRONICO. - (2010), pp. 1-73.
Stochastic Local Search for SMT
Tomasi, Silvia
2010-01-01
Abstract
We describe a new SMT procedure integrating a Boolean Stochastic Local Search (SLS) algorithm with a T-solver by lazy approach. The SLS-based SMT solver uses the SLS solver to explore the set of assignments in order to find an optimal truth assignment for the Boolean abstraction of the input formula. Then it invokes the T-solver to find conflicts which are used for guiding the SLS search process. We also implemented a group of techniques in order to improve the effictiveness of our SMT procedure.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
DISI-10-060.pdf
accesso aperto
Tipologia:
Versione editoriale (Publisher’s layout)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
625.16 kB
Formato
Adobe PDF
|
625.16 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
