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