thesis abstract (English)
Coopération entre démonstrateurs par tableaux et SAT
Troquard, Nicolas
Abstract:
Introduction and motivations
Knowledge representation and reasoning about it are some of the main
directions of research in Artificial Intelligence. The languages of
propositional and modal logics are easy-to-use concepts and are of
high power of expression at the same time. Moreover work within the
field, particularly recent work, has enabled efficient decision
algorithms to be developed. This is all the more true because in
recent years, highly optimised systems have been proposed to decide
the satisfiability of a formula in modal logic, based on propositional
reasoning. Those methods are called "SAT-based" and stem from two
insights. The first is that the reasoning in modal logic can be
implemented as an appropriate combination of propositional
reasonings. The second insight is that propositional reasoning can be
very effective, using the numerous and advanced propositional decision
procedures such as the Davis-Putnam algorithm, and progress in the
knowledge of the problem, such as phase transitions or heavy-tails...
Several convergent factors prompted this thesis. First, works of the
LILaC team of IRIT on formalisation of notions such as knowledge,
beliefs, intentions or interactions between agents, have led to the
development of complex modal logics, needing experimentations to be
validated. The study of automated demonstration procedures for modal
logics is a traditional concern in Artificial Intelligence. However
while provers of the state-of-the-art can only deal with a restricted
range of logics, the automated prover LoTREC which is being developed
by the LILaC team, try to be a generic tool.
It is largely interesting to apply the progress made in propositional
logic to automated deduction in modal logics. Nevertheless, the
integration of a SAT solver can negatively affect the flexibility of
LoTREC. Therefore, the intention is to take advantage of the progress
made in the SAT framework, in order to improve existing tableau-based
provers, and also to extend the use of a SAT prover within LoTREC, so
as to improve its performance without compromising its simplicity.
The satisfiability problem
One of the main parts of this project was to study the
state-of-the-art of the satisfiability problem. Indeed, the aim of
SAT-based methods is to take advantage of the wealth of knowledge on
the SAT problem to decide the satisfiability of a modal formula. In
fact, least progress in connection with SAT will also affect
drastically the effectiveness of the modal decision procedure.
We can characterize two classes of provers : the complete and
incomplete. A complete algorithm answers yes if and only if the input
formula is satisfiable. Incomplete provers, such as GSAT, are unable
to deal with inconsistency of a formula. GSAT is a local greedy search
on assignments of a set of propositional clauses. The procedure
chooses a random variables assignment, then flips the truth value of
the variable which allow to maximize the growth of the number of
satisfied clauses.
We can illustrate the complete provers with the well-known
Davis-Putnam algorithm (hereafter "DP"). In its basic form, it
consists of testing each possible variables assignment. A backtrack is
executed when an inconsistency is reached. Certain rules can be used
in order to reduce the search space (for example the unit clause rule
or the pure literal rule). DP is a very efficient method and the
source code of well-engineered implementations is available free to
charge.
SAT-based methods for system K
Fausto Giunchiglia and Roberto Sebastiani have introduced the KSAT
algorithm to decide the satisfiability of a modal formula in system K
[GS96]. The aim is to consider sub-formulae which can not be
propositionally reduced (a, []a, [](a v b)...) as a propositional
variables, and to use a complete procedure in order to find a
propositional model. Then we try to extend it to a K-model. It is
however important for the completeness of the algorithm to get a
complete set of propositional models, and DP (or any complete method)
can easily be adapted.
It is not obvious that the SAT-based methods are the most
efficient. Indeed, many papers have been published claiming the
superiority of SAT-based or translation-based methods. The problem is
to devise an experimental protocol and a class of instances that do
not give an advantage to one or other method. The reader is referred
to [GS96, GGST, HS97, GT02]. Nevertheless, SAT-based methods are
intrinsically better than tableau-based ones, as it has been formally
proved by R. Sebastiani and D. McAllester [SM97].
Moreover, SAT-based methods can be extended to more complex logics
such as description logics, normal or non-normal logics. In
particular, [SV98] contains a generalization to a set of normal
logics. It shows clearly that SAT-based methods can be seen as
Fitting's standard tableaux with factorized Smullyan rules in a SAT
decision procedure.
Our KSAT implementation : ProSaBa
We have decided to implement our own SAT-based prover. The reasons are
that LoTREC requires flexibility, and existing systems are tailored to
specific applications. On the other hand, we have reported a bug with
*SAT, the reference platform.
Since a prototype of a new version of LoTREC was developed in PROLOG,
our implementation ProSaBa (for PROlog SAt-BAsed) has been made in
PROLOG too. It is a very simple code (the whole source code is
presented in an annex to the thesis), and we have adapted it in order
to display models that have been found.
Prospects for the generic prover LoTREC
The main problem with LoTREC is that application of propositional
rules are completely ineffective, now experimentations especially
concern modal ones. Using SAT could improve LoTREC's application of
propositional rules without compromising versatility. The idea is that
SAT could be used as a heuristic in deciding a modal formula. With
such a method, we could use semantic rather than syntactic branching,
and so, which significantly reduces the number of applications of
propositional rules. LoTREC can take advantage of this reduction,
particularly when input instances are highly constrained.
However, we can imagine using KSAT as a heuristic for more complex
logics. For example, a formula will be S4-satisfiable only if it is
K-satisfiable. The interest lies in the fact that KSAT has a better
behaviour than standard tableaux in worst case.
Discussion
What we have explained in the last section has unfortunately not been
tested experimentally. For the moment, the architecture of LoTREC is
not flexible enough to allow such testing. When it is, we shall be
able to test cooperations LoTREC-SAT and LoTREC-ProSaBa.
One important thing is that the next version of LoTREC must provide a
SAT-engine which is easy to replace, in order to use the latest free
efficient provers.
References
[GS96] Fausto Giunchiglia and Roberto Sebastiani. Building decision
procedure for modal logics from propositional decision procedure - the
case study of modal K. In Conference on Automated Deduction, pages 583
- 597, 1996.
[GGST] E. Giunchiglia, F. Giunchiglia, R. Sebastiani, and
A. Tacchella. Sat vs. Translation based decision procedures for modal
logics : a comparative evaluation.
[HS97] Ullrich Hustadt and Renate A. Schmidt. On evaluating decision
procedures for modal logics. In IJCAI (1), pages 202-209, 1997.
[GT02] Enrico Giunchiglia, Armando Tacchella, and Fausto
Giunchiglia. Sat-based decision procedures for classical modal
logics. J. Autom. Reason., 28(2) :143-171, 2002.
[SM97] R. Sebastiani and D. McAllester. New upper bounds for
satisfiability in modal logics - the case study of modal k, 1997.
[SV98] Roberto Sebastiani and Adolfo Villafiorita. SAT-based decision
procedures for normal modal logics: a theoretical framework. In
Artificial Intelligence: Methodology, Systems, Applications -
AIMSA'98, number 1480 in LNAI. Springer Verlag, 1998.
Bibtex-entry:
@MastersThesis{Troquard04dea,
author = {Troquard, Nicolas},
title = {Coopération entre démonstrateurs par tableaux et SAT },
school = {Université Paul Sabatier},
year = 2004,
keywords = "tableaux, SAT, KSAT"
}