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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [39 references]  Display  Hide  Download

https://hal.univ-cotedazur.fr/hal-02271392
Contributor : Valentin Montmirail <>
Submitted on : Monday, August 26, 2019 - 5:35:50 PM
Last modification on : Monday, September 30, 2019 - 9:07:46 PM

File

JIAF.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02271392, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

21

Files downloads

8