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

Le solveur SAT est devenu un oracle NP e cace pour resoudre des problemes NP-complet (voir au-dela). En ge-neral, ces problemes sont resolus soit par une traduction di-recte vers SAT soit en resolvant iterativement des problemes SAT dans une procedure comme CEGAR. Recemment, une nouvelle boucle CEGAR recursive travaillant sur deux ni-veaux d'abstractions, appelee RECAR, a ete proposee et ins-tanciee pour la logique modale K. Nous visons a completer ce travail pour les logiques modales utilisant les axiomes (B), (D), (T), (4) et (5). De plus, pour le rendre performant en pratique, nous generalisons le framework RECAR pour uti-liser des compositions de fonctions d'abstraction. Les resul-tats experimentaux montrent l'e cacite de cette approche et qu'elle surpasse les solveurs de l'etat de l'art pour les lo-giques modales K, KT et S4 sur les benchmarks consideres. 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.