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.
2010
Trento
Università degli Studi di Trento
Stochastic Local Search for SMT / Tomasi, Silvia. - ELETTRONICO. - (2010), pp. 1-73.
Tomasi, Silvia
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

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

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

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