Digitale Bibliotheek
Sluiten Bladeren door artikelen uit een tijdschrift
 
<< vorige   
     Tijdschrift beschrijving
       Alle jaargangen van het bijbehorende tijdschrift
         Alle afleveringen van het bijbehorende jaargang
           Alle artikelen van de bijbehorende aflevering
                                       Details van artikel 21 van 21 gevonden artikelen
 
 
  USING A THEOREM PROVER FOR REASONING ON CONSTRAINT PROBLEMS
 
 
Titel: USING A THEOREM PROVER FOR REASONING ON CONSTRAINT PROBLEMS
Auteur: Cadoli, Marco
Mancini, Toni
Verschenen in: Applied artificial intelligence
Paginering: Jaargang 21 (2007) nr. 4-5 pagina's 383-404
Jaar: 2007-04
Inhoud: The efficiency of systems for constraint programming (CP) is currently highly affected by the actual formulation of the input problem. To this end, several choices have to be made by modelers in order to write efficient specifications and handle instances of realistic size, and this, of course, represents a major obstacle to reach full declarativeness. Several structural properties of problem specifications have been investigated in order to provide techniques that reformulate a constraint program into one which is more efficiently evaluable by the solver at hand. In this paper we consider two such properties, symmetries and functional dependencies among variables, and show that, by characterizing problem specifications as logical formulae, the task of deciding whether such properties hold, and consequently that of performing the relevant reformulations, can be practically mechanized by means of automated theorem proving (ATP) technology. In particular, we report the results on using ATP technology for checking the existence of symmetries, checking whether a given constraint is symmetry-breaking, and checking the existence of functional dependencies in a specification. The output of the reasoning phase is a transformed constraint program, consisting in a reformulated specification and, possibly, a search strategy. We show our techniques on problems such as graph coloring, Sailco inventory, and protein folding.
Uitgever: Taylor & Francis
Bronbestand: Elektronische Wetenschappelijke Tijdschriften
 
 

                             Details van artikel 21 van 21 gevonden artikelen
 
<< vorige   
 
 Koninklijke Bibliotheek - Nationale Bibliotheek van Nederland