In the last years we have witnessed an impressive advance in the efficiency of boolean solving techniques, which has brought large previously intractable problems at the reach of state-of-the-art solvers. Unfortunately, simple boolean expressions are not expressive enough for representing many real-world problems, which require handling also integer or real values and operators. On the other hand, mathematical solvers, like computer-algebra systems or constraint solvers, cannot handle efficiently problems involving heavy boolean search, or do not handle them at all. In this paper we present the foundations and the basic algorithms for a new class of procedures for solving boolean combinations of mathematical propositions, which combine boolean and mathematical solvers, and we highlight the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration. Finally we show how existing systems are captured by our framework.

Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms and Requirements / Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Kornilowicz, Artur; Sebastiani, Roberto. - ELETTRONICO. - (2002).

Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms and Requirements

Cimatti, Alessandro;Sebastiani, Roberto
2002-01-01

Abstract

In the last years we have witnessed an impressive advance in the efficiency of boolean solving techniques, which has brought large previously intractable problems at the reach of state-of-the-art solvers. Unfortunately, simple boolean expressions are not expressive enough for representing many real-world problems, which require handling also integer or real values and operators. On the other hand, mathematical solvers, like computer-algebra systems or constraint solvers, cannot handle efficiently problems involving heavy boolean search, or do not handle them at all. In this paper we present the foundations and the basic algorithms for a new class of procedures for solving boolean combinations of mathematical propositions, which combine boolean and mathematical solvers, and we highlight the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration. Finally we show how existing systems are captured by our framework.
2002
Trento, Italia
Università degli Studi di Trento. DEPARTMENT OF INFORMATION AND COMMUNICATION TECHNOLOGY
Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms and Requirements / Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Kornilowicz, Artur; Sebastiani, Roberto. - ELETTRONICO. - (2002).
Audemard, Gilles; Bertoli, Piergiorgio; Cimatti, Alessandro; Kornilowicz, Artur; Sebastiani, Roberto
File in questo prodotto:
File Dimensione Formato  
42.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 342.99 kB
Formato Adobe PDF
342.99 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/358463
 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
social impact