SAT-Based Decision Procedures for Classical Modal Logics.
We present a set of SAT-based decision procedures for various classical modal logics. By SAT based, we mean built on top of a SAT solver. We show how the SAT-based approach allows for a modular implementation for these logics. For some of the logics we deal with, we are not aware of any other implementation. For the others, we define a testing methodology that generalizes the 3CNFi>K methodology by Giunchiglia and Sebastiani. The experimental evaluation shows that our decision procedures perform better than or as well as other state-of-the-art decision procedures.
Introduction
Propositional reasoning is a fundamental problem in many areas of
Computer Science. Many researchers have put, and still put, years of
eort in the design and implementation of new and more powerful SAT
solvers. Most importantly, the source code of many of these implementations
is freely available and can be used as a basis for the development
of decision procedures for more expressive logics (see, e.g., (Giunchiglia
and Sebastiani, 1996a; Cadoli et al., 1998)).
In this paper, we present a set of SAT-based decision procedures for
various classical modal logics (Montague, 1968; Segerberg, 1971). By
SAT-based, we mean built on top of a SAT solver. We show how the
SAT-based approach allows for a modular implementation for these
logics. For some of the logics we deal with, we are not aware of any
other implementation. For the others, we dene a testing methodology
which generalizes the 3CNFK methodology by Giunchiglia and
(1996a). The experimental evaluation shows that our deci-
1999 Kluwer Academic Publishers. Printed in the Netherlands.
A. Tacchella
sion procedures perform better than or as well as other state-of-the-art
decision procedures.
Our approach, rst suggested by Giunchiglia and Sebastiani (1998),
consists of two steps:
1. take o the shelf one of the fastest SAT procedures available, and
2. use it as the basis for your modal decider.
Our approach diers from most of the previous works in decision
procedures for modal logics, which are either tableau-based, (i.e., based
on Smullyan's tableau for propositional logic (Smullyan, 1968): see,
e.g., (Fitting, 1983; Massacci, 1994; Baader et al., 1994)), or translation-based
(i.e., based on a reduction to rst order logic: see, e.g., (van
Benthem, 1984; Ohlbach, 1988; Hustadt and Schmidt, 1997a)). Some
of the dierences and advantages of the SAT-based approach with respect
to the tableau based and translation based approaches have been
already pointed out in (Giunchiglia and Sebastiani, 1996b; Giunchiglia
et al., 1998). Here we show how the SAT-based approach provides for a
simple and natural schema for the development of decision procedures
for modal logics.
Our approach diers also from the approaches by Horrocks (1998)
and Patel-Schneider (1998). These authors developed their own SAT
checker and used it as a basis for their modal decider. This approach
allows for a better integration among the dierent modules of the system
and for a ner tuning of the reasoning strategies. On the other
hand, it does not exploit the great amount of ongoing work on SAT
deciders. Each year, new and faster SAT engines are proposed. With
some standard modications of the source code we can inherit in the
modal setting all the benets of state-of-the-art propositional checkers. 1
Finally, our system, called *sat, improves also on previous works
by Sebastiani and ourselves (1996a; 1996b; 1998). In particular,
*sat is built on top of the SAT decider sato (Zhang, 1997). *sat
inherits many of the sato congurable options, and allows for
some more options (including early pruning, caching, two forms of
backjumping, and the choice of various splitting heuristics); and
*sat is able to deal with 8 modal logics, namely E, EM (=M),
EN, EMN, EC, EMC (=R), ECN, EMCN (=K) (see (Chellas,
1980)). For EN, EMN, EC and ECN, we do not know of any
similar point is made by Kautz and Selman (1998) as an explanation for the
better performances of SATPLAN with respect to specialized engines for planning
problems.
SAT-Based Decision Procedures for Classical Modal Logics 3
other implemented decision procedure, nor of any reduction to a
formalism for which a decision procedure is available.
The paper is structured as follows. In Section 2 we review some
basic denitions about classical modal logics. Then, in Section 3, we
present the idea of the SAT-based approach to modal reasoning, and
discuss in detail the algorithms for the 8 logics we consider. Section 4
is devoted to *sat: it discusses some of the motivations underlying
its construction, and some of its features. The experimental analysis
comparing *sat with other state-of-the-art decision procedures is done
in Section 5. Our analysis is restricted to K (for which there are several
systems available) and E (for which there exists a reduction to bimodal
K). We end in Section 6 with the conclusions and the future work.
2. Classical modal logics
Following (Chellas, 1980), a modal logic is a set of formulas (called
theorems) closed under tautological consequence. Most modal logics
are closed under the rule
for certain values of n. If then the logic is said to be monotone.
then the logic is said to be regular. If n  0 then the logic is
said to be normal. The smallest monotone, regular and normal modal
logics are called M, R and K respectively (see, e.g., (Chellas, 1980)).
Classical modal logics (Montague, 1968; Segerberg, 1971) are weaker
than normal modal logics. In fact, the only requirement is that the set
of theorems is closed under the rule
As a consequence, the schemas
2 The symbols > and ? are 0-ary connectives representing truth and falsity
respectively.
4 E. Giunchiglia, F. Giunchiglia and A. Tacchella
which are theorems in K do not necessarily hold in classical modal
logics. The three principles N, M, and C enforce closure conditions on
the set of provable formulas which are not always desirable, especially if
the 2 operator has an epistemic (such as knowledge or belief) reading.
If we interpret 2' as \a certain agent a believes '", then N enforces
that a believes all the logical truths, M that a's beliefs are closed under
logical consequence, and C that a's beliefs are closed under conjunction.
These three closure properties are dierent forms of omniscience, and
|as such| they are not appropriate for modeling the beliefs of a real
agent (see, e.g., (Giunchiglia and Giunchiglia, 1997) and (Fagin et al.,
Chapter 9). We can easily imagine situations involving a's beliefs,
where only an arbitrary subset of the above properties holds.
There are eight possible ways to add the three schemas M, C, and
N to the smallest classical modal logic E. The resulting modal logics
are called E, EM (equivalent to the logic M), EN, EMN, EC, EMC
(equivalent to R), ECN, EMCN (equivalent to K), where EX denotes
the logic obtained adding the schemas in X to E.
3. SAT-based procedures for classical modal logics
We say that a conjunction  of propositional literals and formulas of the
form 2' or :2' is an assignment if, for any pair ; 0 of conjuncts in
, it is not the case An assignment  satises a formula
' if  entails ' by propositional reasoning. A formula ' is consistent
in a logic L (or L-consistent) if :' is not a theorem of L, i.e., if :' 62
L.
Consider a formula '. Let S be a set of assignments satisfying ', and
let L be a modal logic. As noticed by Sebastiani and Giunchiglia (1997),
the following two facts hold:
If at least one assignment in S is L-consistent then ' is L-consistent.
If no assignment in S is L-consistent then ' is not L-consistent as
long as the set S is complete for ', i.e., as long as the disjunction
of the assignments in S is propositionally equivalent to '.
From these facts, it follows that the problem of determining whether '
is L-consistent can be decomposed in two steps:
generate an assignment  satisfying ', and
test whether  is L-consistent.
In all the logics we consider, testing the consistency of an assignment
amounts to determining the consistency of other formulas whose
SAT-Based Decision Procedures for Classical Modal Logics 5
depth (i.e., the maximum number of nested 2 operators) is strictly minor
than the depth of . This implies that we can check the consistency
of these other formulas by recursively applying the above methodology,
at the same time ensuring the termination of the overall process. The
above methodology can be implemented by two mutually recursive
procedures:
Lsat(') for the generation of assignments satisfying ', and
Lconsist() for testing the L-consistency of each generated assignment
.
In order to simplify the presentation, we rst present Lconsist(),
and then Lsat(').
3.1. Lconsist()
Whether an assignment is consistent, depends on the particular logic
being considered. Furthermore, depending on the logic L considered,
the consistency problem for L (i.e., determining whether a formula is
consistent in L) belongs to dierent complexity classes. In particular,
the consistency problem for E, EM, EN, EMN is NP-complete, while
for EC, ECN, EMC, EMCN it is PSPACE-complete (see (Vardi, 1989;
Fagin et al., 1995)). Here, to save space, we divide these eight logics in
two groups. We present the algorithms for checking the L-consistency
of an assignment rst in the case in which L is one of E, EM, EN, EMN,
and then in the case in which L is one of the others.
3.1.1. Logics E, EM, EN, EMN
The following Proposition is an easy consequence of the results presented
in (Vardi, 1989).
PROPOSITION 1. Let
be an assignment
in which
is a propositional formula. Let L be one of the logics E, EM,
EN, EMN.  is consistent in L if for each conjunct :2 j in  one of
the following conditions is satised:
L-consistent for each conjunct 2 i in , and L=E;
L-consistent for each conjunct 2 i in , and L=EM;
are L-consistent for each conjunct 2 i in
, and L=EN;
are L-consistent for each conjunct 2 i in ,
and L=EMN.
6 E. Giunchiglia, F. Giunchiglia and A. Tacchella
function Lconsist(
foreach conjunct 2 j do
foreach conjunct 2 i do
if M [i;
if M [j;
if M [j; False then return False
if M [j;
if M [j; False then return False
return True.

Figure

1. Lconsist for E, EM, EN, EMN
When implementing the above conditions, care must be taken in order
to avoid repetitions of consistency checks. In fact, while an exponential
number of assignments satisfying the input formula can be generated by
Lsat, at most n 2 checks are possible in L, where n is the number of \2"
in the input formula. Given this upper bound, for each new consistency
check, we can cache the result for a future possible re-utilization in a
This ensures that at most n 2 consistency checks will
be performed. In more detail, given an enumeration of
the boxed subformulas of the input formula, M[i,j], with i 6= j, stores
the result of the consistency check for (' i ^:' j ). M[i,i] stores the result
of the consistency check for :' i . Initially, each element of the matrix
M has value Undef (meaning that the corresponding test has not been
done yet). The result is the procedure Lconsist in Figure 1.
Consider Figure 1 and assume that L=E or L=EN. Given a pair of
conjuncts 2 i and :2 j , we split the consistency test for (
in two simpler sub-tests:
rst, we test whether
only if this test gives False, we test whether (:
SAT-Based Decision Procedures for Classical Modal Logics 7
Notice also that, in case L=EN or L=EMN, if we know that, e.g.,
consistent and we store this
result in M[j,j].
PROPOSITION 2. Let
be an assignment
in which
is a propositional formula. Let L be one of the logics E, EM,
EN, EMN. Assume that, for any formula ' whose depth is less than
the depth of , Lsat(')
returns True if ' is L-consistent, and
False otherwise.
returns True if  is L-consistent, and False otherwise.
Proof: The Proposition is an easy consequence of the hypotheses and
Proposition 1.
3.1.2. Logics EC, ECN, EMC, EMCN
The following Proposition is an easy consequence of the results presented
in (Vardi, 1989).
PROPOSITION 3. Let
be an assignment
in which
is a propositional formula. Let  be the set of formulas  i
such that 2 i is a conjunct of . Let L be one of logics EC, ECN,
EMC, EMCN.  is consistent in L if for each conjunct :2 j in  one
of the following conditions is satised:
L-consistent for each non empty subset
0 of , and L=EC;
L-consistent for each subset  0 of , and
is empty or ((
Assume that L=EC or L=ECN. The straightforward implementation
of the corresponding condition may lead to an exponential number of
checks in the cardinality jj of . More carefully, for each conjunct
in , we can perform at most jj
1. for each formula  i in , we rst check whether (:
consistent in L. Let  0 be the set of formulas for which the above
test fails. Then,
8 E. Giunchiglia, F. Giunchiglia and A. Tacchella
function Lconsist(
is a conjunct of g;
foreach conjunct 2 j do
foreach conjunct 2 i do
if M [j;
if M [j;
if not Lsat(
return True.

Figure

2. Lconsist for EC, ECN, EMC (R), EMCN (K)
2. in case L=ECN or  0 6= ;, we perform the last test, checking
whether ((
consistent in L.
Furthermore, the result of the consistency checks performed in the rst
step can be cached in a matrix M analogous to the one used in the
previous subsection.
If L=EC or L=ECN, the procedure Lconsist in Figure 2 implements
the above ideas. Otherwise, it is a straightforward implementation
of the conditions in Proposition 3.
PROPOSITION 4. Let
be an assignment
in which
is a propositional formula. Let L be one of logics EC, ECN,
EMC, EMCN. Assume that, for any formula ' whose depth is less than
the depth of , Lsat(')
returns True if ' is L-consistent, and
False otherwise.
returns True if  is L-consistent, and False otherwise.
Proof: The Proposition is an easy consequence of the hypotheses and
Proposition 3.
SAT-Based Decision Procedures for Classical Modal Logics 9
function Lsat(')
return Lsatdp (cnf('), >).
function Lsatdp (', )
if f a unit clause (l) occurs in ' g
then return Lsat dp (assign(l;
l := choose-literal('; );
return Lsat dp (assign(l; '), ^ l) or
base */
/* backtrack */
/* unit */
/* split */

Figure

3. Lsat and Lsat dp
3.2. Lsat(')
Consider a formula '. Let L be a modal logic. The generation of assignments
satisfying ' is independent of the particular logic L being
considered. Furthermore, it can be based on any procedure for SAT:
if the SAT decider is complete, then we can generate a nite and
complete set of assignments for ' as follows:
at step 0, ask for an assignment satisfying ', and
at step i for an assignment satisfying ' and the
negation of the assignments generated in the previous steps.
By checking the L-consistency of each assignment, we obtain a
correct and complete decider for L.
if the SAT decider is correct but incomplete, then we cannot generate
a complete set of assignments for ', but we can still build
a correct but incomplete decider for L by checking each generated
assignment. Of course, whether an incomplete eective procedure
for SAT can be turned into an eective incomplete procedure for
a modal logic L, is still an open point.
The above method for generating a complete set of assignments
for ' has the advantage that the SAT decider is used as a blackbox.
A. Tacchella
The obvious disadvantage is that the size of the input formula checked
by the SAT solver may become exponentially bigger than the original
one. A better solution is to invoke the test for L-consistency inside the
procedure whenever an assignment satisfying the input formula
is found. In the case of the Davis-Putnam (DP) procedure (Davis and
Putnam, 1960), we get the procedure Lsat represented in Figure 3. In
the gure,
cnf(') is a set of clauses |possibly with newly introduced propositional
variables| such that, for any assignment  in the extended
language, the following two properties are satised: 3
1. if  satises cnf(') then the restriction of  to the language of
2. if  satises ' then there exists an assignment in the language
of cnf(') which (i) extends  and (ii) satises cnf(').
Examples of such conversions are the \classical conversion" (which
given a formula in negative normal form recursively distribute
conjunctions over disjunctions), and the conversions based on \re-
naming", such as those described in (Tseitin, 1970; Plaisted and
Greenbaum, 1986; de la Tour, 1990).
choose-literal('; ) returns a literal occurring in ' and chosen
according to some heuristic criterion.
if l is a literal, l stands for A if l = :A, and for A if l = :A;
for any literal l and formula ', assign(l; ') is the formula obtained
from ' by (i) deleting the clauses in which l occurs as a disjunct,
and (ii) eliminating l from the others.
As can be observed, the procedure Lsat dp in Figure 3 is the DP-
procedure modulo the call to Lconsist() when it nds an assignment
satisfying the input formula. Notice that in this procedure the pure
literal rule, used by some DP implementations, is not implemented.
In fact, our main interest is in correct and complete modal deciders.
With the pure literal rule, the set of assignments checked by Lconsist
|assuming that each of such call returns False| is not ensured to be
complete. 4
3 Let  be an assignment in a language L. Let L 0  L be a language. The
restriction of  to L 0 is the assignment obtained from  by deleting the conjuncts
not in L 0 . Let  0 an assignment.  0 extends  if each conjunct of  is also a conjunct
of  0 .
4 According to some authors (see, e.g., Freeman (1995)) the pure literal rule only
helps for a few classes of SAT problems. Furthermore, when this rule does help, it
does not result in a substantial reduction in search tree size.
SAT-Based Decision Procedures for Classical Modal Logics 11
In the following, for any formula ' and for any assignment  in
the (possibly extended) language of cnf('),  ' is the restriction of
to the language of '. Analogously, for any set of assignments ,
g.
PROPOSITION 5. Let ' be any modal formula. Assume that, for
any assignment , Lconsist() prints  and returns False. Let be
the set of assignments printed as the result of invoking Lsat('). The
disjunction of the assignments in ' is propositionally equivalent to '.
Proof: In the hypotheses of the Proposition, what we need to prove is
that
_
First, it is clear that cnf(')
2 . For the thesis, the right-to-left
implication is an easy consequence of the rst of the two properties of
cnf('). Assume that the left-to-right implication is false. This means
that there exists an assignment  in the language of ' such that
(1) for any propositional atom A, either A or :A is a conjunct of ,
(2) for any formula 2 in the language of ', either 2 or :2 is a
conjunct of ,
(3)  satises ', and
does not satisfy
.
Given (3) and the second of the properties of cnf('), there must exist
an assignment  0 in the language of cnf(') which
extends ,
thus also
.
means that  0 entails
2  by propositional reasoning. Thus,
there must exist an assignment  00 in such that |given (1), (2), (5)|
each conjunct of  00
' is also a conjunct of  0
' and thus of . This implies
that  entails  00
' . Since  00
, contradicting (4).
We can now state and prove soundness and completeness results for
our procedures.
Theorem [Soundness and Completeness] Let L be one of the logics
E, EM, EN, EMN, EC, ECN, EMC, EMCN. Lsat is sound and
12 E. Giunchiglia, F. Giunchiglia and A. Tacchella
complete for L, i.e., for any modal formula ', Lsat(') returns True if
' is L-consistent, and False otherwise.
Proof: First observe that Lsat(') returns
True if there exists a call to Lconsist() which returns True, and
False if each call to Lconsist() returns False.
The proof is by induction on the depth d of '. If 0 the Theorem
is trivial. Assume that 1. By induction hypothesis, for any
formula whose depth is less than d, Lsat( ) returns True if is L-
consistent, and False otherwise. In the following, we use the following
two facts:
(1) For any two assignments  and  0 diering only for propositional
conjuncts,  is L-consistent i  0 is L-consistent.
This is a trivial consequence of Proposition 1 and Proposition 3.
(2) Let  be an assignment such that Lconsist() is invoked during
the execution of Lsat('). Lconsist() returns True if  is L-
consistent and False otherwise.
Given that the depth of  is less than or equal to d, this is a
consequence of the the induction hypothesis, Proposition 2 and
Proposition 4.
There are two cases:
1. ' is L-consistent. From Proposition 5, it follows that there exists a
call to Lconsist() in which the assignment  (i) satises cnf('),
and (ii) is such that  ' is L-consistent. Since  possibly extends  '
in that it may assign some newly introduced propositional variables,
from (1) it follows that  is L-consistent, and from (2) it follows
that Lconsist() |and thus also Lsat(')| returns True.
2. ' is not L-consistent. From Proposition 5, it follows that for each
call Lconsist(), the assignment  ' is not L-consistent. As above,
from (1) it follows that  is not L-consistent, and from (2) it follows
that Lconsist() returns False.
4. *sat
*sat is built on top of sato ver. 3.2 (Zhang, 1997). The choice of
adopting sato as the basis for our system has been driven by the
following motivations:
SAT-Based Decision Procedures for Classical Modal Logics 13
sato is fast. We have not performed and are not aware of any
up-to-date extensive comparison among the dierent SAT solvers
publicly available. 5 However, according to some experiments we
have done and to the results presented in (Zhang, 1997), sato
seems to behave better than most of the currently available SAT
solvers.
sato has many options, including various splitting heuristics and
backjumping. We have inherited some of these options, and they
are available for experimentation.
sato has been written using some Software Engineering conventions
which have made and will make much easier to tune it for
our goals.
Besides the options inherited from sato, our system allows for other
possibilities that we have developed while implementing the system.
It is out of the goals of this paper to describe *sat structure, optimizations
and congurable options. For a more detailed presentation,
see (Tacchella, 1999) and the manual distributed with *sat. For our
goals, it suces to say that the core of *sat is a C implementation of
the procedures Lsat and Lconsist in Figures 1, 2, 3. In particular,
with reference to Figure 3, in *sat
cnf(') is the set of clauses obtained from ' by applying a conversion
based on renaming, such as those described in (Tseitin,
1970; Plaisted and Greenbaum, 1986).
choose-literal('; ) returns a literal according to a MOMS heuristic
(Maximum Occurrences in clauses of Minimum Size) (Freeman,
1995).
assign(l; ') is a highly optimized procedure which takes time linear
in the number of occurrences of l in '.
*sat also implements two important optimizations which have been
used in the tests presented in the next Section:
Early-pruning. Before each splitting step in Lsat, the L-consistency of
the assignment generated so far is checked by a call to Lconsist.
As in KsatC, care is taken to avoid the repetition of L-consistency
checks on the same branch of the propositional search tree. 6 Early
for a list of publicly available SAT solvers and more.
6 This is obtained through a pointer in the assignment stack which keeps track
of the portion of the current assignment which has been already veried to be
L-consistent.
14 E. Giunchiglia, F. Giunchiglia and A. Tacchella
pruning has proved to be very eective at least on some of the
tests presented in the next Section (see (Giunchiglia et al., 1998)).
Caching for K. In the case of the logic K, *sat uses an additional data
structure which allows to associate to any formula ' the result of
Lsat('). Before invoking Lsat on a formula , Lconsist checks
whether the K-consistency of has already been determined. As in
caching introduces some additional costs, but it may produce
dramatic speedups (see (Horrocks and Patel-Schneider, 1999b)).
We have not yet conducted an exhaustive experimental analysis to
see, for each class of formulas, which combination of *sat options leads
to the best results (see (Horrocks and Patel-Schneider, 1999b) for a
similar study of Dlp options). In all the tests in the next Section, we
used *sat options which seemed more reasonable to us. In particular,
we have set *sat as to use
early pruning on all tests, and
caching (for K) when the depth of the input formula is greater
than 1.
5. A comparative analysis
The availability of decision procedures for the logics we consider varies
signicantly. For EMCN, that we recall is equivalent to K, there are
many implemented decision procedures available, see, e.g.,
et al., 1998; de Swart, 1998). For E, EM and EMC, Gasquet and
Herzig (1996) provide a reduction to normal modal logics: by implementing
this reduction we indirectly obtain decision procedures for
these logics. Fitting (1983) calls U the logic EM, and denes a tableau
system for it. More recently, Governatori and Luppi (1999) dene a
tableau-like proof system for classical, monotonic and regular modal
logics. We are not aware of any implementation of these tableau sys-
tems. For EN, EC, EMN and ECN we are not aware of any other
implemented decision procedure, nor of any reduction into a formalism
for which a decision procedure is available.
Our comparative analysis is restricted to K and E. In fact, both our
decision procedures for E and EM, and Gasquet and Herzig's reductions
for E and EM, are similar. We expect that the experimental analysis
for EM would lead to results similar to the ones we have for E. For
SAT-Based Decision Procedures for Classical Modal Logics 15
EMC, Gasquet and Herzig's reduction is to a normal modal logic for
which we do not have a system available. 7
5.1. Modal K
As we said, there are several systems able to solve the consistency
problem for K. In our comparative experimental analysis, we consider
the four systems *sat, KsatC (Giunchiglia et al., 1998), Dlp (Patel-
Schneider, 1998) and
among the fastest solvers for K. We remember that TA, given a modal
rst determines a corresponding rst order formula '  and
then it performs conventional rst-order theorem proving. In our tests,
as in (Hustadt and Schmidt, 1997a), uses Flotter to convert '
in a set of clauses Cl('  ), and then the theorem prover Spass to solve
Cl('  ). For a brief description of Flotter and Spass, see (Weidenbach
et al., 1996). 8
We test these systems on three problem sets of randomly generated
formulas. A 3CNFK formula is a conjunction of 3CNFK
clauses, each with three disjuncts. Each disjunct in a 3CNFK clause
is either a propositional literal or a formula having the form 2C or
:2C, where C is a 3CNFK clause. See (Giunchiglia and Sebastiani,
1996a) for a more detailed presentation. We only remark that for any
formula ' there exist a 3CNFK formula which is K-consistent i ' is
K-consistent.
Sets of 3CNFK formulas can be randomly generated according to
the following parameters:
(i) the modal depth d;
(ii) the number L of clauses at depth
7 The reduction maps the consistency problem for a formula ' in EMC, into the
consistency problem for a formula ' 0 in the smallest normal modal logic with two
modal operators 21 , 22 and augmented with the schema
See (Gasquet and Herzig, 1996) for more details.
8 The experimental results have been obtained with Dlp ver. 3.1,
ver. 1.4 (Spass/Flotter ver. 0.55), KsatC ver. 1.0, and *sat ver. 1.2.
To compile the systems we have used sml-nj 110.0.3, sicstus prolog
3, ACL 5.0, and gcc 2.7.2.3. The tests have been run on several Intel
PCs, whose conguration varies from P200MHz with 64MbRAM, up to a
PII350MHz with 256 MbRAM. All platforms are running Linux 5.x RedHat. Dlp
is available at http://www-db.research.bell-labs.com/user/pfps.
at http://www.doc.mmu.ac.uk/STAFF/U.Hustadt/mdp. KsatC is available at
ftp://ftp.mrg.dist.unige.it/ in pub/mrg-systems. *sat is available at the WEB
page http://www.mrg.dist.unige.it/~tac/StarSAT.html.
A. Tacchella
(iii) the number N of propositional variables;
(iv) the probability p with which a disjunct occurring in a clause at
depth < d is purely propositional.
Care is taken in order to avoid multiple occurrences of a formula in a
clause, at the same time ensuring that the modal vs. the propositional
structure of each generated formula only depends on p. In more detail,
a clause is generated by randomly generating its disjuncts. When generating
a disjunct, we rst decide whether it has to be a propositional
literal or not. Then a disjunct of the proper type is repeatedly generated
as long as it does not occur in the clause generated so far.
In the tests we consider, a problem set is characterized by N and
p: d is xed to 1, while L is varied in such a way to empirically cover
the \100% satisable { 100% unsatisable" transition. For each pair
in a problem set, 100 3CNFK formulas are randomly generated,
and the resulting formulas are given in input to the procedure under
test. Then, for each run, we consider the time the systems take for
the main processing of the formula, thus excluding the negligible time
the systems take to read and somehow normalize the input formula.
(In particular, for this means that we take into account only the
time needed by Spass to solve the formula generated at the end of
the translation process.) For practical reasons, a timeout mechanism
stops the execution of the system on a formula after 1000 seconds of
CPU time. Even more, for any pair N; p, the execution of *sat, KsatC
and stopped after the system exceeds the timeout on 51 of the
100 samples corresponding to the xed N; p. Dlp instead, stops its
execution on the 100 samples corresponding to a pair N; p if a supermajority
of the rst n tests timeout. 9 When this happens, it is assumed
that Dlp exceeds the timeout for more than 50% of the tests with that
The rst three problem sets we consider have
xed to 0%: according to Hustadt and Schmidt (1997b), xing
corresponds to particularly dicult tests. We call these problem sets
PKN4p0, PKN5p0, and PKN6p0 respectively. PKN4p0 and PKN6p0
are called PS12 and PS13 respectively in (Hustadt and Schmidt, 1997b).
In order to better highlight the behavior of *sat and KsatC, we also
run these systems on a problem set (called PKN7p0) having
In Figure 4, satisability percentages and the median of
the CPU times for the four systems are plotted against the number
9 In more detail, Dlp stops its execution if there are at least 5 tests so far and
more than 90% of them timeout, or if there are at least 10 tests so far and more
than 75% of them timeout, or if there are at least 20 tests so far and more than 55%
of them timeout (Patel-Schneider, 1999).
SAT-Based Decision Procedures for Classical Modal Logics 17
Systems comparison - N=4, d=1, %p=0
CPU
KsatC
Systems comparison - N=5, d=1, %p=0
CPU
KsatC
Systems comparison - N=6, d=1, %p=0
CPU
KsatC
Systems comparison - N=7, d=1, %p=0
CPU
KsatC

Figure

4. Logic K. *sat, KsatC, Dlp, and 7.
samples/point. Background: satisability percentage.
of clauses L. Notice the logarithmic scale on the vertical axis, which
causes that values equal to 0:00 do not get plotted.
Consider Figure 4. The rst observation is that *sat and KsatC
are the fastest. The two systems perform roughly in the same way, with
*sat performing better when 5. For 7, the two systems
have similar performances, one system performing better than the other
for some values of L, but worse for other values of L. This comes at no
surprise: the two systems have the same underlying structure, both use
early pruning and a MOMS heuristic to select the splitting literal. The
two systems do not have an identical behavior because they use dierent
data-structures and implement slightly dierent MOMS strategies.
Considering the other systems, for PKN4p0 the gap between *sat/KsatC
and Dlp [resp. TA] is of more than one order of magnitude at the
cross-over point of 50% of satisable formulas, and goes up to almost
[resp. 4] orders of magnitude at the right end side of the horizontal
axis. For PKN5p0 and PKN6p0, values exceed the timeout
for respectively, while the corresponding values of
A. Tacchella
*sat [resp. KsatC] are 1.22 [resp. 1.83] and 3.32 [resp. 5.64] seconds.
keeps exceeding the timeout for all the successive values. The gap
between *sat/KsatC and Dlp on PKN5p0 is of more than one order
of magnitude at the cross-over points of 50% satisable formula, and
goes up to almost 3 orders at the very right of the plot. When
Dlp median values exceed the timeout for
does not terminate gracefully. 10 Comparing *sat and
Dlp on PKN4p0 and PKN5p0, we see that
the gap between *sat and Dlp seems to increase with L. Both for
PKN4p0 and PKN5p0, the dierence in logarithmic scale between
*sat and Dlp is (almost always) monotonically increasing.
At the crossover point of 50% satisable formulas, the gap between
*sat and Dlp [resp. TA] is roughly 1s [resp. 60s] for PKN4p0; and
220s [resp. 1000s] for PKN5p0.
Such good performances by *sat and KsatC are due to early pruning,
which has revealed to be very eective on these problem sets. For
example, if we disable early pruning in *sat and rerun it on PKN5p0,
the system keeps exceeding the time limit for
When the better behavior of *sat and KsatC than Dlp
and TA, is conrmed by the Q%-percentile graphs in Figure 5, corresponding
to 4. Formally, the Q%-percentile of a set S of values is
the value V such that Q% of the values in S are smaller or equal to
. The median value of a set thus corresponds to the 50% percentile
of the set. Figure 5 reports the 50%, 60%, 70%, 80%, 90% and 100%
percentile values of the CPU-times when *sat (top left), KsatC (top
right), Dlp (bottom left) and (bottom right) are run on PKN4p0.
The percentile plots for PKN5p0 and PKN6p0 look similar to the plots
in

Figure

5. This means that all the systems perform in roughly the
same way on the 50 most dicult samples of the 100 tests corresponding
to a xed N and L.
We also run the four systems on problems with
p is xed to 50%. We call these problem sets PKN4p50, PKN5p50,
PKN6p50, and PKN7p50. In Figure 6 the satisability percentages and
the median of the CPU times for the four systems are plotted against
the number of clauses L. As for
roughly in the same way and are the fastest. Dierently from the tests
in which 0%, at the transition point of 50% of satisable formulas,
the gap between *sat/KsatC and Dlp seems to diminish when the
number of variables increases. Horrocks and Patel-Schneider (1999a)
ver. 3.2 is able to successfully handle formulas with
SAT-Based Decision Procedures for Classical Modal Logics 19206010050709010 -2
percentiles
CPU
KsatC CPU TIME - N=4, d=1, %p=0
percentiles
CPU
percentiles
CPU
percentiles
CPU

Figure

5. Logic K. 50%{100% percentile CPU times of *sat, KsatC, Dlp, and TA.
samples/point.
show that for values of L bigger than 7, Dlp performances are superior
to those of KsatC when
that Dlp performs better than KsatC when p is high and worse
when p is low. We have not yet done such a broad comparison using
*sat instead of KsatC. However, we believe that Horrocks and Patel-
Schneider's conclusions should extend also to *sat, if *sat is used with
the parameter settings we have currently used, i.e., those which make
*sat most similar to KsatC. Of course, a big role can be played by
*sat already available congurable options, and this will be the issue
of future research. In any case, both *sat and KsatC perform better
than the other systems for large values of L, when the formulas are
trivially unsatisable. This is due to the fact that for large values of
L, formulas become propositionally unsatisable, and thus both *sat
and KsatC mostly take advantage of their SAT-based nature, e.g., of
their optimized data structures for handling large formulas.
As for the percentile plots of the timings of the systems
on PKN7p50, do not show big dierences with respect to the plots of
20 E. Giunchiglia, F. Giunchiglia and A. Tacchella
Systems comparison - N=4, d=1, %p=50
CPU
KsatC
Systems comparison - N=5, d=1, %p=50
CPU
KsatC
Systems comparison - N=6, d=1, %p=50
CPU
KsatC
Systems comparison - N=7, d=1, %p=50
CPU
KsatC

Figure

6. Logic K. *sat, KsatC, Dlp, and 7.
samples/point. Background: satisability percentage.
the medians. Considering Dlp and *sat 100% percentile plots, it is
interesting to observe that Dlp has a lower maximum than *sat; on
the other hand, *sat values decrease more rapidly than those of Dlp.
Finally, we see that for most of the problem sets we consider, all the
systems seem to have an easy-hard-easy pattern, whose peak roughly
correspond to the 50% of satisable formulas. When
phenomenon is best evident for *sat and KsatC.
We also consider the benchmarks formulas for K used at the Comparison
of Theorem Provers for Modal Logics at Tableaux'98 (see (de
Swart, 1998)). These consist of nine provable parameterized formulas
(ending with \ p") and nine unprovable parameterized formulas
(ending with \ n"). For each parameterized formula A(n), the test
consists in determining the greatest natural number n  21 satisfying
the following two conditions:
1. the prover returns the correct result for the formulas A(1);
in less than 100 seconds, and
SAT-Based Decision Procedures for Classical Modal Logics 21
percentiles
CPU
KsatC CPU TIME - N=7, d=1, %p=50
percentiles
CPU
percentiles
CPU
percentiles
CPU

Figure

7. Logic K. 50%{100% percentile CPU times of *sat, KsatC, Dlp, and TA.
samples/point.
2. the prover cannot do the formula A(n+ 1) in less than 100 seconds
or
Even though it has been proved that most of these tests can be easily
solved by current solvers, these are still interesting because
they are not 3CNFK formulas, and
some of these tests have not been solved yet.
The results for *sat, and Dlp are reported in Table I. KsatC has
not been tested since KsatC is able to deal with 3CNFK formulas only.
We also show the CPU time requested by the system to solve the last
instance A(n). Notice that *sat has been run with caching enabled,
since the depth of all the formulas in the Table is greater than 1. For
TA, we do not take into account the time needed to compute the rst
corresponding to A(n) (which is negligible), but we
do take into account the time requested by Flotter to convert A  (n)
22 E. Giunchiglia, F. Giunchiglia and A. Tacchella

Table

I. Logic K. *sat, Dlp and performances on Tableaux'98 benchmarks
*sat Dlp
Test Size Time Size Time Size Spass Flotter
branch p 21 0.21
lin n 21 47.80 21 0.70 21 16.07 63.94
lin
path n 21 0.96
path p 21 0.72
ph n 12 0.60 9 40.16 9 45.21 9.92
ph p 8 48.54 6 11.34 6 42.19 0.97
poly n 21 2.25
poly p 21 1.73
into a set Cl(A  (n)) of clauses (reported in the Flotter column), and
the time requested by Spass to determine the consistency or inconsistency
of (reported in the Spass column). Furthermore, we
stopped on A(n) with n < 21, either because Flotter does not
terminate gracefully when computing
or Flotter exceed the 100 seconds time limit. In the table, these three
cases correspond to the rows in which the value for n/Spass/Flotter
respectively is underlined.
As can be observed from Table I, the three systems are able to solve
all the instances of a formula in four cases. *sat and Dlp are able
to solve all the instances except for k branch n, k branch p, k ph n,
ph p. Except for the rst of these four parameterized formulas, *sat
is able to solve more instances than Dlp. For k branch n, both *sat
and Dlp are able to solve the 12th instance, with Dlp taking less time
than *sat to solve it.
SAT-Based Decision Procedures for Classical Modal Logics 23
5.2. Modal E
Gasquet and Herzig (1996) provide a translation which maps any formula
' into a formula 'GH in K 2 , i.e., the smallest normal modal logic
with two modal . The translation is such that ' is
satisable in E i 'GH is satisable in K 2 . This translation is dened
in the following way:
is a propositional variable,
and homomorphic for the cases of the propositional connectives.
Consider a formula '. We compare *sat performances on ' with
respect to *sat, Dlp and performances on 'GH . We could not
run KsatC on 'GH , since KsatC accepts only 3CNFK formulas with
at most one modality. To make evident when a system is run using
Gasquet and Herzig's translation, we append the string \+GH" to
the name of the system. Therefore, in the following, we will have the
systems *sat, *sat+GH, Dlp+GH, and TA+GH.
In E, the 3CNFK test methodology is not suited. Indeed, it is no
longer the case that for any modal formula ' there exists a 3CNFK
formula which is E-satisable i ' is E-satisable. Furthermore, checking
the consistency of an assignment  in E amounts to determine the
consistency of (  :) for each pair of conjuncts 2 and :2 in :
most of these tests, in case  and  are 3CNFK clauses, can be trivially
We therefore consider sets of 3CNFE formulas. A 3CNFE formula
is a conjunction of 3CNFE clauses, each with three disjuncts. Each
disjunct in a 3CNFE clause is either a propositional literal or a formula
having the form 2C or :2C, where C is a 3CNFE formula. For
example,
where each l i (1  i  8) is a propositional literal, is a 3CNFE formula.
For any formula ', there exist a 3CNFE formula logically equivalent
to ' in E.
Sets of 3CNFE formulas can be randomly generated according to the
parameters used to generate 3CNFK formulas, and a new parameter C
representing the number of clauses at depth d > 0. A 3CNFK is thus
a 3CNFE formula in which C = 1. As in the previous subsection, a
problem set is characterized by N and p: d and C are xed to 1 and L
respectively; L is given increasing values in such a way to empirically
cover the \100% satisable { 100% unsatisable" transition. We also
A. Tacchella
Systems comparison - N=4, d=1, %p=0
CPU
TA+GH
Systems comparison - N=5, d=1, %p=0
CPU
Systems comparison - N=6, d=1, %p=0
CPU
Systems comparison - N=7, d=1, %p=0
CPU
TA+GH

Figure

8. Logic E. *sat, *sat+GH, Dlp+GH, and TA+GH median CPU time.
samples/point. Background: satisability percentage.
check that in each sample there are no multiple occurrences of a formula
in a clause, at the same ensuring that the propositional vs. the
modal structure of the formula only depends on p. Notice that while
increasing L also C is increased. As a consequence, for each pair of
in an assignment satisfying a 3CNFE formula,
the recursive E-consistency check for ( has itself a phase
transition from 100% satisable to 100% unsatisable when increasing
L. Overall, for low [resp. high] values of L we expect that each satisfying
assignment should be trivially determined to be E-consistent [resp. not
E-consistent].
As before, for each value N in a problem set, 100 3CNFE formulas
are randomly generated, and the resulting formulas are given in input to
the procedure under test. A timeout stops the execution of the system
on a formula after 1000 seconds of CPU time. We consider the following
problems sets:
SAT-Based Decision Procedures for Classical Modal Logics 25
percentiles
CPU
percentiles
CPU
percentiles
CPU
percentiles

Figure

9. Logic E. 50%{100% percentile CPU times of *sat, *sat+GH, Dlp+GH,
and TA+GH. samples/point.
PEN4p0, PEN5p0, PEN6p0, PEN7p0 in which
respectively, and
PEN4p50, PEN5p50, PEN6p50, PEN7p50 in which
Given the huge amount of time that Flotter takes to prepare the
formula for Spass, we run TA+GH only on the problems sets PEN4p0
and PEN4p50. For PEN7p0 and PEN7p50, we run TA+GH only on the
initial points. As in the preceding subsection, we only take into account
the time the systems take for the main processing of the formula. In
particular, for each system, we do not take into account the time needed
to perform the Gasquet and Herzig's conversion; and for TA+GH we
take into account only the time taken by Spass. The median and the
percentile plots of the systems on PEN4p0, PEN5p0, PEN6p0, PEN7p0
are shown in Figure 8 and Figure 9 respectively.
Consider Figure 8. As can be observed, *sat is the fastest: the gap
with the other systems is of more than one order of magnitude for
26 E. Giunchiglia, F. Giunchiglia and A. Tacchella
Systems comparison - N=4, d=1, %p=50
CPU
TA+GH
Systems comparison - N=5, d=1, %p=50
CPU
Systems comparison - N=6, d=1, %p=50
CPU
Systems comparison - N=7, d=1, %p=50
CPU

Figure

10. Logic E. *sat, *sat+GH, Dlp+GH, and TA+GH median CPU time.
samples/point. Background: satisability percentage.
certain values of L. However, both *sat+GH and Dlp+GH perform
quite well, better than one could have imagined given that the consistency
problem for E and K 2 belongs to two dierent complexity classes.
However, a closer look to Gasquet and Herzig's reduction reveals that,
considering a 3CNFE formula ', and an assignment
(as usual we assume that
is a propositional formula)
in the language of ',
1.  satises ' i GH satises 'GH .
2. for checking the E-consistency of , *sat performs at most 2mn
consistency checks involving the formulas
3. for checking the K 2 -consistency of GH , both *sat+GH and Dlp+GH
perform at most 2mn consistency checks involving the formulas
SAT-Based Decision Procedures for Classical Modal Logics 27
percentiles
CPU
percentiles
CPU
percentiles
CPU
percentiles
CPU

Figure

11. Logic E. 50%{100% percentile CPU times of *sat, *sat+GH, Dlp+GH,
and TA+GH. samples/point.
The rst two points are obvious. To understand the last, it suces to
notice that GH is propositionally equivalent to
Given that both *sat+GH and Dlp+GH use caching, these procedures
will perform at most a quadratic number of checks in the number of
subformulas of 'GH . This is not the case for TA+GH, since Spass does
not have any caching mechanism. This explains the good behavior of
*sat+GH and Dlp+GH, and the bad behavior of TA+GH.
It is interesting to compare *sat+GH and Dlp+GH performances.
As can be observed, Dlp+GH performs better than *sat+GH for low
values of L, but worse for high values of L. This behavior re
ects
the dierent mechanisms used by *sat+GH and Dlp+GH to prune
the search space when checking the K-consistency of an assignment.
As we said in Section 4, in all the tests we have set *sat+GH as to
28 E. Giunchiglia, F. Giunchiglia and A. Tacchella
use the early pruning strategy. Dlp+GH instead implements a backjumping
schema in the spirit of (Baker, 1995): when an assignment is
discovered to be not K-consistent, backtracking to a point which does
not lead to the same contradiction is enforced. While implementing
early pruning does not introduce overheads, this is not the case for
backjumping, where a dependency set of each derived clause has to be
maintained (see (Patel-Schneider, 1998) for more details). Despite the
additional costs introduced, backjumping clearly wins if compared to
early pruning in logic K, for low values of L. In this case, almost each
assignment is K-consistent and early pruning may cause additional (i.e.,
not performed by a backjumping strategy) checks. On the other hand,
for high values of L, when the formula under test is not K-consistent but
there are still assignments satisfying it, *sat+GH is able to greatly cut
the search by checking the inconsistency of the assignment generated
so far. Dlp+GH instead checks the consistency of an assignment only
when it satises the current formula. Dlp+GH may therefore generate
many assignments which, even though they satisfy the input formula,
are not K-consistent. When L is so high that the input formulas become
propositionally unsatisable, *sat+GH may still perform additional
K-consistency checks, but these get compensated by (i) *sat+GH
SAT-based nature and (ii) the costs Dlp+GH has because of back-
jumping. Considering Figure 9, we see that Dlp+GH has a better
behavior than the other systems on some of the hardest instances.
Evidently, on these tests, backjumping leads to a more uniform behavior
than early pruning. Horrocks and Patel-Schneider (1999a) show that
for some randomly generate 3CNFK formulas, early pruning leads to a
more uniform behavior than backjumping.
For
TA+GH median and percentile times are plotted in Figure 10 and

Figure

respectively. As it can be observed, the situation is very
similar to the case in which 0%. The only dierence is that
now *sat+GH performs better than Dlp+GH for a lower value of L.
This is reasonable, since for each L, the number of consistency checks
performed by *sat+GH because of early pruning, diminishes when p
increases.
Finally, notice the easy-hard-easy pattern of *sat. To better appreciate
it, Figure 12 shows the number of calls to Lsat done by Lconsist
on PEN4p0-PEN7p0 (left), PEN4p50-PEN7p50 (right) against the ratio
between L and N . As can be observed, *sat performs a number of
Lsat calls whose maximum roughly correspond to the 50% of satisable
formulas. This transition happens when L
N is close to 5 for
to 6 for This behavior re
ects the above stated intuition
SAT-Based Decision Procedures for Classical Modal Logics 29
checks d=1 %p=0
OF
CHECKS
7 variables
6 variables
5 variables
4 variables
Consistency checks d=1 %p=50
OF
CHECKS
7 variables
6 variables
5 variables
4 variables

Figure

12. Logic E. *sat median number of calls to Lsat. 7.
samples/point. Background: satisability
percentages.
according to which for low [resp. high] values of L all the formulas
should be easily determined to be E-consistent [resp. not E-consistent].
6. Conclusions and future work
We have presented a set of SAT-based decision procedures for eight
classical modal logics. We have shown how the SAT-based approach
allows for ecient and modular implementations for these logics. We
have presented *sat. *sat is the only system that is able to deal with
EN, EC, ECN and EMN. In the case of the logic E, we have dened
a testing methodology which generalizes the 3CNFK methodology by
Giunchiglia and Sebastiani (1996a), and which is suitable for testing
systems for non-normal modal logics. The experimental evaluation
shows that *sat performances are superior to or comparable to the
performances of other state-of-the-art systems.
In the future, we plan to conduct an extensive experimental analysis
(similar to that presented in (Horrocks and Patel-Schneider, 1998; Horrocks
and Patel-Schneider, 1999b)) to understand, for each class of
formulas, which combination of *sat options leads to the best results.
We also plan to extend *sat in order to handle more expressive decidable
logics. We will also consider logics, like S4, for which more
sophisticated methods than that described in Section 4 have to be
employed in order to ensure the termination of the decision procedure.
A. Tacchella

Acknowledgments

We are grateful to Hullrich Hustadt, Peter F. Patel-Schneider, and
Hantao Zhang for the assistance they provided on their systems. Special
thanks to Roberto Sebastiani for the many useful discussions related
to the subject of this paper. Thanks also to the anonymous reviewers
for their helpful comments and suggestions. The rst and last authors
are partially supported by the Italian Spatial Agency.



--R


Intelligent backtracking on the hardest constraint problems.
An algorithm to evaluate quanti
Modal Logic - an Introduction
A computing procedure for quanti

Swart, editor. Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux'98
Reasoning about knowledge.
Proof Methods for Modal and Intuitionistic Logics.

Improvements to propositional satis
PhD thesis
From classical to normal modal logics.
Ideal and Real Belief about Belief.
Building decision procedures for modal logics from propositional decision procedures - the case study of modal

of the 5th International Conference on Principles of Knowledge Representation and Reasoning - KR'96
More evaluation of decision procedures for modal logics.
Labelled tableaux for non-normal modal logics
Comparing subsumption optimizations.
Advances in propositional modal
Optimising description logic subsumption.
Journal of Logic and Computation
Using an expressive description logic: FaCT or
On evaluating decision procedures for modal logic.
On evaluating decision procedures for modal logic.
BLACKBOX: A new approach to the application of theorem proving to problem solving.
Strongly analytic tableaux for normal modal logics.

Translation methods for non-classical logics - an overview
DLP system description.
Personal communication
A Structure-preserving Clause Form Translation
Journal of Symbolic Computation
From Tableau-based to SAT-based procedures - preliminary report
An Essay in Classical Modal Logic.



On the complexity of proofs in propositional logics.
Correspondence theory.
On the complexity of epistemic reasoning.


--TR

--CTR
Andrei Voronkov, How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi, ACM Transactions on Computational Logic (TOCL), v.2 n.2, p.182-215, April 2001
Enrico Giunchiglia , Armando Tacchella, A Subset-Matching Size-Bounded Cache for Testing Satisfiability in Modal Logics, Annals of Mathematics and Artificial Intelligence, v.33 n.1, p.39-67, September 2001
SAT-based planning in complex domains: concurrency, constraints and nondeterminism, Artificial Intelligence, v.147 n.1-2, p.85-117, July
Enrico Giunchiglia , Yuliya Lierler , Marco Maratea, Answer Set Programming Based on Propositional Satisfiability, Journal of Automated Reasoning, v.36 n.4, p.345-377, April     2006
Alessandro Armando , Claudio Castellini , Enrico Giunchiglia , Marco Maratea, The SAT-based Approach to Separation Logic, Journal of Automated Reasoning, v.35 n.1-3, p.237-263, October   2005
Franz Baader , Diego Calvanese , Deborah L. McGuinness , Daniele Nardi , Peter F. Patel-Schneider, Bibliography, The description logic handbook: theory, implementation, and applications, Cambridge University Press, New York, NY,
modal logic;SAT-based decision procedure