--- title: "A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem" authors: - "Jean-Marie Lagniez" - "Daniel Le Berre" - "Tiago de Lima" - "Valentin Montmirail" doi: "10.24963/ijcai.2017/94" url: "https://ijcai.org/proceedings/2017/94" pdf: "https://ijcai.org/proceedings/2017/0094.pdf" venue: "Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence" year: 2017 pages: "674-680" track: "Main track" keywords: - "Constraints and Satisfiability: Satisfiability" - "Constraints and Satisfiability: Modeling/Formulation" - "Knowledge Representation, Reasoning, and Logic: Non-classical logics for Knowledge Representation" --- # A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, Valentin Montmirail *Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence*, pages 674-680. DOI: [10.24963/ijcai.2017/94](https://doi.org/10.24963/ijcai.2017/94) ## Abstract Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking large systems. Since then, it has been applied to many different problems. It especially proved to be an highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both a CEGAR and a RECAR approach for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered. ## Full text ## 1 Introduction SAT technology has proven to be a very successful practical approach to solve some NP-complete problems [Biere et al., 2009]. One of the main issues is to find the "right" encoding for the problem, i.e. to find a polynomial reduction from the original problem into a propositional formula in Conjunctive Normal Form (CNF, a set of clauses) which can be e�ciently solved by a SAT solver [Prestwich, 2009]. The SAT solver is a generic problem solving engine, whose input is a satisfiability equivalent CNF representing the original problem. It often happens that either the SAT solver can solve e�ciently the CNF or not at all (see e.g. the results of the SAT competitions [J¨arvisalo et al., 2012]). A particular case is when the resulting CNF is very large: the time for generating and reading the input is greater than the time to solve it. This is due to the limited available main memory allocated to the approach and not the SAT solver itself. We address one of such particular cases in this paper. For huge CNF encodings, specific approaches have been designed in the past, where a SAT solver is used as an oracle in a more complex procedure. One such procedure is called Counter-Example-Guided Abstraction Refinement (CEGAR) [Clarke et al., 2003]. The SAT solver is fed with an abstraction of the original problem allowing more models (which we will call under-approximation). If the abstraction is unsatisfiable, then the original problem is also unsatisfiable (UNSAT shortcut). Else the procedure is able to verify if the model found for that abstraction is a correct solution for the original problem. In this case, we have an additional SAT shortcut to decide the satisfiability of the formula. If it is not the case, new constraints are added to prevent the solver from finding such spurious examples (refinement step) and the process repeats. Eventually, a complete satisfiability equivalent propositional formula is provided, and the SAT solver can decide the problem. One of the reasons for using CEGAR is that the complete formula is in practice too large to even be generated, so the only hope to solve the original problem is to "get lucky" (satisfiable shortcut) or to be able to take into account a specific structure of the problem (unsatisfiable shortcut). This framework is elegant and has been applied to many areas: Satisfiability Modulo Theory [Brummayer and Biere, 2009], Planning [Seipp and Helmert, 2013] and more recently QBF [Janota et al., 2016]. The latter is especially inspiring, because it appears to be the best practical solution overall to solve QBF formulas according to the latest QBF competition [Pulina, 2016]. The aim in this work is to follow these steps on another PSPACE complete problem, which is the satisfiability of modal logic K formulas. Several previous SAT-based approaches have already been proposed in the field of Modal Logic [Sebastiani and Tacchella, 2009], one could even argue that *SAT [Giunchiglia et al., 2002] is already a CEGAR approach for the modal logic K. In this paper, we introduce an extension of the CEGAR approach which includes a recursive step to introduce a new shortcut in the original CEGAR procedure. In our context, the main CEGAR loop contains a SAT shortcut (Esat), while the recursive step allows the procedure to provide an UNSAT shortcut (Eunsat). We call this extension "Recursive Explore and Check Abstraction Refinement" (RECAR). The idea of mixing SAT and UNSAT shortcuts in a CEGAR procedure is not new: it has been already used for SMT [Brummayer and Biere, 2009] and for bug detection [Wang et al., 2007]. Here the novelty is that we use an abstraction of the original problem in the loop, made possible by a recursive call to the main procedure. The RECAR procedure is generic, i.e. it is not bounded to a specific domain. In this paper, we present the conditions required on the abstractions used, and the correctness of the approach. Then, we instantiate our framework for the satisfiability of modal logic K, by providing abstraction functions for this problem and experimental results of the approach against the state-of-the-art provers. We believe that the good practical results we obtained by using RECAR on that particular domain are promising for other areas. This paper presents, in that respect, a generic procedure with a successful use case. The remainder of the paper is organized as follows: we first present the CEGAR approach; then we propose our new framework called RECAR and show its soundness and completeness; we provide an implementation of the RECAR approach for modal logic K; we finally compare the e�ciency of the RECAR approach against the state-of-the-art modal logic K solvers. ## 2 CEGAR Preliminaries Counter-Example-Guided Abstraction Refinement, CEGAR, is an incremental way to decide the satisfiability of formulas in classical propositional logic (CPL). It has been originally designed for model checking [Clarke et al., 2003], i.e. to answer questions such as "Does S j= P hold?" or, equivalently, "Is S ^ :P unsatisfiable?", where S describes a system and P a property. In such highly structured problems, it is often the case that only a small part of the formula is needed to answer the question. The idea behind CEGAR is to replace � = S ^ :P by an approximation � 0 , where � 0 is easier to solve in practice than �. There are two kinds of approximations: (1) an over-approximation of � is a formula ˆ� such that ˆ� j= � holds: ˆ� has at most asmanymodels as �; (2) an underapproximation of � is a formula ˇ� such that � j= ˇ� holds: ˇ� has at least as many models as �. Usually, � is in CNF. Then, a classical way to under-approximate � is to "forget" some clauses, i.e. ˇ� is a subset of the clauses in �. A model of ˇ� also may by chance satisfy �. Moreover, if ˇ� is found to be unsatisfiable, then so is �. This double possibility to conclude earlier makes under-approximation based CEGAR very popular. A classical way to over-approximate is to bound the generation of the formula � to a given n smaller than the one needed to reach equi-satisfiability to the original problem (as in bounded model checking [Clarke et al., 2003] or planning [Seipp and Helmert, 2013]). As such a model of ˆ� can be extended to a model of � but the unsatisfiability of � means that the bound n has to be increased and the process is repeated. An example of a CEGAR using over-approximations is given on Fig. 1. It receives a formula � as input and computes an over-approximation . Then it uses a SAT solver to check whether is satisfiable. If so it concludes that � is satisfiable. Otherwise, is refined, i.e. it gets closer to �, until it is satisfiable, or until the refined over-approximation is detected to be equi-satisfiable to �, denoted �sat �, (i.e. 9M; M j=1 i� 9M 0 ; M 0 j=2 �) 1 , where it concludes that � is unsatisfiable. In the following, � � ? sat means an incomplete e�cient equi-satisfiability test which returns yes or unknown. Recent SAT solvers are able to check satisfiability "under assumption" [E´en and S¨orensson, 2003], i.e. given the satisfiability of a set of literals called assumptions, and to provide in case of unsatisfiability a "reason" in terms of those literals for the unsatisfiability of a formula. 1 j=1 and j=2 denote possibly di�erent consequence relations (for propositional logic and modal logic K for instance). Figure 1: The CEGAR framework with over-approximation ![Image](https://ijcai.org/proceedings/2017/fulltext/94/image_000000_7e519a6ad1b210ea1ea079ee43a5dbabed759884747246c7520718fc1cfffb7b.png) Definition 1 (Unsatisfiable core with assumptions). Let � a CNF and A a consistent set of literals from �. Let � be satisfiable and (� ^ V a2A a) be unsatisfiable. L � A is an unsatisfiable core of � if and only if (�^ V l2L l) is unsatisfiable. Therefore, a SAT oracle for �, given A, can be seen as a procedure providing a pair (d; ) with d 2 fSAT;UNSATg and is a model of � if d = SAT or an unsatisfiable core of � if d = UNSAT. Modern SAT-based procedures are able to take into account in both cases. Unsatisfiable cores have been used for instance in a CEGAR approach for deciding the satisfiability of the propositional fragment of first-order logic [Khasidashvili et al., 2015]. ## 3 Recursive Explore and Check Abstraction Refinement A classic CEGAR approach with over-approximation and a SAT shortcut performs well when the input is satisfiable. But generally, it does not perform well in problems which are unsatisfiable. The reason is that it may have to keep refining until it reaches equi-satisfiability with the original problem. One way to address this issue is to mix SAT and UNSAT shortcuts, as in [Brummayer and Biere, 2009] and [Wang et al., 2007]. In these approaches, the methods alternate between over and under approximations. The RECAR approach, depicted in Fig. 2 and Fun. 1, interleaves both kinds of approximations: each abstraction is performed with the information retrieved from solving the previous one. The UNSAT shortcut is implemented using a recursive call to the main procedure when a strict underapproximation ˇ� can be built. One should also note that the proposed approach permits abstractions on two di�erent levels: one is used to simplify the problem at the domain level (recursive call), while the other one is used to approximate the problem at the oracle level. In order to apply RECAR, the under-approximation ˇ� and the over-approximation ˆ� must satisfy some properties. In the following, isSAT(�) means that � is satisfiable (6 j=1 :�) and isUNSAT(�) means (j=2 :�), but on possibly di�erent consequence relations. RC(�; ˇ�) denotes a Boolean function deciding if a Recursive Call should occur. Figure 2: The RECAR framework ![Image](https://ijcai.org/proceedings/2017/fulltext/94/image_000001_668fcfb2ab68d3b6160f171f779f849f3f11edb27edbde52ca96f97f01707f7d.png) ## RECAR assumptions: 1. Function 'check' is a sound and complete implementation of 'isSAT' which terminates. 2. isSAT( ˆ�) implies isSAT(refine( ˆ�)). 3. There exists n 2 N such that refine n ( ˆ�) � ? sat �. 4. isUNSAT( ˇ�) implies isUNSAT(�). 5. Let under(�) = ˇ�. There exists n 2 N such that RC(under n (�); under n+1 (�)) evaluates to false. Note that we have isSAT( ˆ�) implies � is satisfiable by Assumptions 2 and 3 together. In the following, we show that, under these assumptions, RECAR is sound, complete and terminates. To do so, we present the algorithm recar(�) in Fun. 1. ## Function 1: recar(�) ``` 1 ˆ� 2 while � ? sat � returns "unknown" do 3 if check( ) = SAT then return SAT ; 4 if RC(�; ˇ�) then 5 if recar( ˇ�) = UNSAT then return UNSAT ; 6 refine( ) ; 7 return check( ) ``` Theorem 1 (Soundness). If recar(�) returns SAT then � is satisfiable. Proof. Assume that recar(�) returns SAT. This happens only if check( ) returns SAT, either from line 3 or from line 7. Thus, we know that isSAT( ) holds (by Assump. 1). But equals to ˆ� or equals to refine n (�) for some n 2 N. Then � is satisfiable (by Assump. 2 and 3). � The intuition behind the proof of Th. 2 is that there are two ways to conclude that � is UNSAT. In the first case, ˆ� is refined a finite number of times until it is detected equisatisfiable to � and check returns UNSAT. Then � is unsatisfiable. In the second case, one of the under-approximations is shown UNSAT, then � is UNSAT (by Assump. 4). Theorem2 (Completeness). If recar(�) returns UNSAT then isUNSAT(�). Proof. By induction on the number k of recursive calls to recar (Line 5). Assume recar(�) returns UNSAT after k recursive calls. In the induction base k = 0 (no recursive call). Then we must have exited the loop ( � ? sat �) and check( ) returns UNSAT. This means that is unsatisfiable (by Assump. 1) and therefore isUNSAT(�) holds (because of equi-satisfiability). The induction hypothesis is: for all k � n, if recar(�) returns UNSAT after k recursive calls then isUNSAT(�). In the induction step k = n + 1. Then the conditions of lines 4 and 5 of the algorithm are true. This means that recar( ˇ�) returns UNSAT after k recursive calls to recar. Then isUNSAT( ˇ�) (by I.H.). Then isUNSAT(�) (by Assump. 4). � The intuition behind the proof of Th. 3 is that the function performs a finite number of recursive calls (Assump. 5). Moreover, each of these calls will have a finite number of refinements before terminating (Assump. 3). Theorem 3 (Termination). RECAR terminates for any input �. Proof. We have that (1) For all �, there exists n 2 N such that RC(under n (�); under n+1 (�)) evaluates to false (by Assump. 5) and (2) For each i � n there is mi 2 N such that refine mi ( ˆ�) � ? sat � (by Assump. 3). Then, for any input �, the recursive call of line 5 of the algorithm will be executed at most n times before the condition of line 4 becomes false. For each one of these recursive calls, the while-loop of the algorithm will be executed at most mi times before the condition of line 2 becomes false. Therefore, for any input, recar halts after at most n + � n i=0 (mi) recursive calls. � ## 4 Solving K-SAT with RECAR In this section, we show how RECAR is applied to solve the satisfiability problem for modal logic K, which is a PSPACE complete problem [Ladner, 1977; Halpern and Moses, 1992]. ## 4.1 Modal Logic K Before showing how we applied the RECAR approach, let us define formally what the modal logic K is. Let a finite non-empty set of propositional variables P = fp1; p2; : : : g and a set of m unary modal operators M = f�1; : : : ; �mg be given. The language of K (noted L) is the set of formulas containing P, closed under the set of propositional connectives f:; ^g and the set of modal operators in M. We also use the standard abbreviations for >, ?, \_ and ^. For instance ^a� = :�a:�. Definition 2 (Model). A Kripke model is a triplet M = hW; fRa j �a 2 Mg; Vi, where: W is a non-empty set of possible worlds; Each Ra � W�W is a binary accessibility relation on W; V : P ! 2 W is a valuation function which associates, to each p 2 P, the set of possible worlds from W where p is true. A pointed Kripke model is a pair hM; wi, where M is a Kripke model and w is a possible world in W. Thereafter, whenever we use the term 'model' we refer to 'pointed Kripke model'. In the following, the size of a model hM; wi, which is the number of elements in W, is denoted by jMj. Definition 3 (Satisfaction relation). The relation j= between models and formulas is recursively defined as follows: Definition 4 (Validity). As usual, a formula � 2 L is valid (noted j= �) if and only if it is satisfied by all models hM; wi. A formula � 2 L is satisfiable in K (noted isKSAT(�)) if and only if 6 j= :�. We also use isKUNSAT(�) to mean j= :�. In the sequel, we define a translation from modal logic K to classical propositional logic. Definition 5 (Translation). tr(�; n) = tr 0 (nnf(�); 0; n) The translation adds fresh variables pi and r a i; j to the formula: pi denotes that variable p is true in the world wi whereas r a i; j corresponds to wj being accessible from wi by the relation a. We have the following as an immediate result (where nm(�) is the number of modal operators in �) based on x25.2.2 [Sebastiani and Tacchella, 2009]. Theorem4. isKSAT(�) if and only if isSAT(tr(�; nm(�)+1)). Therefore, in order to decide the satisfiability of a formula � 2 L, one can simply feed a SAT solver with tr(�; nm(�)+1). In fact, this is the approach proposed in Km2SAT [Sebastiani and Vescovi, 2009]. The main issue is that the translation may generate an exponentially larger formula. In this paper, we try to circumvent this problem by using RECAR. For simplicity, from now on we use tr(�) instead of tr(�; nm(�) + 1). In [Caridroit et al., 2017], the authors also use this translation frommodal logic S5 to classical propositional logic, but replacing nm(�) by the diamond degree dd(�), which is generally smaller. Unfortunately, this cannot be used for K. The counter-example below shows why. Counter-Example 1. Let � = (p1 ^ p2 ^ p3) ^ (^a(p1 ^ p2 ^ :p3^�a(p1^:p2^p3)))^(^a(p1^:p2^:p3^�a(:p1^:p2^ p3))) ^ (�a^a p3), with dd(�) = 3. This formula is satisfied by the model in Fig. 3. However, it is easy to see that there is no model satisfying � with less than 5 possible worlds. Figure 3: M j= � ![Image](https://ijcai.org/proceedings/2017/fulltext/94/image_000002_51989c69fe2928ba332c36284adc84fba27195722f8e18d096b401f2872e2192.png) ## 4.2 Over-approximation Now, in order to apply the RECAR approach, we first need to find an over-approximation which respects the assumptions presented in Sec. 3. Definition 6 (Over-approximation). Let � 2 L. The overapproximation of �, denoted ˆ�, is the formula tr(�; 1). Definition 7 (Refinement). Let 1 � n � nm(�)+1. The refinement of tr(�; n), noted refine(tr(�; n)) is the formula tr(�; n+1). Theorem5. If isSAT(tr(�; n)) then isSAT(tr(�; n+1)), for all 1 < n � nm(�) + 1. (RECAR Assump. 2) Proof Sketch. The idea is that if � is satisfied by a model M with n worlds, then we can find a model M 0 with n + 1 worlds satisfying �. The additional world is just not accessible from the ones already in M. � The latter result allows us to use this over-approximation and refinement in the RECAR approach. It is easy to see that RECAR assumptions 2 and 3 are satisfied. ## 4.3 Under-approximation To understand the intuition behind the under-approximation we use an example. Let � = (^p^�:p^�) for some � 2 L, where nm(�) is huge. This is clearly unsatisfiable because (^p^�:p) is unsatisfiable. One can see that right away without even knowing what � looks like. However, a CEGAR approach using the over-approximation and refinement defined earlier will take a long time before finally conclude it. The reason is that each refinement tr(�; n + 1) of the original formula will be shown unsatisfiable and it will not stop until the huge number nm(�) + 1 is reached. Figure 4: How selectors are applied to � = (^p ^ �:p ^ �) ![Image](https://ijcai.org/proceedings/2017/fulltext/94/image_000003_76b57899977b48aef8fddddd33a39871922c39c60e204a3998cd539f2d637026.png) To avoid these pathological cases, the RECAR approach also performs under-approximations. To see how it works, let us take that formula � again. First, we add to each conjunct in � a fresh variable si (a selector) that will be assumed to be true by the SAT solver, as done in Fig. 4. Then, we make the first over-approximation tr(�; 1) and give it to a modern SAT solver. The solver will return UNSAT with an unsatisfiable core. From this core, we extract a set of selectors core. Let us assume, in our example, that core = fs1; s2g. This means that the formula ˇ� = (^p ^ �:p), which is the one labelled by the selectors, is enough to prove the unsatisfiability of � with only 1 possible world. Proving the unsatisfiability of ˇ� will imply that � is unsatisfiable. Note that, in this specific case, nm( ˇ�) is much smaller than nm(�). Thus the CEGAR approach applied to ˇ� will succeed much earlier, while it may have failed for the entire formula �. Formally, we have the following. ## Definition 8 (Under-Approximation). under(p; core) = p under(:p; core) = :p under(�a�; core) = �a(under(�; core)) under(^a�; core) = ^a(under(�; core)) under((� ^ ); core) = under(�; core) ^ under( ; core) The intuition of the proof is that each selector si enables an operand in a conjunction of the formula. Each time function 'under' is called with a non-empty core, operands not enabled with a selector from the core will be removed from the formula. Proof. Let � be in NNF. We show that isKSAT(�) implies isKSAT(under(�; core)) by induction on the structure of �. Assume isKSAT(�). Then 9 M; w s.t. hM; wi j= �. There are two cases in the induction base: (1) � = p and (2) � = :p. In both of them under(�; core) = �. There are four cases in the induction step: - (1) � = ^a( ). 9 M; w s.t. hM; wi j= ^a( ). Then 9 M; w 0 s.t. (w; w 0 ) 2 R, hM; w 0 i j= . Then hM; w 0 i j= under( ; core) by induction hypothesis. Thus hM; wi j= under(�; core); - (2) � = �a( ). This case is analogous to (1). - (3) � = ( ^ �). 9 hM; wi j= ( ^ �). Then hM; wi j= and hM; wi j= �. Then hM; wi j= under( ; core) and hM; wi j= under(�; core) by induction hypothesis. Thus hM; wi j= under(�; core); - (4) � = ( \_ �). We consider the three cases: - (4.a) = :si and si 2 core. Then 9 hM; wi j= (:si \_ �) but si 2 V(w), then hM; wi j= �. Then hM; wi j= under(�; core) by induction hypothesis. Thus hM; wi j= under(�; core); - (4.b) = :si and si < core. 9 hM; wi j= (:si \_ �). but we always have hM; wi j= >. Thus hM; wi j= under(�; core). Theo. 6 shows that function 'under' satisfies RECAR Assump. 4. To see that it also satisfies Assump. 5, note that the length of under n+1 (�; core) is smaller or equal to that of under n (�; core 0 ) (even though the sets core and core 0 usually di�er). Figure 5: MoSaiC : RECAR for modal logic K ![Image](https://ijcai.org/proceedings/2017/fulltext/94/image_000004_a9ed86e1077df62b863bafef49463db4a019b3bf188e54f5bf2518febbff40d9.png) ## 5 MoSaiC : RECAR for K-SAT We implemented the RECAR approach for modal logic K satisfiability problem within the solver MoSaiC, using the over and under approximations defined in the previous section. MoSaiC combines several features found in state-of-the-art solvers. As in Km2SAT [Sebastiani and Vescovi, 2009], it optimises the input by performing the rules: Box Lifting, Flattening, and Truth Propagation through modal and Boolean operators (see [Sebastiani and Vescovi, 2009] for more details). MoSaiC also uses the SAT solver Glucose in incremental mode [E´en and S¨orensson, 2003; Audemard et al., 2013] to decide the satisfiability of each . Note that some implementation details di�er a bit from Fig. 5. For instance, we do not call Glucose on but on an updated 0 with selectors on conjuncts under the assumption that these selectors are satisfied; we do not need to generate the under approximation ˇ� to test the condition ˇ� = �: we just need to know the number of selectors involved in the unsatisfiability of the formula. We also return a Kripke model in the main procedure, not just SAT/UNSAT. We take advantage of such information to provide a new bound for l. And finally, note that in our case max(jMj; l+1) always returns jMj because it is not possible to find a model smaller than M by construction of ˇ�. The CEGAR solver presented in Sec. 6 uses a similar schema, but without the recursive RECAR step. ## 6 Experiments We compared our approach against existing solvers considered state-of-the-art in [Nalon et al., 2016], namely KS P 0.1 [Nalon et al., 2016], BDDTab 1.0 [Gor´e et al., 2014], FaCT++ 1.6.4 [Tsarkov and Horrocks, 2006], InKreSAT 1.0 [Kaminski and Tebbi, 2013], *SAT 1.3 [Giunchiglia et al., 2002], Km2SAT 1.0 [Sebastiani and Vescovi, 2009] combined with the same Glucose SAT solver we use in MoSaiC, Spartacus 1.0 [G¨otzmann et al., 2010] and a combination of the optimized functional translation [Horrocks et al., 2007] with Vampire 4.0 [Kov´acs and Voronkov, 2013]. MoSaiC was configured as a standard CEGAR approach or with the proposed RECAR approach. We chose to execute these solvers on the following benchmarks: the complete set of TANCS-2000 Figure 6: Scatter-plot CEGAR vs RECAR ![Image](https://ijcai.org/proceedings/2017/fulltext/94/image_000005_3dfd922be564e80f1167b67399025d9ed53f393074a4166aa9811ba3f1178391.png) ![Image](https://ijcai.org/proceedings/2017/fulltext/94/image_000006_7448cd3ab250f062a6ee97b5cd8211c36e0ff3d2d6cd19ddfe98331b73a63fce.png) modalised random QBF (MQBF) formulae [Massacci and Donini, 2000] complemented by the additional MQBF formulae provided by [Kaminski and Tebbi, 2013], 1016 formulae, 617 satisfiable, 399 unsatisfiable; LWB basic modal logic benchmark formulae [Balsiger et al., 2000], with 56 formulae chosen from each of the 18 parametrized classes, generated from the script given by the authors of [Nalon et al., 2016], 1008 formulae, 504 satisfiable, 504 unsatisfiable; randomly generated 3CNFKSP formulae [Patel-Schneider and Sebastiani, 2011] of depth 1 or 2, 1000 formulae, 457 satisfiable, 464 unsatisfiable. Few of the considered solvers could deal with multiple modalities like MoSaiC, however to the best of our knowledge, there is no standard benchmark for modal logic K containing multiple modalities. We used a memory limit of 32GB and a runtime limit of 900 seconds per solver per benchmark. Note that due to lack of space, the results presented here are global 2 . The behavior of the solvers vary a lot with the benchmark families. We believe however that they provide an interesting insight of the capabilities of the proposed approach. RECAR vs CEGAR We can see on Fig. 6 that for most benchmarks, the RECAR approach outperforms the CEGAR one. The under approximation often provides a formula with a much smaller nm value, which produces a CNF of reasonable size to be handed in to the SAT solver. Note that in this plot, memory out for the CEGAR approach is denoted by a timeout, i.e. a point at 900s. This is mainly due to improvements in solving unsatisfiable benchmarks (1118=1367) for RECAR vs (155=1367) for CEGAR. For satisfiable benchmarks, the bound update resulting from the recursive call helps to reach faster a satisfiable formula. 1446 for RECAR vs 1053 for CEGAR. Comparison with state-of-the-art We can see on Fig. 7 that our over-approximation CEGAR approach is the worst solver whereas our RECAR approach outperforms the other solvers. Km2SAT performs specific reasoning to detect earlier some UNSAT benchmarks without generating the CNF, which explains why it performs much better than our CEGAR approach. *SAT interleaves SAT reasoning and domain reasoning, and can be considered as an under-approximation CEGAR approach. It shows good results, despite being tied with the old SAT solver SATO 3 . Our best competitor, Spartacus, is based on a tableaux method, not on SAT: SAT basedtechniques were not the best way to tackle such problems up to now. Spartacus reaches the timeout on unsolved benchmarks while we exhaust the available memory: the solvers behave quite di�erently and have di�erent limits. 2 Additional results can be found on http://www.cril. univ-artois.fr/~montmirail/mosaic Figure 7: Runtime distribution on all the benchmarks ## 7 Conclusion We proposed here a new approach to solve decision problems using a recursive abstraction refinement approach. We showed it is sound and complete and we instantiated it for the modal logic K satisfiability problem. We compared our approach against solvers representing, to the best of our knowledge, the state-of-the-art for practical K-SAT solving, on a wide range of classical modal logic benchmarks. A basic over-approximation based CEGAR approach is not competitive at all, because many of the available benchmarks are UNSAT. Our RECAR approach, mixing SAT and UNSAT shortcuts, outperformed the other solvers on the benchmarks considered. Those promising results are a first step toward more e�cient modal logic solvers: MoSaiC can be extended to other modal logics such as KT, S4, S5 and KD45, by adapting the current translation into CNF. We also believe that RECAR is an appealing framework for tackling decision problems above NP in the polynomial hierarchy. It is not clear yet for us if existing CEGAR related approaches for QBF such as [Janota et al., 2016] could fit in such framework. This is an exciting future work. ## Acknowledgments The authors would like to thank the anonymous reviewers for their insightful comments and for detecting a flaw which is now corrected. Part of this work was supported by the ANR project SATAS (ANR-15-CE40-0017), the French Ministry for Higher Education and Research and the Nord-Pas de Calais Regional Council through the "Contrat de Plan ´Etat R´egion (CPER)" and by an EC FEDER grant. 3 *SAT is deeply integrated with SATO, which makes very di�- cult an update to a more recent SAT solver. ## References 1. [Audemard et al., 2013] Gilles Audemard, Jean-Marie Lagniez, and Laurent Simon. Improving glucose for incremental SAT solving with assumptions: Application to MUS extraction. In Proc. of SAT'13, pages 309-317, 2013. 2. [Balsiger et al., 2000] Peter Balsiger, Alain Heuerding, and Stefan Schwendimann. A Benchmark Method for the Propositional Modal Logics K, KT, S4. J. Autom. Rea- soning, 24(3):297-317, 2000. 3. [Biere et al., 2009] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfi- ability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. 4. [Brummayer and Biere, 2009] Robert Brummayer and Armin Biere. Effective bit-width and under- approximation. In Proc. of EUROCAST'09, pages 304-311, 2009. 5. [Caridroit et al., 2017] Thomas Caridroit, Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima, and Valentin Montmirail. A SAT-based Approach For Solving The Modal Logic S5-Satisfiability Problem. In Proc. of AAAI'17, 2017. 6. [Clarke et al., 2003] Edmund M. Clarke, Orna Grum- berg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for sym- bolic model checking. J. ACM, 50(5):752-794, 2003. [Eén and Sörensson, 2003] Niklas Eén and Niklas Sörensson. An Extensible SAT-solver. In Proc. of SAT'03, pages 502-518, 2003. 7. [Giunchiglia et al., 2002] Enrico Giunchiglia, Armando Tac- chella, and Fausto Giunchiglia. SAT-Based Decision Pro- cedures for Classical Modal Logics. J. Autom. Reasoning, 28(2):143-171, 2002. 8. [Goré et al., 2014] Rajeev Goré, Kerry Olesen, and Jimmy Thomson. Implementing Tableau Calculi Using BDDs: BDDTab System Description. In Proc. of IJCAR'14, pages 337-343, 2014. 9. [Götzmann et al., 2010] Daniel Götzmann, Mark Kaminski, and Gert Smolka. Spartacus: A Tableau Prover for Hybrid Logic. Electr. Notes Theor. Comput. Sci., 262:127-139, 2010. 10. [Halpern and Moses, 1992] Joseph Y. Halpern and Yoram Moses. A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief. Artif. Intell., 54(2):319-379, 1992. 11. [Horrocks et al., 2007] Ian Horrocks, Ullrich Hustadt, Ul- rike Sattler, and Renate A. Schmidt. 4 Computational modal logic. Studies in Logic and Practical Reasoning, 3:181-245, 2007. 12. [Janota et al., 2016] Mikolás Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Artif. Intell., 234:1- 25, 2016. 13. [Järvisalo et al., 2012] Matti Järvisalo, Daniel Le Berre, Olivier Roussel, and Laurent Simon. The international SAT solver competitions. AI Magazine, 33(1), 2012. 14. [Kaminski and Tebbi, 2013] Mark Kaminski and Tobias Tebbi. InKreSAT: Modal Reasoning via Incremental Re- duction to SAT. In Proc. of CADE'13, pages 436-442, 2013. 15. [Khasidashvili et al., 2015] Zurab Khasidashvili, Konstantin Korovin, and Dmitry Tsarkov. EPR-based k-induction with Counterexample Guided Abstraction Refinement. In Proc. of GCAI'15, volume 36, pages 137-150, 2015. 16. [Kovács and Voronkov, 2013] Laura Kovács and Andrei Voronkov. First-Order Theorem Proving and Vampire. In Proc. of CAV'13, pages 1-35, 2013. 17. [Ladner, 1977] Richard E. Ladner. The Computational Com- plexity of Provability in Systems of Modal Propositional Logic. SIAM J. Comput., 6(3):467-480, 1977. 18. [Massacci and Donini, 2000] Fabio Massacci and Francesco M. Donini. Design and results of TANCS-2000 non-classical (modal) systems comparison. In Proc. of TABLEAUX'00, pages 52-56, 2000. 19. [Nalon et al., 2016] Cláudia Nalon, Ullrich Hustadt, and Clare Dixon. K S P : A Resolution-Based Prover for Mul- timodal K. In Proc. of IJCAR'16, pages 406-415, 2016. 20. [Patel-Schneider and Sebastiani, 2011] Peter F. Patel- Schneider and Roberto Sebastiani. A new general method to generate random modal formulae for testing decision procedures. CoRR, abs/1106.5261, 2011. 21. [Prestwich, 2009] Steven David Prestwich. CNF encodings. In Handbook of Satisfiability, pages 75-97. IOS Press, 2009. 22. [Pulina, 2016] Luca Pulina. The ninth QBF solvers evalua- tion -preliminary report. In Proc. of the 4th International Workshop (QBF 2016) co-located with (SAT 2016), pages 1-13, 2016. 23. [Sebastiani and Tacchella, 2009] Roberto Sebastiani and Ar- mando Tacchella. SAT techniques for modal and descrip- tion logics. In Handbook of Satisfiability, pages 781-824. IOS Press, 2009. 24. [Sebastiani and Vescovi, 2009] Roberto Sebastiani and Michele Vescovi. Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. J. Artif. Intell. Res. (JAIR), 35:343-389, 2009. 25. [Seipp and Helmert, 2013] Jendrik Seipp and Malte Helmert. Counterexample-guided cartesian abstrac- tion refinement. In Proc. of ICAPS'13, 2013. 26. [Tsarkov and Horrocks, 2006] Dmitry Tsarkov and Ian Hor- rocks. FaCT++ Description Logic Reasoner: System De- scription. In Proc. of IJCAR'06, pages 292-297, 2006. 27. [Wang et al., 2007] Chao Wang, Aarti Gupta, and Franjo Ivancic. Induction in CEGAR for detecting counterexam- ples. In Proc. of FMCAD'07, pages 77-84, 2007.