Une approche SAT sensible à la mémoire pour les logiques modales PSPACE
Abstract
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.
Domains
Artificial Intelligence [cs.AI]Origin | Files produced by the author(s) |
---|
Loading...