Many real-world problems require the ability of reasoning efficiently on formulae which are boolean combinations of boolean and unquantified mathematical propositions. This task requires a fruitful combination of efficient boolean reasoning and mathematical solving capabilities. SAT tools and mathematical reasoners are respectively very effective on one of these activities each, but not on both. In this paper we present a formal framework, a generalized algorithm and architecture for integrating boolean reasoners and mathematical solvers so that they can efficiently solve boolean combinations of boolean and unquantified mathematical propositions. We describe many techniques to optimize this integration, and highlight the main requirements for SAT tools and mathematicalsolvers to maximize the benefits of their integration.
Efficiently Integrating Boolean Reasoning and Mathematical Solving / Bertoli, Piergiorgio; Cimatti, Alessandro; Audemard, Gilles; Kornilowicz, Artur; Sebastiani, Roberto. - ELETTRONICO. - (2003), pp. 1-20.
Efficiently Integrating Boolean Reasoning and Mathematical Solving
Cimatti, Alessandro;Sebastiani, Roberto
2003-01-01
Abstract
Many real-world problems require the ability of reasoning efficiently on formulae which are boolean combinations of boolean and unquantified mathematical propositions. This task requires a fruitful combination of efficient boolean reasoning and mathematical solving capabilities. SAT tools and mathematical reasoners are respectively very effective on one of these activities each, but not on both. In this paper we present a formal framework, a generalized algorithm and architecture for integrating boolean reasoners and mathematical solvers so that they can efficiently solve boolean combinations of boolean and unquantified mathematical propositions. We describe many techniques to optimize this integration, and highlight the main requirements for SAT tools and mathematicalsolvers to maximize the benefits of their integration.File | Dimensione | Formato | |
---|---|---|---|
011.pdf
accesso aperto
Tipologia:
Versione editoriale (Publisher’s layout)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
465.63 kB
Formato
Adobe PDF
|
465.63 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione