Navarro-Pérez, JA; Voronkov, A; (2007) Encodings of problems in effectively propositional logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , 4501 LNCS 3 - 3.
Full text not available from this repository.
Solving various combinatorial problems by their translation to the propositional satisfiability problem has become commonly accepted. By optimising such translations and using efficient SAT solvers one can often solve hard problems in various domains, such as formal verification and planning. This approach to solving combinatorial problems is usually implemented by a translation procedure turning a formal description of the problem written in a domain-specific language L (for example, SMV for model checking problems  or STRIPS  for planning problems) into a SAT problem. Such translation procedures share the following common features: 1. They contain many isomorphic or nearly isomorphic subsets of clauses obtained by the translation of the same expression of L. 2. The size of the resulting SAT problem is dominated by these copies. In this talk the second author will present encodings able to specify some combinatorial problems, namely LTL bounded model checking  and planning within the Bernays-Schönfinkel fragment of first-order logic. This fragment, which also corresponds to the category of effectively propositional problems (EPR) of the CASC system competitions , allows a natural and succinct representation of both the transition systems corresponding to the problems and the property that one wants to verify, while avoiding the problem of creating isomorphic copies. Our technique provides a rich collection of benchmarks with close links to real-life applications for the automated reasoning community and may boost development of new translation techniques and solvers for effectively propositional problems. © Springer-Verlag Berlin Heidelberg 2007.
|Title:||Encodings of problems in effectively propositional logic|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science > Computer Science|
Archive Staff Only: edit this record