Une approche SAT sensible à la mémoire pour les logiques modales PSPACE - Université Côte d'Azur Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Une approche SAT sensible à la mémoire pour les logiques modales PSPACE

Résumé

Le solveur SAT est devenu un oracle NP e cace pour résoudre des problèmes NP-complet (voir au-delà). En gé-néral, ces problèmes sont résolus soit par une traduction di-recte vers SAT soit en résolvant itérativement des problèmes SAT dans une procédure comme CEGAR. Récemment, une nouvelle boucle CEGAR récursive travaillant sur deux ni-veaux d'abstractions, appelée RECAR, a été proposée et ins-tanciée pour la logique modale K. Nous visons à compléter ce travail pour les logiques modales utilisant les axiomes (B), (D), (T), (4) et (5). De plus, pour le rendre performant en pratique, nous généralisons le framework RECAR pour uti-liser des compositions de fonctions d'abstraction. Les résul-tats expérimentaux montrent l'e cacité de cette approche et qu'elle surpasse les solveurs de l'état de l'art pour les lo-giques modales K, KT et S4 sur les benchmarks considérés. Abstract SAT technology has become an e cient running NP-oracle for solving NP-complete problems (and beyond). Usually those problems are solved by direct translation to SAT or by solving iteratively SAT problems in a procedure like CEGAR. Recently, a new recursive CEGAR loop working with two abstraction levels, called RECAR, was proposed and instantiated for modal logic K. We aim to complete this work for modal logics based on axioms (B), (D), (T), (4) and (5). Moreover, to make it e cient in practice, we generalize the RECAR framework to deal with compositions of abstraction functions. Experimental results show that the approach is e cient and outperforms state-of-the-art modal logic solvers for modal logics K, KT and S4 on considered benchmarks.
Fichier principal
Vignette du fichier
JIAF.pdf (870.67 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02271392 , version 1 (26-08-2019)

Identifiants

  • HAL Id : hal-02271392 , version 1

Citer

Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail. Une approche SAT sensible à la mémoire pour les logiques modales PSPACE. JIAF 2019 - 13es Journées de l'Intelligence Artificielle Fondamentale, Jul 2019, Toulouse, France. ⟨hal-02271392⟩
90 Consultations
101 Téléchargements

Partager

Gmail Facebook X LinkedIn More