Solving the Satisfiability Problem of Modal Logic S5 Guided by Graph Coloring

1 Introduction

Modal logic provides a theoretical framework for important applications in many areas of artificial intelligence, including game theory [Lorini and Schwarzentruber, 2010], knowledge compilation [Bienvenu et al., 2010], contingent planning [Niveau and Zanuttini, 2016] and formal verification [Aguilera and Fern´andez-Duque, 2016; Fairtlough and Mendler, 1994]. In the past decades, automated reasoning techniques for modal logic has been vastly studied (e.g. [Balco et al., 2018; Giunchiglia and Sebastiani, 1996; Kaminski and Tebbi, 2013]).

S5 is a well-known modal logic system, which is suitable for representing and reasoning about the knowledge of a single agent [Fagin et al., 2004]. Recently, modal logic S5 is used in knowledge compilation [Bienvenu et al., 2010; Niveau and Zanuttini, 2016] and epistemic planner [Wan et al., 2015]. So, it promotes us to develop and improve automated reasoning technique for modal logic S5.

There are four common ways to tackle the modal logic satisfiability problems: tableau methods [G¨otzmann et al.,

∗Corresponding Authors

2010; Gasquet et al., 2005], first-order logic based methods [Ohlbach, 1991], resolution methods [Auffray et al., 1990; Nalon et al., 2017] and SAT-based methods [Kaminski and Tebbi, 2013; Lagniez et al., 2018]. Due to the improvement of modern SAT solvers, SAT-based methods are showing their potential and strength such as the-state-of-the-art S5 solver named S52SAT [Caridroit et al., 2017]. The SAT-based method has three advantages: 1) It can easily return a model (compared with resolution methods). 2) It can learn from the conflicts (CDCL) and utilize them. 3) It makes a good balance between guess and reasoning.

S5-SAT can be reduced to SAT based on the theoretical proof showed in [Ladner, 1977; Fagin et al., 2004]. However, naive SAT translation method will produce numerous variables and clauses. For some relatively large S5 formulas, it will cause hundreds of thousands of variables and millions of clauses. Existing SAT-based methods frequently run out of memory for these intractable scale formulas. Besides, a large number of variables and clauses will wear away the efficiency and the advantages of the SAT core.

In this paper, we propose a novel SAT-based method for S5-SAT which can save a lot of memory and significantly improve the computation efficiency. We first show a CNF-like normal form and name it S5-NF. Based on this normal form, a diamond conflict graph can be derived whose chromatic number provides an upper bound on the number of necessary worlds. In practice, the chromatic number is obtained approximately with a heuristic graph coloring algorithm, so that the extra cost is quite limited. Moreover, a lot of unnecessary search spaces can be eliminated in this process. Experimental results show that our solver outperforms the state-of-the-art S5 solvers, on some instances even by orders of magnitudes in efficiency. Besides, our solver consumes much less memory on many large scale S5 formulas.

This paper is organized as follows: first, we introduce some preliminaries about modal logic S5; then we detail the S5-NF; after that, the diamond conflict checking (DCC) strategy and the framework of solving S5-SAT will be expounded; furthermore, we evaluate and discuss the experimental results; in the final section, conclusions are drawn.

2 Preliminaries

This section briefly reviews the syntax and the semantics of modal logic S5. The set of formulas φ of S5 is a language L which extends the propositional language with the modal connectives (or modal operators) □ and ♦. □ (box) means necessity and ♦ (diamond) means possibility. For example, □p expresses the concept that "It is necessary that p" and ♦p expresses the concept that "It is possible that p". The language is defined by the grammar:

where p ∈ P and P denotes a countably infinite non-empty set of propositional variables. Logical connectives '→' and '↔' are omitted here.

Now-standard Kripke semantics for modal logic defines a frame, which consists of a non-empty set W, and a binary relation R. The members of W are generally called possible worlds. The relation R, also known as the accessibility relation, is defined between the possible worlds in W. For example, w R w′ means the world w′ is accessible from world w. I is a function W × P → {0, 1}.

S5 has the following axioms:

These axioms imply that the relation R in S5 is reflexive, symmetric and transitive. So the possible-worlds semantics for S5 can be simplified as a simple version without accessibility relation [Fitting, 1999]. The satisfiability relation ⊨ for formulas in L is recursively defined as follows:

Following the semantics (satisfiability relation), we have a list of equivalences as follows.

The diamond degree of a negation normal form φ, dd(φ), is defined recursively as:

3 ANormal Form for S5

A normal form for S5 formulas, called S5-NF, is defined in this section. It is a kind of CNF-like normal form. Actually, many CNF-like normal forms were defined in previous works for resolution such as [del Cerro, 1982; Enjalbert and del Cerro, 1989; Salhi and Sioutis, 2015]. The S5-NF is similar to these CNF-like normal forms but with some textural difference. It is designed for our solving framework, and we will show how to transform an S5 formula into an S5-NF.

3.1 Reduction Rules

First, some key rules in the transformation process are listed as follows. Note that ⊙ ∈ {□, ♦}.

The correctness of these rules is easy to verify. We present the sketch of the proof of these rules.

Lemma 1 can be easily proved according to the reflexivity, symmetry and transitivity of S5.

Applying these rules recursively we can conclude that 1) and 2) hold. These two rules can simplify multiple modal operators to one, such as □♦□♦□□φ ↔ □φ. That means each formula can only keep the nearest modal operator.

Rules 3) and 4) can be easily proved via iii) and iv) of the equivalences listed previously.

Rules 5) and 6) can be seen as supplements of 3) and 4). In fact, we can not rewrite □(p ∨ q) to the disjunction □p ∨ □q because □(p∨q) ↮ □p∨□q. But we can rewrite □(p∨♦q) to □p ∨ ♦q, as formulated in the following lemma.

One can easily prove the lemma via axioms in S5. Applying these rules recursively we can prove that 5) and 6) hold.

3.2 S5 Normal Form

S5-NF is similar to the CNF in propositional logic. So, we extend some concepts from propositional logic to name the components of S5-NF. Any S5 formula can be reduced to an equivalent one of modal degree 0 or 1 [Mints and Minc, 1992]. S5-NF is a kind of first degree normal form.

Definition 1 (S5-literal). Propositional literal p, □(p1 ∨p2 ∨ ... ∨ pj) and ♦(p1 ∧ p2 ∧ ... ∧ pk) are called S5-literal, iff ∀i ∈ N, pi is a propositional literal. The S5-literal ♦(p1 ∧ p2 ∧ ... ∧ pk) is called D-literal, and □(p1 ∨ p2 ∨ ... ∨ pj) is called B-literal.

Example 1. p, ¬q, □p, ♦¬p, □(¬p∨q∨¬r) and ♦(p∧¬q) are S5-literals.

Definition 2 (S5-clause). If ∀i ∈ N, li is an S5-literal then the disjunction of S5-literals, (l1 ∨ l2 ∨ ... ∨ ln), is called S5-clause.

Example 2. ♦¬p ∨ □(¬p ∨ q ∨ ¬r) ∨ ♦(p ∧ ¬q) is an S5clause.

Definition 3 (S5-NF). If ∀i ∈ N+, Ci is an S5-clause then the conjunction of S5-clauses, C1 ∧ C2 ∧ ... ∧ Cn, is called S5 normal form (S5-NF).

Theorem 1. Any S5 formula can be transformed into an equisatisfiable S5-NF formula.

Proof. Step1. Eliminate → and ↔. Then, transform S5 formula into an equivalent negation normal form(NNF), that is, negations appear only in front of propositional variables (definition in [Robinson and Voronkov, 2001]).

Step2. Apply the 6 reduction rules and distributive rules recursively, until the formula only contains S5-literals and ∨, ∧.

Step3. Transform the formula into conjunction normal form, in a way such as [Tseitin, 1968]. Note that during this step, each S5-literal remains intact.

After the above 3 steps, the formula is transformed into the S5-NF formula.

Fig 1 shows an example that how to transform an S5 formula into an equivalent S5-NF formula. After transformation, we get six S5-clauses.

In step 2, We use distributive rules to show the feasibility. Theoretically, only using distributive rules can blow up formula size in some cases. Introducing new variables and applying a Tseitin-like transformation locally can alleviate this problem. The following equivalences can be used to encode subformulas and x is a new variable.

Example 3. Consider the formula:

It can be rewritten as a conjunction of the following two formulas with new variables xi, yj :

In practice, many problems are formalized as:

Ai is an axiom (assumption, knowledge, state) and C is a conjecture (goal). The task is to check whether the formula is a tautology. It is equivalent to proving the following one is unsatisfiable.

In order to get S5-NF, we only need to transform each subformula Ai and ¬C to S5-clause. Generally, the size of Ai and C are not too large.

4 Dimond Elimination

In this section, we introduce a basic method to eliminate the diamond operator based on S5-NF. This method is a variant of Skolemization. In first-order logic, Skolemization is a key technique in satisfiability testing which can remove existential quantifiers from formal logic statements. For example, ∃xA(x) may be changed to A(c), where c is a new constant. The difference is that our method will not introduce new functions. In order to make our method more readable, we use first-order logical language as a transition. How to model S5-NF with propositional logic language will be discussed in Section 6.

Definition 4. Translation function tr-(φ) for an S5-NF φ is a substitution procedure which can produce a new formula:

1. ⊤⇒⊤ ⊥⇒⊥
2. For all propositional literals: p ⇒ p(0)
3. For all B-literals:
4. □(p ∨ q ∨ · · · ∨ s) ⇒ ∀x(p(x) ∨ q(x) ∨ · · · ∨ s(x))
5. For all D-literals:

♦(p ∧ q ∧ · · · ∧ r) ⇒ (p(i) ∧ q(i) ∧ · · · ∧ r(i)) The constant i is the index of the S5-clause Ci where ♦(p ∧ q ∧ · · · ∧ r) ∈ Ci.

Example 4. Based on the definition of tr-(φ), the S5-NF in Figure 1 can be rewritten as:

∀x(p(x) ∨ q(x)) ∧ ∀x(¬p(x) ∨ ¬q(x)) ∧ ∀x(¬p(x) ∨ r(x) ∨ s(x)) ∧ (p(4) ∧ ¬q(4)) ∧ {r(0) ∨ (p(5) ∧ q(5)) ∨ (p(5) ∧ ¬q(5))} ∧ (∀x¬r(x) ∨ p(6))

Theorem 2. The formula tr-(φ) is equisatisfiable with the S5-NF φ.

Proof. i) Assume tr-(φ) is satisfiable. That is, there exists a model M = 〈D, I ′ 〉 for tr-(φ) where D is a non-empty domain and I ′ is an interpretation function. Then we can construct a Kripke structure to satisfy φ where W = D and I(wi, p) = 1 iff 〈i〉 ∈ I ′ (p).

ii) Assume φ = {C1 ∧ C2, ... ∧ Cn} is satisfiable, then for each clause in φ, there exists at least one satisfied S5-literal. We pick out only one satisfied S5-literal from each Ci, these S5-literals can be denoted as F = ∧xλ=1 rλ ∧ ∧yλ=1 □(bλ,1 ∨ · · ·∨bλ,ji )∧∧zλ=1 ♦(dλ,1∧· · ·∧dλ,mλ ) where x+y+z = n. We know that F ⊢ φ, so the Kripke structure satisfies F can also satisfy φ.

1. Create z + 1 possible worlds. w0 ∈ W and if the Dliteral ♦(dλ,1 ∧ · · · ∧ dλ,mλ ) is picked out from Ci then wi ∈ W. Next, for all rλ, (W, I,w0) ⊨ rλ.
2. For all B-literals □(bλ,1 ∨ · · · ∨ bλ,ji ), ∀w ∈ W, (W, I, w) ⊨ bλ,1 ∨ · · · ∨ bλ,ji .
3. For all D-literals, if the ♦(dλ,1 ∧ · · · ∧ dλ,mλ ) is picked out from Ci then we make (W, I, wi) ⊨ dλ,1 ∧ · · · ∧ dλ,mλ .

After 3 steps, a Kripke structure satisfying F has been constructed. Based on this Kripke structure we can build a model M = 〈D, I ′ 〉 for tr-(φ). D is composed by all the constants that occur in the formula tr-(φ) and element 0. Then make 〈i〉 ∈ I ′ (p) iff (W, I, wi) ⊢ p

An S5-NF φ and tr-(φ) are equisatisfiable but may have different models. Some models can be eliminated in the translations. Intuitively, predicates p(i) can be seen as the truth value of p in the world wi. The diamond elimination process binds each D-literal with a specific world. For example, in Fig 2, M1, M2 and M3 are tree models for the original formula. However, M2 is eliminated from tr-(φ), because q must be true in the world w2. M3 is an implied situation, ¬r can be satisfied in w2 and w3 simultaneously to realize ♦¬r.

For tr-(φ), what we are concerned about is whether ¬r can

be satisfied in w3. The truth value of ¬r in the world w2 can

be ignored in search stage.

It is easy to prove that if tr-(φ) with m constants is satisfiable, then there exists a model M=〈D, I ′ 〉 satisfying the formula where |D| = m. So the satisfiability of the S5-NF φ can be decided with at most m possible worlds. Based on the definition of dd(φ), we know that dd(φ) is equivalent to m-1. It is consistent with the conclusion that the satisfiability of an S5 formula can be decided with at most dd(φ) + 1 possible worlds presented in [Caridroit et al., 2017].

5 Diamond Conflict Checking (DCC)

In Sect. 4, we know that the satisfiability of an S5-NF φ can be decided with at most dd(φ) + 1 worlds. The D-literals in the same S5-clause can be realized via the same world and the D-literals in different S5-clauses are realized via different worlds. In this context, a question naturally arises: whether can some worlds be reused to realize the D-literals in different S5-clauses? Deciding the satisfiability of φ with dd(φ) + 1 worlds is in the sense of 'at the most' which considers the worst case. Sometimes, an S5 formula can be satisfied with a small-model where |W| is smaller than the theoretical upper bound. For example, the S5-NF in Fig 2 can be satisfied with two possible worlds because ♦q and ♦¬r can be realized via the same world simultaneously.

In this section, we propose a strategy called diamond conflict checking (DCC). The basic idea is to check whether Dliterals in two S5-clauses can be in conflict when they are realized via the same world. Based on the conflict relation among these S5-clauses, we can build a graph. And, deciding which D-literals in different S5-clauses will be realized via the same world can be reduced to graph coloring by nature.

Although the conjunctive form of the D-literals provide convenience to identify the conflicts, determining the conflicts precisely is still difficult. We propose a conservative estimation of the conflicts among D-literals. What the method can guarantee is that the estimated D-literals without conflicts can be realized via the same world in safety.

Two D-literals dl1 and dl2 may interact with each other through B-literals. For example, ♦p, ♦q and □(¬p ∨ ¬q) occur in a formula simultaneously. If □(¬p ∨ ¬q) must be true, then ♦p and ♦q are in conflict when we try to realize them with the same world.

Suppose that the S5-NF formula under consideration is given and BL is the set of all B-literals in the given formula. Let PL(l) denote the set of all the propositional literals in an S5-literal l. An effect propagation set of a propositional literal p is defined as:

Then the D-literal infection set DI(dl) of a D-literal dl is defined as:

DI(dl) is an estimation of which literals may become true in the world w when we try to realize the D-literal dl via the w. Apart from the literals in PL(dl), other literals also can be true due to the B-literals.

Example 5. In Fig 1, we assume that dl is ♦p in C6, then:

In the first iteration, when we assume p in DI0(dl) is true, we can deduce r and s may become true based on □(¬p∨r ∨ s). So we have r, s ∈ DI1(dl). Based on □(¬p ∨ ¬q), we have ¬q ∈ DI1(dl)

It is easy to know that the iteration of DI(dl) will converge in 2 × Vn steps in the worst case where Vn is the number of propositional variables.

Definition 5. Let dl1 and dl2 be two D-literals. dl1 and dl2 are said to be in D-literal conflict with each other, if there exists p such that p ∈ PL(dl2) and ¬p ∈ DI(dl1).

The D-literal conflict relation is symmetric with respect to dl1 and dl2. In fact, the following holds:

There exists p such that p ∈ PL(dl2) and ¬p ∈ DI(dl1) iff there exists q such that q ∈ PL(dl1) and ¬q ∈ DI(dl2).

The details of the proof can be found in link 1 .

Definition 6. Two S5-Clauses C1, C2 are said to be in diamond conflict with each other, iff ∃dl1 ∈ C1 and ∃dl2 ∈ C2 such that dl1 and dl2 are in D-literal conflict.

Definition 7. Diamond conflict graph of an S5-NF is denoted as an ordered pair G = (V,E). V ={Ci | Ci ∈ S5NF and Ci has at least one D-literal} and E = {(Ci, Cj) | Ci and Cj are in diamond conflict with each other}.

Based on the diamond conflict graph, a vertex coloring process can be introduced to decide which D-literals in different clauses can be realized via the same world. The clauses sharing same color can reuse the same world. If the chromatic number is χ, then the upper bound of the possible worlds to

decide the satisfiability of the S5-NF is χ + 1. We name this framework as diamond conflict checking (DCC).

Algorithm 1: Dimond Conflict Checking (DCC)

Input: An S5-NF formula φ

Output: Color(Ci) and χ

• 1 Construct diamond conflict graph G = (V, E) of φ ;
• 2 Apply coloring algorithm to G ;
• 3 ∀Ci ∈ V , record Color(Ci);
• 4 χ←The chromatic number ;
• 5 return Color(Ci) and χ

Color(Ci) is the color of the clause Ci and Color(Ci) ∈ N+. Finding the optimal χ is NP-hard. It may cost too much time when the diamond conflict graph is large. Thus, we use a heuristic coloring algorithm when we implement this framework. The χ is found by a greedy algorithm which considers the vertices in descending order according to their degrees and assigns to each vertex the smallest available color in this order. This heuristic is sometimes called the Welsh-Powell algorithm [Welsh and Powell, 1967].

Improved by DCC, the 4th rule in definition 4 can be modified as:

• For all D-literals:

Fig 3 shows the diamond conflict graph of the S5-NF in Fig 1. The graph can be colored with two chromatics.

We assume that Green → 1 and Y ellow → 2. Based on the coloring result in Fig 3, the S5-NF in Fig 1 can be rewritten as:

1 http://www.square16.org/tools/s5cheetah

Compared with the basic method in Example 4, it saves a world to decide the satisfiability of the formula.

6 Solving Framework

In section 4 and 5 we use FOL and tr-(φ) as medium to introduce our method. In this section, tr-(φ) embedding with DCC will be modified to SAT version.

If an S5 formula with mmodal operators is satisfiable, then there exists an S5-model satisfying the formula with at most m+1 worlds (upper-bound) [Ladner, 1977]. Since S5-SAT is NP-Complete, encoding the S5-SAT problem into SAT can be done in polynomial time. [Caridroit et al., 2017] has shown a translation method. They also improve the upper-bound with the new metric called diamond degree. These two upperbounds are theoretical results which consider 'the worst' case.

However, for many practical instances, the satisfiability of the formula can be decided with a small number of worlds. Our method can automatically discover that potential of the input S5 formulas. The upper-bound of necessary possible worlds (χ + 1) is determined by a graph coloring algorithm.

Definition 8. The translation function tr(φ) can produce a propositional formula for an input S5-NF φ with χ+1 worlds:

1. For all propositional literals: p ⇒ p0
2. For all B-literals: □(p ∨ q ∨ · · · ∨ s) ⇒ ∧χj=0 (pj ∨ qj ∨ · · · ∨ sj)
3. For all D-literals: ♦(p ∧ q ∧ · · · ∧ r) ⇒ (pc ∧ qc ∧ · · · ∧ rc) The constant c=Color(Ci) where ♦(p∧q∧· · ·∧r) ∈ Ci.

Fresh Boolean variables pi are added to the formula, denoting the truth value of p in the world wi. In this function, the i represents the index of world. If two S5-clauses C1 and C2 are in different colors and both have ♦ϕ as a subformula, then the SAT encoding of ♦ϕ in them are different such as ϕcolor(C1) and ϕColor(C2). So, the framework of solving S5SAT problem is shown as Algorithm 2.

Algorithm 2: The Framework of solving S5-SAT

Input: An S5 formula θ

Output: The satisfiability of θ

• 1 Transform the formula θ into an equivalent S5-NF φ;
• 2 (Color(Ci), χ) ←DCC(φ);
• 3 Σ← tr(φ) ;
• 4 return result ←SAT-Solver(Σ);

This framework can be divided into two stages. The first stage uses axioms and basic rules to reduce the formula to S5-NF and applies DCC to determine the upper bound. It can help the second stage avoid some unnecessary searching spaces and reduce the upper bound of possible worlds. It also has potential to improve other methods to tackle S5-SAT.

The second stage is trying to assign some variables and find a model via SAT solvers. Clauses learning, nonchronological backtracking, and good decision heuristics of modern SAT solvers make this stage to be efficient.

For SAT-based method, the number of variables and clauses of the propositional logic are greatly influenced by the upper bound of possible worlds. The S5-NF transformation process will eliminate a lot of modal operators and DCC will reuse some necessary worlds.

Suppose the input S5 formula θ has m modal operators, dd(θ) is diamond degree and χ is the chromatic number of its diamond conflict graph. Generally, χ is less than dd(θ) and m. For example, if θ is the original formula in Figure 2, then:

If the input is an S5-NF φ, the situation χ = dd(φ) occurs when the diamond conflict graph is a complete graph.

7 Experiments

Based on our method, we implemented an S5-SAT solver named S5cheetah 1 . We compared it with the state-of-the-art solver S52SAT and tableau method solver LCKS5TabProver (LCK) [Abate et al., 2007]. S52SAT uses Glucose 4.0 as the back-end SAT solver. For fair comparison, we also choose Glucose 4.0 as back-end SAT solver and use the same InToHyLo format benchmarks. LCK is able to read that format via a simple transformation.

The well-established modal logic benchmarks include QMLTP 2 , 3CNF [Patel-Schneider and Sebastiani, 2003], QS5, MQBFK [Massacci, 1999], TANCS2000K [Massacci and Donini, 2000] and LWBK,KT,S4 [Balsiger et al., 2000]. QMLTP are designed for testing automated theorem proving systems for first-order modal logics. It contains 177 propositional benchmarks for S5 from different domain (e.g. planning, querying databases, natural language processing, general algebra). All the benchmarks in QS5 are satisfiable which are generated based on hard combinatorial design about quasigroup. Note that MQBFK, TANCS2000K and LWBK,KT,S4 are not designed for S5. However, the results on those benchmarks are still valuable. They share the same grammar and S5-SAT entails K, KT and S4-SAT. All the benchmarks can be downloaded from the link 1

The experiments are performed on a server with Intel(R) Xeon(R) CPU(2.40GHz), Ubuntu 16.04 and 64G RAM. We set the best performance parameters for S52SAT.

Table 1 shows the comparison of efficiency on each instance family. We report the number of instances which are firstly solved by each solver. And the mean time of tackling each instance family is listed in the column 'Tavg(ms)'. The time bound is set to 120s and memory bound is set to 16GB for QMLTP, LWB, MQBFK (qbfMS), and Table 1: The comparison of efficiency on all benchmarks.

2 http://www.iltp.de/qmltp/

TANCS2000K (qbfS, qbfL) as most instances of these benchmarks are relatively easy to solve. However, many instances in QS5, MQBFK (qbfML) and 3CNF cannot be solved by S52SAT within 120s with 16GB RAM. So, we set the time bound to 300s and memory bound to 64GB for them.

In Table 1, the sum of #Win of all solvers is not necessary equal to #total, since there can be certain instances on which all solvers fail. We can see that our solver S5cheetah is more efficient on these benchmarks.

Figure 4 and 5 show the comparison of run time for all instances. The x-axis corresponds to the time used by S5Cheetah and the y-axis corresponds to the time used by S52SAT and LCK. The axes are in logarithmic scale. The points above the line y=x means that our solver consumes less time on these instances.

Most of the instances in 3CNF are unsatisfiable and all instances in QS5 are satisfiable. We solved all QS5 instances and 999 3CNF instances within time bound while S52SAT solved 168 QS5 instances and 930 3CNF instances.

Table 2 shows the average number of necessary possible worlds (#W), SAT variables (#Var) and clauses (#Clauses) of each instance family. We can see that our method reduces the number of necessary worlds. It generates fewer propositional variables and clauses compared with S52SAT.

The number of SAT clauses can reflect memory usage from a certain angle. However, it does not mean actual memory usage. The solver may store some intermediate information while running. Besides, LCK is not based on SAT. So, we record the maximum memory usage for each instance family and the results are shown in Table 3.

We did not record the LCK memory consumption on TANCS, QS5 and 3CNF since LCK is barely able to solve any instance in these benchmarks. The results in Table 3 show that S5cheetah uses much less memory than other solvers. The maximum memory usage of S5cheetah for these benchmarks is 1.4GB. By contrast, S52SAT often consumes more than 1GB memory on many benchmarks and even 50GB in some extreme circumstances. Therefore, our solver is much more practical in terms of memory consumption.

8 Conclusion

We propose a novel SAT-based method to solve the S5-SAT problem and implement a fast solver called S5cheetah. First, an input S5 formula is normalized to a kind of first degree normal form, namely, S5-NF. Apart from reducing the modal degree of the original S5 formula, it can make structural and semantic information more obvious. So, a reasoning method for the candidate Kripke model comes into being. We design a strategy called diamond conflict checking (DCC) which can make good use of the structural and semantic information of the S5-NF to eliminate a lot of unnecessary search spaces and automatically discover the small-model potential of a modal logic formula.

The experiments show that our S5-SAT solver is much more efficient than some state-of-the-art S5 solvers and it consumes less memory. This significant improvement inspires us to improve other methods (e.g. Tableau) to tackle S5-SAT and study how to migrate this idea to other modal logics in the future work.

Acknowledgments

This work is supported by the Key Research Program of Frontier Sciences, Chinese Academy of Sciences (CAS), Grant No.QYZDJ-SSW-JSC036, and National Natural Science Foundation of China (NSFC) under grant No.61672504. Feifei Ma is also supported by the Youth Innovation Promotion Association, CAS.

We would like to thank the anonymous reviewers for their comments and suggestions. We thank Yongmei Liu and Qiang Liu for providing some benchmarks.