Paper deep dive
Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts
Rajeev Goré, Cormac Kikkert
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 98%
Last extracted: 7/5/2026, 8:06:13 AM
Summary
The paper investigates methods to extend CEGAR-tableaux with SAT-shortcuts for modal logic satisfiability. It compares two approaches: using the RECAR (Recursive Explore and Check Abstraction Refinement) framework and using the KSP modal resolution theorem prover as an oracle. The authors introduce CEGARBox++, a C++ implementation of CEGAR-tableaux. Experimental results on MQBF benchmarks demonstrate that using KSP as an oracle for ESAT-shortcuts is superior to both the standard CEGARBox++ and the RECAR approach, effectively integrating SAT, tableaux, and resolution methods to outperform its individual components.
Entities (6)
Relation Signals (4)
KSP → actsasoraclefor → CEGARBox++
confidence 100% · using the modal resolution theorem prover KSP as an oracle
CEGARBox++ → implements → CEGAR-tableaux
confidence 100% · Our experiments using our C++ implementation CEGARBox++ of CEGAR-tableaux
KSP → issuperiorto → RECAR
confidence 90% · CEGARBox++ using KSP to provide SAT-shortcuts is superior to both CEGARBox++ and KSP
RECAR → providesshortcutfor → CEGAR-tableaux
confidence 90% · extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR but also a totally new approach using the modal resolution theorem prover KSP as an oracle. Our experiments using our C++ implementation CEGARBox++ of CEGAR-tableaux show that: (1) CEGARBox++ with RECAR SAT-shortcuts is not competitive (2) CEGARBox++ using KSP to provide SAT-shortcuts is superior to both CEGARBox++ and KSP, particularly on large satisfiable problems. As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts.
Tags
Links
- Source: https://arxiv.org/abs/2606.31878v1
- Canonical: https://arxiv.org/abs/2606.31878v1
Trouble viewing inline? Open PDF directly →
Full Text
50,560 characters extracted from source content.
Expand or collapse full text
M. Bílková, M. Gattinger, I. van der Giessen, M. Girlando, Y. Wang (Eds.): Advances in Modal Logic 2026 (AiML 2026) EPTCS 447, 2026, p. 427–444, doi:10.4204/EPTCS.447.24 © Rajeev Goré & Cormac Kikkert This work is licensed under the Creative Commons Attribution License. Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts Rajeev Goré Faculty of Information Technology, Monash University, Australia rajeev.gore@monash.edu Cormac Kikkert Cormac Kikkert Research We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previ- ously known approach called RECAR but also a totally new approach using the modal resolution theorem proverK S Pas an oracle. Our experiments using our C++ implementationCEGARBox++of CEGAR-tableaux show that: (1)CEGARBox++with RECAR SAT-shortcuts is not competitive (2) CEGARBox++usingK S Pto provide SAT-shortcuts is superior to bothCEGARBox++andK S P, particu- larly on large satisfiable problems. As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts. 1 Introduction Propositional modal, temporal and description logics are of fundamental importance in logic-based ar- tificial intelligence, hardware and software verification [22] and knowledge representation and reason- ing [1]. Thus efficient decision procedures for modal logic are an important area of research. Such research has not matched the advances in SAT-solving, until recently, when various authors independently used SAT-solvers for modal satisfiability [19, 8, 13, 14, 9] using a technique originally due to Claessen and Rosén [5] for propositional intuitionistic logic, which was, itself, “inspired” by the work of Goré et al. on “modal clause learning” using binary decision diagrams [11]. We previously [9] presented a new type of tableaux calculus which uses a SAT-solver and the stan- dard counter-example guided abstraction refinement (CEGAR) methodology [6] to search for a rooted Kripke model for a given formula in modal clausal normal form (mcnf). We showed how to modify the initial mcnf to “compile in” the axioms T and 4 via a preprocessing stage, adding a standard loop-check for termination when required. Our Haskell implementationCEGARBoxwas, overall, the best over the standard benchmarks for the modal logics K, KT and S4, sometimes by orders of magnitude. Indeed, the only benchmark whereCEGARBoxdid not win were the K-MQBF benchmarks, where the modal resolu- tion theorem proverK S Psolved approximately 50 (out of 1000) more problems in 32 seconds each [9]: see Figure 3. When using SAT-solvers as oracles, we usually first create a formula of classical propositional logic (cpl) which is an approximation of the given (modal) formulaφ 0 . The approximation is an under- approximation ˇ φ 0 if its cpl-UNSATisfiability implies the modal unsatisfiability ofφ 0 , giving us an EUNSAT-shortcut. The approximation is an over-approximation ˆ φ 0 if its cpl-SATisfiability implies the modal satisfiability ofφ 0 , giving us aESAT-shortcut. Here we report on two ways to addESAT-shortcuts to CEGAR-tableaux: the RECAR approach and a totally new approach using the resolution-based solverK S Pas an oracle. Using our new C++ implemen- tationCEGARBox++, our experiments show that: (1)CEGARBox++with RECARESAT-shortcuts is not competitive; and (2)CEGARBox++usingK S Pto provideESAT-shortcuts is superior to each, particularly on large satisfiable problems. 428Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts M,w⊩⟨α⟩φiff∃v,R α (w,v)&M,v⊩φ M,w⊩[α]φiff∀v,R α (w,v)⇒M,v⊩φ Figure 1: Semantics of multi-modal logic K n (aka ALC) 2 Preliminaries: syntax, semantics and modal clausal normal form LetAgbe a non-empty finite set of agent names. LetAtmbe a set of atomic formulae withAtm∩Ag=/0. Consider the language of formulae defined from atomsp∈Atmandα∈Agby the BNF grammar: φ::=⊥|⊤|p|¬φ|φ∧φ|φ∨φ|[α]φ|⟨α⟩φ Define(φ 1 →φ 2 ):= (¬φ 1 ∨φ 2 )and(φ 1 ↔φ 2 ):= ((φ 1 →φ 2 )∧(φ 2 →φ 1 )). Let[α] 0 φ:=φand [α] n+1 φ:= [α][α] n φ. The modal-depth of a formula is the maximum number of nested modalities in it. For a finite setΓ=φ 1 ,·,φ k of formulae, let b Γ= (φ 1 ∧·∧φ k )and let[α]Γ=[α]φ 1 ,·,[α]φ k . The Kripke semantics for these multimodal (description) logics use Kripke models consisting of triplesM:=⟨W,R α α∈Ag ,θ⟩over some non-empty setW(of possible worlds), and binary relations R α overWfor every agentα∈Ag, and a valuationθ(w,p)⊆W×Atmtelling us the truth value of each atomic formulapat each worldw∈W. Truthhood at worldwin modelM, written asM,w⊩φ, extends the usual truth-tables for classical propositional logic (cpl): see Figure 1. A formulaφis K n -satisfiable if there is a Kripke modelMcontaining a worldwsuch thatM,w⊩φ. A formulaφis K n -valid if¬φis not K n -satisfiable. Formulaeφandψare logically equivalent ifφ↔ψ is K n -valid, and are equi-satisfiable ifφis K n -satisfiable iffψis K n -satisfiable. 2.1 Separated modal clausal normal form forK n Apositive literalis an atomic formulap. Anegative literalis a negated atomic formula¬p. Aliteralis a positive literalpor else a negative literal¬p. We useatofandlandrfor literals. We useA,B,Cand Dfor a set of literals. Let ̄ l:=¬pifl=pand ̄ l:=pifl=¬pso that ̄ ̄ l=l. A formula is innegation normal form(NNF) if it is implication-free and negations appear only in front of atomic formulae. An NNF can be created with a linear descent of the formula. Proposition 2.1.A formulaφ 0 of modal depthκcan be converted into a logically equivalent formula n f(φ 0 )in NNF which is at most polynomially longer. A modal clause is any formula of one of the following forms [21, 15, 10]: cpl-clause: a formula(l 1 ∧·∧l i )→(r 1 ∨·∨r j )of literals; box-clause: a formulaa→[α]bwith literalsaandband agent nameα∈Ag; dia-clause: a formulac→⟨α⟩dwith literalscanddand agent nameα∈Ag. Using semicolon to indicate a set-union, an arbitrary setC= (C c pl ;C box ;C dia ), of modal-clauses can be partitioned into the cpl-clausesC c pl and box-clausesC box and dia-clausesC dia as defined above. Our modal clausal normal form requires notation to succinctly express finite sequences of modalities such as[α 1 ][α 2 ]·[α k ]which naturally correspond to all finite pathsw 1 R α 1 w 2 R α 2 ·R α k w k in a Kripke model. We therefore abuse notation to extend the language of formulae using constructs from regular expressions even though they are not part of the official syntax. We use the composition operator “;” from regular expressions withεfor the empty regular expression obeying(ε;α) = (α;ε) =α. We letα 0 =εandα k>0 = (α;α k−1 ). We write[α 1 ;α 2 ;·;α k ]instead of Rajeev Goré & Cormac Kikkert429 [α 1 ][α 2 ]·[α k ], write[α n ;β m ]for[α] n [β] m and writew 1 R α 1 ;·;α k w k forw 1 R α 1 w 2 R α 2 ·R α k w k . Let Ag ∗ be the set of all finite regular expressions overAgthat use only “;” and letAg k be the set of all finite regular expressions of lengthkoverAgthat use only “;”. Proposition 2.2.A formulaφ 0 of modal depthκcan be put into an equi-satisfiable modal clausal normal form r∧ \ SNF mc (φ 0 )by naming subformulae using new atomic propositions, using r as the name forφ 0 , and where eachCbelow is a finite set of modal clauses (essentially the SNF ml of Nalon et al. [17] who prove this proposition in detail): SNF mc (φ 0 ):=C ε ; S σ∈Ag 1 [σ]C σ ;·; S σ∈Ag κ [σ]C σ Example 2.3.Consider the negationφ 0 :=¬([α](p→q)→([α]p→[α]q))of the K axiom with modal depthκ=1. Its NNF is[α](¬p∨q)∧[α]p∧⟨α⟩¬q. Puttingras the name forφ 0 gives us: C ε :=r→[α]b;r→[α]p;r→⟨α⟩¬qandC α :=b→¬p∨qwith SNF mc (φ 0 ) =C ε ;[α]C α . Note, the setC ε excludesrso we must add it explicitly to form(r; SNF mc (φ 0 )). 3 SAT-solvers with internal state as CPL-oracles CEGAR-tableaux [9] assume we have access to a SAT-solvers, with internal state, to which we can add a cpl-clauseφviaaddClause(s,φ), and which accepts a setAof literals, called unit assumptions, such asMiniSAT[7]. Intuitively, we want all literals inAto be assigned to true. When pre-loaded with a setC c pl of cpl-clauses and called withsolve(s,A), such a SAT-solver returns one of two results: (sat,θ): if(A;C c pl )is true under some cpl-valuationθ⊇Aor-else (unsat,UC): ifUC⊆Ais a, not necessarily unique, minimal “unsatisfiable core” ofAsuch that (UC;C c pl )is cpl-unsatisfiable, and hence so is(A;C c pl ). UCitself may be cpl-satisfiable but the term “unsatisfiable core” is standard. Since SAT-solvers handle classical propositional logic, they should return a cpl-valuationθ⊆Atm. That is, strictly speaking, a cpl-valuationθis just a set of atomic formulae. But in concrete applications, it may be more useful for a user to assert “I know that atomic formulacis false”, which can be achieved with¬c∈A. Thus, the valuations returned by a SAT-solver are actually a subset of the set of all literals that appear in(A;C c pl ). We can then easily extend such a set of literals to a valuation over all atoms that appear in an mcnf by putting all missing atoms to false. Example 3.1.From our previous example,φ 0 is equi-satisfiable with(r;C ε ;[α]C α ). Create a SAT- solvers0for modal depth 0, pre-loads0withC c pl ε =/0, the cpl-part ofC ε , putA ε =rbecausermust be true at modal depth 0, and callsolve(s0,A ε ): it must return(sat,θ ε )whereθ ε =r⊇A ε since (A ε ;C c pl ε ) = (r; /0) =ris true underθ ε =r. Create a SAT-solvers1for modal depth 1, pre-loads1withC c pl α =b→¬p∨q, the cpl-part ofC α , putA α =b,p,¬q, and callsolve(s1,A α ): it must return(unsat,UC α )whereUC α =b,p,¬q⊆ A α since (UC α ;C c pl σ ) =b,p,¬q,b→¬p∨qis cpl-unsatisfiable but every proper subset is cpl- satisfiable. Finally, add¬rtos0viaaddClause(s0,¬r), and restart it viasolve(s0,A ε ): it must return (unsat,UC ε )whereUC ε =r⊆A ε because(UC ε ;(C c pl ε ;¬r)) = (r;¬r)is cpl-unsatisfiable but no proper subset is so. 430Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts Algorithm 1CEGARTAB(A,Trie[σ]) 1:Inputs:Ais a set of unit assumptions, Trie[σ]is a node in our Trie containing modal clauses and a SAT-solver. 2:Lett σ := solve(Trie[σ].sat,A) isC c pl σ cpl-satisfiable 3:ift σ = (unsat,UC σ )then 4:returnUnsatisfiable(UC σ ) becauseC σ isK n -unsatisfiable 5:else ift σ = (sat,θ σ )then 6:Check box and diamond clauses that fire under classical valuationθ σ 7:for(c→⟨α⟩d)∈Trie[σ].DiaClwithc∈θ σ do 8:LetB=b|(a→[α]b)∈Trie[σ].BoxClanda∈θ σ 9:evaluate the nextα-successor using the jump rule 10:ifCEGARTAB((d;B),Trie[σ].child(α)) = Unsatisfiable(UC σ;α )then 11:CS:=c∪a|(a→[α]b)∈Trie[σ].BoxClanda∈θ σ andb∈UC σ;α 12:Letφ:= W l∈CS ¬l 13:addClause(Trie[σ].sat,φ) Learn new clauseφ:=¬ V CS 14:returnCEGARTAB(A,Trie[σ]) apply (restart) 15:end if 16:end for 17:returnSatisfiable because every fired diamond is fulfilled 18:end if Figure 2: Algorithm of CEGARTABfor multi-modal (description) logic K n (ALC) 4 CEGAR-tableaux for multi-modal logicK n (aka ALC) We now describe the CEGAR-tableaux [9] procedure extended to multi-modal logic K n (aka ALC) without local (ABox) and global (TBox) assumptions. Conceptually, the extension from mono-modal logic K to multi-modal logic K n is easy because there are no interactions between the different modalities, so we just haven“copies” of K, one for each modality[α]for every agentα∈Ag. We give the extension of the main CEGARTABalgorithm from Goré and Kikkert [9] as Algorithm 1 in Figure 2, and make the connection to the general form of SNF mc (φ 0 )but with a non-singletonAg: SNF mc (φ 0 ):=C ε ; S σ∈Ag 1 [σ]C σ ;·; S σ∈Ag κ [σ]C σ Because CEGARTABhandled only mono-modal logics, the mcnf of a given formulaφ 0 of modal depthκwas as below for a singletonAg=α(say) : SNF mc (φ 0 ):=C ε ;[α]C α ;[α 2 ]C α 2 ;·;[α κ ]C α κ Conceptually, these “modal contexts” were stored in a linear Trie (a.k.a. prefix tree) data structure with Node[0]initialised to containC ε and nodeNode[i], fori>0, initialised to containC α i , eliding the box-prefix[α i ]without loss of generality, but saving quadratic space. In the multi-modal case, we use a multi-dimensional trie and all trie-edges are labelled by an agent name and the trie-root is labelled withε. For a regular expressionσ, we writeTrie[σ]for the corre- spondingTrieNode. For example, from the trie-root nodeTrie[ε] =C ε there is a trie-path labelled by anα-edge followed by aβ-edge to the trie-nodeTrie[α;β] =C α;β . Rajeev Goré & Cormac Kikkert431 In Algorithm 1 in Figure 2, and in the implementation, eachC σ is stored at trie-positionTrie[σ]in four fields by partitioning it into its three disjoint componentsC σ = (C c pl σ ;C dia σ ;C box σ )and adding “next” pointers as follows: 1.Trie[σ].satis a dedicated SAT-solver for this trie-node pre-loaded withC c pl σ 2.Trie[σ].DiaClcontainsC dia σ := S α∈Ag c→⟨α⟩d|(c→⟨α⟩d)∈C σ 3.Trie[σ].BoxClcontainsC box σ := S α∈Ag a→[α]b|(a→[α]b)∈C σ 4.Trie[σ].Child(α)is (a pointer to) the nodeTrie[σ;α], for eachα∈Ag. The second and third fields are structured further so that we can select the dia-clauses and box-clauses for a particular agentα∈AgviaTrie[σ].DiaCl(α)andTrie[σ].BoxCl(α), respectively. We often write “formula in aTrieNode” or even “φ∈Trie[σ]" to refer to formulae that are stored in one of these fields. Recall thatrnames the initial formula but it is not in the rootTrie[ε]. Now we simply start by calling CEGARTAB(r,Trie[ε]) as shown in Figure 2. Example 4.1.Let us continue with our example. We know thatφ 0 is equi-satisfiable withr;C ε ;[α]C α , whereC c pl ε =/0 andC dia ε = (r→⟨α⟩¬q)andC box ε = (r→[α]b;r→[α]p), meaningTrie[ε].satis s0. We also haveC c pl α = (b→¬p∨q)andC dia α =/0 andC box α =/0, meaningTrie[α].satiss1. Recursion 0.The initial call to CEGARTAB(r,Trie[ε]) setsσ:=εandA:=r=A ε so line 2 issolve(s0,A ε ): it returns(sat,θ ε )whereθ ε =rso we enter the “then” part of line 5. At line 7, there is only one “fired” dia-clause(r→ ⟨α⟩¬q)∈Trie[ε].DiaCl=C dia ε withr∈θ ε , so c:=randd:= (¬q)and we know that⟨α⟩¬qmust be (modally) true at modal depth 0. Underθ ε = r, every box-clause inC box ε “fires”, thus the set[α]b,[α]pis (modally) true at modal depth 0, and hence the setB=b,pformed at line 8 must be classically true at someR α -successor for¬qat modal depth 1. To evaluate thisR α -successor, we compute(d;B) =b,p,¬qat line 10 and recurse via CEGARTAB(b,p,¬q,Trie[α].Child(α)). Recursion 1.Soσ:=αandA:=b,p,¬q=A α and the relevant SAT-solver is the “next” one so Trie[α].sat=s1. Line 2 calls this SAT-solver, so this is the callsolve(s1,A α ): it must return (unsat,UC α )whereUC α =b,p,¬qso we return Unsatisfiable(b,p,¬q) at line 4 and pop the recur- sion stack. Recursion 0.We return to line 11 whereσ:=εand so(σ;α) =α, soUC σ;α =UC α =b,p,¬q. We know the chosenθ ε at modal depth 0 caused a clash at modal depth 1 involvingb,p,¬q, and hence that[α]b,[α]p,⟨α⟩¬qcannot be jointly true at modal depth 0. At line 11 we trace the relevant box- and dia-clauses to find the conflict setCS=rat modal depth 0. To avoid this “mistake”, we compute the “refinement”φ=¬rat line 12 of recursion level 0. Line 13 is then justaddClause(s0,¬r)so C c pl ε =¬r. The refined SNF mc (φ 0 )demandsris false at the root. At line 14, we call CEGARTAB(r, Trie[ε]) but we stay at the current SAT-solver at modal depth 0 thereby restartings0. Recursion 1.Line 2 callssolve(s0,A ε ): it returns(unsat,UC ε )whereUC ε =rwhich returns Unsatisfiable(r) to line 14 of Recursion 0: our final answer. Theorem 4.2.IfTriecontains SNF mc (φ 0 )and r namesφ 0 thenCEGARTAB(r,Trie[ε]) terminates, and returns Satisfiable iffφ 0 isK n -satisfiable. 432Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts Figure 3: Performance ofCEGARBox++andK S Pon the MQBF benchmarks. Problems on the top/right edge indicate a timeout forCEGARBox++/K S Prespectively. Proof.A simple modification of the proofs for mono-modal K from Goré and Kikkert [9] which proceed by induction on the number of restarts. 5 CEGAR-tableaux with different (ESAT) shortcuts We previously showed [9] thatCEGARBoxoutperformed all solvers we tested on the extended LWB K-benchmarks, and 3CNF K-benchmarks, mostly by orders of magnitude. However, on the MQBF K- benchmarks,CEGARBoxloses toK S Pby about 50 problems. We first determine why and then explore two solutions. 5.1 Why doesCEGARBox++not win on the MQBF benchmarks? Figure 3 shows thatCEGARBox++solves all unsatisfiable benchmarks but struggles on the satisfiable ones, whileK S Psolves all satisfiable benchmarks but struggles on the unsatisfiable ones.K S Pperforms better overall as there are 617 satisfiable and 399 unsatisfiable problems in the MQBF benchmarks. By inspecting the individual (satisfiable) benchmarks thatCEGARBox++struggles on, we saw that CEGARBox++learns few clauses, and instead spends most of its time building a large model. That is, becauseCEGARBox++explicitly builds a satisfying model, a huge model can cause it to timeout. This is particularly noticeable in benchmarks with lots of branching, as it can result in satisfying models having Rajeev Goré & Cormac Kikkert433 an exponential number of worlds with respect to the size of the original benchmark.K S Pon the other hand doesn’t need to explicitly build a model to deem a formula as satisfiable, it simply applies rules untilsaturation. This is a fundamental weakness in not just CEGARTAB, but the CEGAR procedure itself. For a formulaφ, we first test whether an under-approximation ˇ φconsisting of the cpl-clauses of its mcnf is cpl-satisfiable. If ˇ φis cpl-unsatisfiable, we can perform an (EUNSAT) shortcut by immediately returning UNSAT asφmust also be modally unsatisfiable. However, there is no corresponding (ESAT) shortcut. Our observation is not new. Brummayer [3] devised an under-approximation for SMT that allows for early termination in the UNSAT case. Wang et al. [23] used induction to show the existence of large counter-models in model-checking. These frameworks are domain specific, so it is unlikely their insights would apply to CEGARTAB. However, for SAT-solving, Lagniez et al. [12] presented ageneralvariant of CEGAR, which allows for both (ESAT) and (EUNSAT) shortcuts. We first analyse the RECAR approach of Lagniez et al. [12]. We have previously shown [9] their implementation was unsound and their benchmarks were incorrect, but the theory of RECAR is sound so we incorporate their ideas [12] to create our own variant of RECAR-Tableaux. We also create our own novel approach by detecting fixpoints in our under-approximation. Al- though it is specific to recursive CEGAR algorithms, we show that it works exceptionally well, allowing CEGARBox++to solve all problems in the MQBF benchmark set bar one. Our approach combinesK S P withCEGARBox++, giving a solver that elegantly combines SAT, tableaux and resolution methods, which previously were the three competing methods for K-satisfiability. 5.2 Background on modal resolution and RECAR We first give some background on modal resolution and the RECAR framework. 5.2.1 Modal clausal resolution (K S P). Recalling the definition of SNF mc , we briefly outline the modal calculus rules ofK S P[16] for multi-modal K n , which is a resolution prover that operates on SNF ml , a close variant of SNF mc . Proposition 5.1.A formulaφ 0 of modal depthκcan be put into the equi-satisfiable separated normal form with modal layers SNF ml (φ 0 )of Nalon et al [17], who prove this proposition in detail, and where eachC i below is a set of modal clauses: SNF ml (φ 0 ):=C 0 ;[ ] 1 C 1 ;·;[ ] κ C κ Informally, but not exactly becauseK S Prequires extra clauses that are not required byCEGARBox++, we haveC l ≈ S σ∈Ag l C σ , whereC σ is from our SNF mc (φ 0 ). That is, eachC l is the “union” formed by taking a “horizontal slice” across layerl=|σ|of our “vertical tree-like” SNF mc (φ 0 ), where|σ|is the length of the Trie-pathσ. But now, SNF ml (φ 0 )can be implemented as a linear trie, rather than a branching trie as for SNF mc (φ 0 ). Let us writen:ψto indicate the clauseψis stored at then-th node in the (linear) trie, where the root is element 0. Using this notation, the resolution rules used byK S Pare presented in Figure 4. They differ from normal resolution as clauses are now labelled by their modal layer. Applying these rules will either derive an empty clause, meaningφ 0 is K n -unsatisfiable, or terminate after saturation, meaningφ 0 is K n -satisfiable. Observe the following close connection between modal resolution and CEGARTAB: all resolvents inK S Pare classical clauses as are all learnt clauses in CEGARTAB. We will use this insight to combine both these approaches. 434Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts [LRES] n:D∨ln:D ′ ∨¬l n:D∨D ′ [MRES] n:l 1 ⇒[α]ln:l 2 ⇒⟨α⟩¬l n:¬l 1 ∨¬l 2 [GEN1] n:l ′ 1 ⇒[α]¬l 1 ,·,n:l ′ m ⇒[α]¬l m ,n:l ′ ⇒⟨α⟩¬t,n+1 :l 1 ∨·∨l m ∨t n:¬l ′ 1 ∨·∨¬l ′ m ∨¬l ′ [GEN2] n:l ′ 1 ⇒[α]l 1 n:l ′ 2 ⇒[α]¬l 1 n:l ′ 3 ⇒⟨α⟩l 2 n:¬l ′ 1 ∨¬l ′ 2 ∨¬l ′ 3 [GEN3] n:l ′ 1 ⇒[α]¬l 1 ,·,n:l ′ m ⇒[α]¬l m ,n:l ′ ⇒⟨α⟩l,n+1 :l 1 ∨·∨l m n:¬l ′ 1 ∨·∨¬l ′ m ∨¬l ′ Figure 4: The resolution rules used byK S P[16]. 5.2.2 The RECAR framework (MOSAIC). RECAR (Recursive Explore and Check Abstraction Refinement) is an extension of the CEGAR approach which introduces a recursive step to allow for an additional shortcut [12]. There are two vaiants, RECAR- under, where the main CEGAR loop contains an UNSAT shortcut (EUNSAT), whilst the recursive step allows for a SAT shortcut (ESAT), and RECAR-over where the main CEGAR loop contains a SAT shortcut (ESAT), whilst the recursive step allows for an UNSAT shortcut. We present just the RECAR-under algorithm here, as the main “CEGAR” loop of the RECAR-under framework has (EUNSAT) shortcuts, like CEGAR-tableaux. This will help motivate our own application of RECAR later but note that the RECAR-over algorithm can be defined analogously (and is what is used inMOSAIC[12]). We require the following assumptions, see Figure 5, whereRCis a Boolean function that determines whether or not a recursive call occurs: Definition 5.2.Assumptions for RECAR-under [12] 1. Function ‘check’ is a sound, complete and terminating implementation that decides if an input formula is K-unsatisfiable. 2. Function refine(φ)is a function that constrainsφwith more clauses so that: (a) If the under-approximation ˇ φis K-unsatisfiable, then so is refine( ˇ φ). (b) There exists ann∈Nsuch that refine n ( ˇ φ)is K-satisfiable iffφis so. 3. If the over-approximation ˆ φis K-satisfiable, then so isφ. 4. Let over(φ) = ˆ φ. There existsn∈Nsuch thatRC(over n (φ),over n+1 (φ))evaluates to false (guar- anteeing termination). Proposition 5.3.RECAR-under is sound, complete and terminating [12]. The RECAR framework was implemented in the solverMOSAIC[12]. Briefly, the over-approximation involves checking if some formulaφis K-satisfiable with≤nworlds via a naive SAT translation, with O(Atom(φ)×n+n 2 )variables, whereAtom(φ)denotes the number of atoms inφ. The translation has variables for each world, as well as extra variables indicating which worlds are accessible from each Rajeev Goré & Cormac Kikkert435 recar(φ) UNSAT (UNSAT) ψ← ˇ φ check(ψ) θ ? |=φ sat,θ SAT yes no ψ←refine(ψ) RC(φ, ˆ φ) unk. recar( ˆ φ) (SAT) yes unsat Figure 5: The RECAR-under framework [12]. other. Over the course of the algorithm,nwill increase until it reaches the boundn=Atom(φ) depth(φ) where K-satisfiability can be determined asφis K-satisfiable if and only if it has a model withn worlds [18]. The under-approximation involves “removing” conjuncts inφ. Thus both the under- approximation and over-approximation involve reasoning about the formulaφin its entirety via a SAT- solver. This is exactly what CEGAR-tableaux aim to avoid by using a SAT-solver to only determine worlds (and not models), thus requiring onlyO(n)variables in a SAT-solver. 5.3RECARTAB: Extending CEGAR-tableaux with RECAR We now extend CEGAR-tableaux with RECAR (ESAT)-shortcuts. First, we must take some liberties when applying RECAR to CEGAR-tableaux. Note our under- approximation ˇ φ:=C c pl (φ)is a classical logic formula, whilstφis a modal logic formula. As the algorithm progresses, ˇ φwill be refined with classical clauses only, and so whilst there exists annwhere refine n ( ˇ φ)is K-satisfiable iffφis so, we are unable to detect when we have reached thisn. This differs fromMOSAIC, where the upper boundn=U B(φ)can be pre-calculated by recursively counting the number of diamond sub-formulae inφ. Second, CEGAR-tableaux already have a recursive step because they are based on recursive CEGAR loops, unlike RECAR which is based on just one CEGAR loop. These differences arise because CEGARTABconsiders only one world of the Kripke model at a time, as opposed to naive SAT-translation approaches that translate the whole input modal formula. We believe that keeping worlds separate is one of the main factors of CEGARTAB’s success, and so we keep the 436Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts under-approximation as is. Thus, instead of implementing a faithful RECAR algorithm, we shall instead perform RECAR on each world. Our under-approximation is unchanged, but our over-approximation is best motivated by an example. Algorithm 3Algorithm of RECARTABfor incorporating (ESAT) shortcuts 1:Inputs:Ais a set of unit assumptions, Trie[σ]is a node in our Trie containing modal clauses and a SAT-solver. 2:Lett σ := solve(Trie[σ].sat,A) isC c pl σ cpl-satisfiable 3:ift σ = (unsat,UC σ )then 4:returnUnsatisfiable(UC σ ) becauseC σ isK n -unsatisfiable 5:else ift σ = (sat,θ σ )then 6:LetL=l|(c→ l ⟨α⟩d)∈Trie[σ].DiaClandc∈θ σ 7:Check box and diamond clauses that fire under classical valuationθ σ 8:fori∈Ldo 9:LetD=d|(c→ l ⟨α⟩d)∈Trie[σ].DiaClandc∈θ σ andl=i 10:LetB=b|(a→[α]b)∈Trie[σ].BoxClanda∈θ σ 11:evaluate the nextα-successor using the jump rule on all fired diamonds 12:ifRECARTAB(D∪B,Trie[σ].child(α)) = Unsatisfiable(UC σ;α )then 13:LetD UC :=UC σ;α ∩DHow many diamonds in conflict set? 14:if|D UC |=1then 15:Normal clause learning 16:Findc→ l ⟨α⟩dwhered∈D UC 17:CS:=c∪a|(a→[α]b)∈Trie[σ].BoxCl,a∈θ σ ,b∈UC σ;α 18:Letφ:= W l∈CS ¬l 19:addClause(Trie[σ].sat,φ) Learn new clauseφ:=¬ V CS 20:else if|D UC |<1then 21:No diamond in conflict — pick random d∈D and simulate normal clause learning 22:Pick arbitraryd∈D 23:Findc→ l ⟨α⟩d 24:CS:=c∪a|(a→[α]b)∈Trie[σ].BoxCl,a∈θ σ ,b∈UC σ;α 25:Letφ:= W l∈CS ¬l 26:addClause(Trie[σ].sat,φ) 27:else 28:(ESAT) shortcut failed: multiple conflicting diamonds 29:for(c→ l ⟨α⟩d)∈Trie[σ].DiaClwithc∈θ σ ,l=i,d∈UC σ;α do 30:Replacelwith a fresh labell ′ inc→ l ⟨α⟩d 31:end for 32:end if 33:returnRECARTAB(A,Trie[σ]) apply (restart) 34:end if 35:end for 36:returnSatisfiable because every fired diamond is fulfilled 37:end if Rajeev Goré & Cormac Kikkert437 Suppose we are creating a model with depthn, and each world is ‘firing’ two diamond clauses. This results in creatingO(2 n )worlds, and as CEGARTABmust iterate over each of these worlds, this will clearly timeout for largen. Instead, let us create an over-approximation that will aim to reduce the number of successors for each node. Instead of creating two worlds for⟨α⟩p∧⟨α⟩q, one forpand one forq, we will attempt to create oneα-successor with (p;q). If this fails we will get a conflictA ′ , and ifp,q⊆A ′ , we know we must separate these diamond clauses. Otherwise, we have just managed to create a model forw 0 that has one successor, not two. If every world succeeds in grouping diamond clauses we can create a model withO(n)worlds instead ofO(2 n )worlds, as formalised next. 5.4RECARTAB: the RECAR-tableaux over-approximation algorithm We begin by annotating each dia-clause with a ‘label’, initialised to 1: i.e. we replacea→⟨α⟩bwith a→ 1 ⟨α⟩b, for all dia-clauses. Now, we create a sole successor for each firedlabel, instead of each fired dia-clause. The number of labels will increase as the algorithm progresses so let the set of labels beL. Theorem 5.4.Algorithm 3 forRECARTABis a sound and complete decision procedure forK n . Proof. Termination:Separating diamond clauses can happen only finitely many times. Thus for RECAR- tableaux to not terminate, it must either jump or restart infinitely, but both are impossible by the proofs for CEGAR-tableaux [9]. Soundness:Any clause learned by RECARTABis of the form¬c∨¬a 1 ∨·∨¬a m as in line 17 and 24 and is a logical consequence of the discovery that for some labell, the setc,a 1 ,·,a m ,c→ l ⟨α⟩d,a 1 → l [α]b 1 ,·,a m → l [α]b m is K-unsatisfiable just as they are in CEGARTAB, so it is sound to learn such a clause. But when the conflict set contains multiple diamonds, as in line 28, we separate these conflicting diamonds using different labels, and restart, which will reduce the cardinality ofLat line 6. This corresponds to finding that(⟨α⟩D;[α]B)is K-unsatisfiable and then attempting to K-satisfy(⟨α⟩D ′ ;[α]B)for someD ′ ⊂Dinstead. The move is sound because we maintain the requirement for (ESAT)-shortcuts that if(⟨α⟩D ′ ;[α]B)is K-satisfiable then so is each individual set(⟨α⟩d ′ ;[α]B)for alld ′ ∈D ′ . In the worst case, this will lead to every dia-clause having its own label, meaning that RECARTABwill just simulate CEGARTAB, which we know to be sound. CompletenessSuppose RECARTABreturns Satisfiable and proceed by induction on the number of jumps on the maximal sequence of jumps. If there are no jumps the Kripke model is just a dead-endw ε withθ ε . Otherwise, consider the first jump from this root world on this sequence for anyi∈L. The fired diamonds consist of some set⟨α⟩D=⟨α⟩d 1 ,·,⟨α⟩d n>0 while the fired boxes are[α]B=[α]b 1 ,·,[α]b m≥0 . We jump to a child containing the assumptions (D;B) =d 1 ,·,d n ,b 1 ,·,b m and the recursive call at line 12 must have returned Satisfiable so this childw i α must be K-satisfiable by the induction hypothesis. Thus(⟨α⟩D;[α]B)is K-satisfiable atw ε in the K-model obtained by puttingw ε R α w i α . But then so must each set(⟨α⟩d;[α]B)for everyd∈Dsince⟨α⟩(p∧q)→⟨α⟩p∧⟨α⟩qis K-valid. Thus eachi∈Lgenerates such anR α - child for its corresponding diamond jump and the for-loop over thesei∈Lat line 8 succeeds only when all such children return Satisfiable, meaning K-satisfiable. Thus every(⟨α⟩d;[α]B)fired by θ ε has a K-satisfiable witness, giving a K-model for SNF mc (φ 0 ). 438Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts 1 2 4 8 9 5 10 11 3 6 12 13 7 14 15 1 2 4 8 9 5 3 K S P CEGARTAB CEGARTAB(K S P) Figure 6: A comparison of the search process of CEGARTABand CEGARTAB(K S P). CEGARTABeval- uates worlds with a pre-order traversal, and in the meantime,K S Psaturates layers bottom-up. So CEGARTAB(K S P) generates no successors for “fixpoint” worlds 5 and 3 giving scenarios where CE- GARTAB(K S P) evaluates a linear number of worlds, whilst CEGARTABevaluates an exponential number. We report on experiments on RECAR-Tableaux at the end of this section, but let us first propose our own approach to achieving (ESAT) shortcuts. 5.5 (ESAT) shortcuts via fixpoint detection usingK S P One of the main issues with RECARTABis that it explicitly generates the model, meaning it suffers from the same shortcomings as regular CEGAR-tableaux. Sure, it uses heuristics to find smaller models, but there is no guarantee these smaller models exist, and this “optimism” might lead to wasted work. We propose a different method of finding (ESAT) shortcuts. Instead of explicitly creating a model, we simply check if one exists by searching for fixpoints in the CEGARTABunder-approximation where, intuitively, a fixpoint is a set of clauses which will never be refined with any new clauses by CEGARTAB. Lemma 5.5(Fixpoints are Satisfiable).IfA σ is a set of unit assumptions, andCEGARTABwill not refine C c pl σ with any clauses in the future, thenA σ ;C c pl σ is classically satisfiable iffA σ ;C c pl σ ;C box σ ;C dia σ isK n -satisfiable. Proof.IfA σ ;C c pl σ ;C box σ ;C dia σ is K n -satisfiable then its subsetA σ ;C c pl σ is clearly classically satisfi- able. IfA σ ;C c pl σ is classically satisfiable then CEGARTAB(A,Trie[σ])will find a classical valuation, then iterate over diamonds. For a contradiction, suppose a diamond jump returns Unsatisfiable. Then we learn a clause to add toC c pl σ , contradicting thatC c pl σ is a fixpoint. Thus all diamonds must be ful- filled, and so CEGARTAB(A,Trie[σ])returns Satisfiable. By the correctness of CEGARTAB, the set A σ ;C c pl σ ;C box σ ;C dia σ is K n -satisfiable. Lemma 5.5 allows CEGARTABto skip the potentially expensive process of generating a model if we know there are no clauses left to learn. This helps when a satisfying model is large, but “easy” to produce. But how to determine whetherC c pl σ is a fixpoint? To this end we useK S P, as explained next. 5.6 CEGAR-tableaux with a resolution-based oracle Recall thatK S Puses SNF ml rather than SNF mc and that SNF ml leads to a linear Trie data structure, as explained previously. Nevertheless, Lemma 5.5 still applies. Rajeev Goré & Cormac Kikkert439 Algorithm 4CEGARTAB(K S P)(A,Trie[l]) 1:Inputs:Ais a set of unit assumptions, Trie[l]contains the setC l of modal clauses from SNF ml (φ 0 )and a SAT-solver. 2:Merge Step: Check if external KSP process has saturated layer l wrt layer l+1(bottom-up) 3:ifexists KSP-output-file for layerlthen 4:Add new KSP clauses toTrie[l].sat 5:Fix point:=true 6:end if 7:Lett l := solve(Trie[l].sat,A) isC c pl l cpl-satisfiable 8:ift l = (unsat,UC l )then 9:returnUnsatisfiable(UC l ) becauseC l isK n -unsatisfiable 10:else ift l = (sat,θ l )then 11:ifFix point=true then 12:returnSatisfiable Fixpoint reached by KSP: skip child generation 13:end if 14:Check box and diamond clauses that fire under classical valuationθ l 15:forevery(c→⟨α⟩d)∈Trie[l].DiaClwithc∈θ l do 16:LetB=b|(a→[α]b)∈Trie[l].BoxClanda∈θ l 17:evaluate the next layer using the jump rule onα 18:ifCEGARTAB((d;B),Trie[l+1])) = Unsatisfiable(UC l+1 )then 19:CS:=c∪a|(a→[α]b)∈Trie[l].BoxClanda∈θ l andb∈UC l+1 20:Letφ:= W l∈CS ¬l 21:addClause(Trie[l].sat,φ) Learn new clauseφ:=¬ V CS 22:returnCEGARTAB(A,Trie[l]) apply (restart) 23:end if 24:end for 25:returnSatisfiable because every fired diamond is fulfilled 26:end if Figure 7: Algorithm of CEGARTAB(K S P) on SNF ml showing the integration of fixpoint detection. Theorem 5.6(K S Pproduces CEGARTABfixpoints).Suppose that asaturatedderivation from SNF ml (φ 0 ) byK S Presults in a new setC ′ l of modal clauses (at layer l). ThenC ′ l is a fixpoint ofCEGARTAB. Proof.IfC ′ l is not a CEGARTABfixpoint, the restart rule is applicable. Then the learnt clause cor- responds exactly to one of the [GEN] resolution rule applications from Figure 4 byK S P, so the set of clauses is not saturated: contradiction. Our algorithm for “fixpoint detecting” CEGAR-Tableaux is CEGARTAB(K S P) but our implementation isCEGARBox++(K S P). For simplicity,CEGARBox++(K S P) ismultithreaded, runningCEGARBox++andK S P independently, with naive communication via file writing/reading. We thank Cláudia Nalon for adjusting K S Pto make this possible. The approach is as follows where bothCEGARBox++andK S Puse the linear Trie for SNF ml , not the tree-like Trie for SNF mc , see Figure 6 and Figure 7: 1. RunK S Pon an input formulaφ 0 , and have it print out SNF ml (φ 0 ); 440Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts 2.K S Pthen performs (layered) resolution, from deepest (κ) to shallowest layers (0), and after fully saturating a layer, prints out all classical clauses it has learned; 3. CEGARTABruns independently on SNF ml (φ 0 ), from shallowest (0)to deepest (κ) layers, but when it receives clauses fromK S Pat layerl, it adds them toC c pl l (at modal layerl), marks the layer as a fixpoint and ignores the jump rule at that layer (sound by Lemma 5.5). There are some subtle points in this integration which deserve noting. At any particular time,K S P is saturating some layerlwith respect to layerl+1 using the resolution rules and adding cpl-clauses to layerlas required to avoid the jumps that would cause a clash at layerl+1. IfCEGARBox++arrives at layerlfrom layeri−1beforebeforeK S Phas saturated layerlwrt layerl+1, then the flagFixpointwill be false and line 12 will be skipped, soCEGARBox++(K S P) mimicsCEGARBox++at layerl. Else, ifK S P has already saturated layerlwrt layerl+1, and printed out new cpl-clauses, thenFixpointis put to true at line 5.CEGARBox++therefore imports the new cpl-clauses at line 4 and calls the SAT-solver at layer lat line 7 with the assumptionsA. That is,CEGARBox++checks whether the assumptionsAdemanded by the jump from layerl−1 to layerlare jointly cpl-satisfiable wrt the old cpl-clauses of layerl(inside the SAT-solver at layerl) plus these new cpl-clauses, But surely,K S Phas already told us that layerlis satisfiable, so why do we need this check? Not quite: it is perfectly possible that the new cpl-clauses make layerlcpl-unsatisfiable under assumptionsAas demanded by layerl−1, sinceK S Phas not checked this possibility (yet). Thus the call to the SAT-solver at line 7 is essential in both cases. At worst, this algorithmshouldbe as strong as CEGARTAB. As we shall see, the combination works surprisingly well, despite the rather naive integration. 5.7 Experimental evaluation of the two new approaches Our experiments used an Intel i7-11700F@2.50 GHz CPU with 16GB of RAM. We used the same K-benchmarks as in our original paper [9]. Our code can be found here:https://github.com/ cormackikkert/CEGARBoxCPP. We usedMiniSAT[7] as our SAT-solver, preliminary results showed that using other SAT-solvers leads to negligible performance differences. UsingCEGARBox++as our control, we tested our two variants that implement (ESAT) shortcuts: CEGARBox++(K S P) andRECARBox. Finally, asCEGARBox++(K S P) runs an instance ofK S P“under the hood”, we compare againstK S Ptoo. We useK S P(0.1.6), whereas our previous work [9] used version 0.1.3 (the latest at that time). SinceCEGARBox++(K S P) uses multi-threading, CPU-time is not an appropriate measure of perfor- mance, so all reported times are “wall time”, not CPU-time. Figure 8 shows that in all casesRECARBoxis worse thanCEGARBox++, likely meaning that the extra work required to look for smaller models is wasted. On the other hand we see thatCEGARBox++(K S P) outperformsCEGARBox++by a large margin on the MQBF benchmarks and is equal on the 3CNF bench- marks. However,CEGARBox++outperformsCEGARBox++(K S P) on the LWB-K benchmarks. This results in both provers being about equal overall.RECARBoxperforms better thanCEGARBox++(K S P) on the LWB-K benchmarks, which we believe is due to the presence of massive formulae in these benchmarks: see our conclusion. Synergy vs. ParallelismFinally, as the integration involves multithreading, one might wonder whether the performance gains are due to the parallelism itself (effectively “cheating” by doubling resources). Specifically for the MQBF benchmarks, isCEGARBox++helpingto solve the satisfiable problems, or is it simply justK S Psolving them all (since it is best on satisfiable formulae)? Rajeev Goré & Cormac Kikkert441 Figure 8: Performance of solvers on the standard K benchmarks To this end, we compareCEGARBox++(K S P) withK S Pin Figure 9. We can see that on hard satisfiable benchmarks,CEGARBox++(K S P) outperformsK S P, meaning thatCEGARBox++is contributing. We can see no satisfiable timeouts forCEGARBox(K S P), and even see a 100x improvement in some satisfiable problems, refuting the possibility that this improvement comes just from the doubling of resources due to parallelisation. This highlights a distinction between a simple portfolio approach and our integration. WhileK S P andCEGARBox++generally excel at different problem types (satisfiable vs. unsatisfiable), the integration appears to be better than the sum of their parts. Communicating fixpoints has allowed us to achieve results that a non-communicating portfolio could not. 6 Conclusions We can see that RECAR-tableaux doesn’t perform that well. We believe this is because it operates on a much stricter form of (ESAT) shortcuts, where it tries to create smaller models, as opposed to CEGARTAB(K S P), which doesn’t create models, but just shows they exist. Creating smallest models is intractable [4, 24] in general, and if they don’t exist, RECAR-tableaux simply wastes its time. 442Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts Figure 9: Performance ofCEGARBox++(K S P) andK S Pon the MQBF benchmarks. Problems on the top edge and the right edge indicate a timeout forCEGARBox++(K S P) andK S Prespectively. Problems in the bottom right triangle/top left triangle are solved byCEGARBox++(K S P) /K S Pquickest. Our approach, CEGARTAB(K S P), for dealing with (ESAT) shortcuts shows a lot of promise, outper- forming all solvers on the MQBF benchmarks. We believe a better implementation would result in CEGARTAB(K S P) outperforming CEGARTABacross the board. In particular, the issue with the current approach is that theK S Pnormal forming procedure produces approximately two times as many clauses as CEGARTAB, resulting in slowdowns onmassiveformulae, which are present in the LWB-K benchmarks. These are whyRECARBoxperforms better thanCEGARBox++(K S P) on the LWB-K benchmarks.K S Pcan simplify this normal form (resulting in a smaller number of clauses than CEGARTAB), but on these mas- sive formulae the simplification times out. A more polished integration would use CEGARTAB’s normal forming procedure, and have better and more real-time communication protocols. We imagine this would be capable of outperforming CEGARTABon the 3CNF and LWB-K benchmarks, whilst also full-solving the MQBF benchmarks. An implementation of such is easier said than done asK S Phas certain re- quirements on its normal form and must produce extra clauses that are not needed for CEGARTAB. An alternative would be to instead optimise the simplification process ofK S P, so it can produce reasonable normal forms quickly. In general, this idea of searching for fixpoints is simply a method of detecting if ˇ φandφare equi- satisfiable, a normal idea in classical CEGAR, but more difficult in complicated CEGAR algorithms, where the under-approximation is a different type to the input (in our case a classical formula vs a modal formula). This fixpoint approach will be generally useful for other recursive CEGAR algorithms, such as Rajeev Goré & Cormac Kikkert443 CAQE [20], or PDR [2], though of course it is most effective in applications such as CEGARTABwhere branching is involved, meaning any (ESAT) shortcut can possibly result in an exponential improvement in speed. Whilst any approach could be used for fix-point detection, it is interesting to consider the implications of using resolution here. Previously, SAT-based, tableaux-based and resolution-based solvers were the state-of-the-art solvers used for reasoning in modal K. Now, CEGARTAB(K S P), is an elegant combination of all these approaches, that is greater than the sum of its parts. In particular, this highlights a key similarity of CEGARTABand resolution methods. In CEGARTABwe learn clauses when we need to (i.e. lazily), whereasK S Plearns clauses iteratively (i.e.eagerly). We usedK S Pas an oracle for CEGARTAB. From discussion with Cláudia Nalon, Clare Dixon, Ullrich Hustadt, and Fabio Papacchini, creating an efficient implementation by reversing the roles is not obvious. References [1] Franz Baader, Ian Horrocks & Ulrike Sattler (2008):Description logics.Foundations of Artificial Intelligence 3, p. 135–179. [2] Aaron R. Bradley (2011):SAT-Based Model Checking without Unrolling. In Ranjit Jhala & David A. Schmidt, editors:Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings,Lecture Notes in Computer Science 6538, Springer, p. 70–87, doi:10.1007/978-3-642-18275-4_7. [3] Robert Brummayer & Armin Biere (2009):Effective Bit-Width and Under-Approximation. In Roberto Moreno-Díaz, Franz Pichler & Alexis Quesada-Arencibia, editors:Computer Aided Systems Theory - EU- ROCAST 2009, 12th International Conference, Las Palmas de Gran Canaria, Spain, February 15-20, 2009, Revised Selected Papers,Lecture Notes in Computer Science5717, Springer, p. 304–311, doi:10.1007/978- 3-642-04772-5_40. [4] T. Y. Chen, Jean-Louis Lassez & Graeme S. Port (1986):Maximal Unifiable Subsets and Minimal Nonunifi- able Subsets.New Gener. Comput.4(2), p. 133–152, doi:10.1007/BF03037439. [5] Koen Claessen & Dan Rosén (2015):SAT Modulo Intuitionistic Implications. In Martin Davis, Ansgar Fehnker, Annabelle McIver & Andrei Voronkov, editors:Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, Lecture Notes in Computer Science9450, Springer, p. 622–637, doi:10.1007/978-3-662-48899-7_43. [6] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu & Helmut Veith (2003):Counterexample- guided abstraction refinement for symbolic model checking.J. ACM50(5), p. 752–794, doi:10.1145/876638.876643. [7] Niklas Eén (2006):The Minisat page.http://minisat.se/. [8] Luca Geatti, Nicola Gigante & Angelo Montanari (2021):BLACK: A Fast, Flexible and Reliable LTL Satis- fiability Checker. In Dario Della Monica, Gian Luca Pozzato & Enrico Scala, editors:Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Twelfth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021), Padua, Italy, September 22, 2021,CEUR Workshop Proceedings2987, CEUR-WS.org, p. 7–12. Available athttps://ceur-ws.org/Vol-2987/paper2.pdf. [9] Rajeev Goré & Cormac Kikkert (2021):CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause- Learning and SAT. In Anupam Das & Sara Negri, editors:Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings,Lecture Notes in Computer Science12842, Springer, p. 74–91, doi:10.1007/978-3-030- 86059-2_5. 444Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts [10] Rajeev Goré & Linh Anh Nguyen (2009):Clausal Tableaux for Multimodal Logics of Belief.Fundam. Informaticae94(1), p. 21–40, doi:10.3233/FI-2009-115. [11] Rajeev Goré & Jimmy Thomson (2013):An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description. In Maria Paola Bonacina, editor:Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, Lecture Notes in Computer Science7898, Springer, p. 275–281, doi:10.1007/978-3-642-38574-2_19. [12] Jean-Marie Lagniez, Daniel Le Berre, Tiago de Lima & Valentin Montmirail (2017):A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem. In Carles Sierra, editor:Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, ijcai.org, p. 674–680, doi:10.24963/ijcai.2017/94. [13] Jianwen Li, Shufang Zhu, Geguang Pu & Moshe Y. Vardi (2015):SAT-Based Explicit LTL Reasoning. In Nir Piterman, editor:Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings,Lecture Notes in Computer Science9434, Springer, p. 209–224, doi:10.1007/978-3-319-26287-1_13. [14] Jianwen Li, Shufang Zhu, Geguang Pu, Lijun Zhang & Moshe Y. Vardi (2019):SAT-based explicit LTL reasoning and its application to satisfiability checking.Formal Methods Syst. Des.54(2), p. 164–190, doi:10.1007/S10703-018-00326-5. [15] Grigori Mints (1988):Gentzen-type systems and resolution rules part I propositional logic. In:International Conference on Computer Logic, Springer, p. 198–231, doi:10.1007/3-540-52335-9_55. [16] Cláudia Nalon, Clare Dixon & Ullrich Hustadt (2019):Modal Resolution: Proofs, Layers, and Refinements. ACM Trans. Comput. Log.20(4), p. 23:1–23:38, doi:10.1145/3331448. [17] Cláudia Nalon, Ullrich Hustadt & Clare Dixon (2017):KSP: A Resolution-based Prover for Multimodal K, Abridged Report. In Carles Sierra, editor:Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, ijcai.org, p. 4919–4923, doi:10.24963/ijcai.2017/694. [18] Linh Anh Nguyen (1999):A New Space Bound for the Modal Logics K4, KD4 and S4. In Miroslaw Kuty- lowski, Leszek Pacholski & Tomasz Wierzbicki, editors:Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS’99, Szklarska Poreba, Poland, September 6-10, 1999, Proceed- ings,Lecture Notes in Computer Science1672, Springer, p. 321–331, doi:10.1007/3-540-48340-3_29. [19] Thomas Pagram (2015):Using decision diagrams for modal and intuitionisic theorem proving. Australian National University. [20] Markus N. Rabe & Leander Tentrup (2015):CAQE: A Certifying QBF Solver. In Roope Kaivola & Thomas Wahl, editors:Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015, IEEE, p. 136–143, doi:10.1109/FMCAD.2015.7542263. [21] Grigori S Tseitin (1983):On the complexity of derivation in propositional calculus.Automation of reasoning: 2: Classical papers on computational logic 1967–1970, p. 466–483, doi:10.1007/978-3-642-81955-1_28. [22] Moshe Y. Vardi (2009):From Philosophical to Industrial Logics. In Ramaswamy Ramanujam & Sundar Sarukkai, editors:Logic and Its Applications, Third Indian Conference, ICLA 2009, Chennai, India, January 7-11, 2009. Proceedings,Lecture Notes in Computer Science5378, Springer, p. 89–115, doi:10.1007/978- 3-540-92701-3_7. [23] Chao Wang, Aarti Gupta & Franjo Ivancic (2007):Induction in CEGAR for Detecting Counterex- amples.In:Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings, IEEE Computer Society, p. 77–84, doi:10.1109/FAMCAD.2007.21. [24] David A. Wolfram (1989):Intractable Unifiability Problems and Backtracking.J. Autom. Reason.5(1), p. 37–47, doi:10.1007/BF00245020.