HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Cooperation of Decision Procedures for the Satisfiability Problem

Christophe Ringeissen 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Constraint programming is strongly based on the use of solvers which are able to check satisfiability of constraints. We show in this paper a rule-based algorithm for solving in a modular way the satisfiability problem w.r.t. a class of theories $Th$. The case where $Th$ is the union of two disjoint theories $Th_1$ and $Th_2$ is known for a long time but we study here different cases where function symbols are shared by $Th_1$ and $Th_2$. The chosen approach leads to a highly non-deterministic decomposition algorithm but drastically simplifies the understanding of the combination problem. The obtained decomposition algorithm is illustrated by the combination of non-disjoint equational theories.
Document type :
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:07:50 PM
Last modification on : Friday, February 4, 2022 - 3:31:27 AM
Long-term archiving on: : Monday, April 5, 2010 - 12:02:09 AM


  • HAL Id : inria-00073939, version 1



Christophe Ringeissen. Cooperation of Decision Procedures for the Satisfiability Problem. [Research Report] RR-2753, INRIA. 1995, pp.19. ⟨inria-00073939⟩



Record views


Files downloads