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.


Paper (pdf)


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"
}