Negation for Free!
- Others:
- Software certification with semantic analysis (CELTIQUE) ; Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4) ; Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Université de Rennes 1 (UR1) ; Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1) ; Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) ; Université de Rennes 1 (UR1) ; Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1) ; Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes) ; Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)
- Département d'Informatique [Oran] ; Université des sciences et de la Technologie d'Oran Mohamed Boudiaf [Oran] (USTO MB)
- Laboratoire d'Informatique, Signaux, et Systèmes de Sophia-Antipolis (I3S) / Equipe CEP ; Modèles Discrets pour les Systèmes Complexes (Laboratoire I3S - MDSC) ; Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S) ; Université Nice Sophia Antipolis (1965 - 2019) (UNS) ; COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS) ; COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S) ; Université Nice Sophia Antipolis (1965 - 2019) (UNS) ; COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS) ; COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)
- INRIA
- DGRSDT Algeria
Description
Global constraint design is a key success of CP for solving hard combinatorial problems. Many works suggest that automaton-based definitions and filtering make easier the design of new global constraints. In this paper, from such a design, we present an approach that gives an automaton-based definition of the NEGATION of a global constraint... for free! For a given global constraint C, the idea lies in giving operators for computing an automaton that recognizes only tuples that are not solution of C, and use the REGULAR global constraint to automatically reason on this automaton. We implemented this approach for automaton-based global constraints, including global contiguity and lex constraints, and got experimental results that show that their automatically computed negation is highly competitive with more syntactic transformations.
Abstract (French)
Les contraintes globales représentent en grande partie la puissance de la PPC. Ces dernières années, on retrouve de nouvelles représentations des contraintes globales par des automates à état fini (DFA) ou encore des MDD (Multivalued Decision Diagram) avec du filtrage générique. Dans cet article, à partir d'une représentation DFA, nous présentons une approche pour la négation des contraintes globales. En prenant une contrainte globale C, l'idée est de définir des opérateurs qui calculent un automate qui ne reconnait que les solutions de $\neg C$. Pour le filtrage, nous utilisons la contrainte générique REGULAR qui prend l'automate de la version niée de la contrainte. Nous avons expérimenté cette approche sur deux exemples (i.e., global_contiguity et Lex), les résultats sont comparés à ceux d'une négation naïve d'un niveau syntaxique.
Additional details
- URL
- https://hal.inria.fr/inria-00629657
- URN
- urn:oai:HAL:inria-00629657v1
- Origin repository
- UNICA