Compile! Project - CRIL-CNRS & Univ. Artois

pddl2cnf: translating PDDL instances into CNF formulae

pddl2cnf is a translator associating with a classical planning instance encoded in PDDL (Planning Domain Definition Language) and a given horizon an output which consists of a CNF formula. The valid plans for the input planning instance correspond to the models of the corresponding output CNF formula, projected onto the action variables.

Ressources for the pddl2cnf translator

• the runtime code of pddl2cnf GNU/Linux operating system

How to use pddl2cnf

Given a PDDL instance, represented by a domain file d.pddl, a problem file p.pddl, and a horizon (5 in the example developed below), pddl2cnf can be run as follows:

The translator generates two files:

• p_t5.cnf, the CNF file encoding the input instance for the specified horizon (5 on the example);
• p_t5.infos, a file containing some information for retrieving a valid plan from a model of the generated CNF formula.

p_t5.infos contains three lines. The first one begins by c i and gives the list of Boolean variables used for representing fluents. As soon as a new predicate is found in the domain file, the full set of corresponding fluents is built, given the number of objects the instance contains and the horizon. As an example, let us consider a block world instance with two blocks A and B, and a predicate on which applies to blocks. 24 (= 2 times 2 times 6) Boolean variables are used to encode the possible positions of the two objects w.r.t. the on predicate at the six possible time points: on(A,A,0), ..., on(A,A,5), on(A,B,1) and so on. Predicates are considered in the order they appear in the domain file, and objects are considered in the order they appear in the problem file. One can check the order w.r.t. which fluents are generated by consulting a log file (see below).

The second line of the information file makes precise the Boolean variables used to denote the goals. The third line indicates the Boolean variables used for encoding the actions. Again, some variables are introduced as soon as a new action is found in the domain file, and their order can be checked in the log file. This log file is generated by setting the -l flag to true.

Note that if you plan to compile the generated CNF using the C2D compiler, you can ask pddl2cnf to generate the variable file that will force the compiler to instantiate action variables using the -c flag.

Flag -d prevents from considering two or more occurrences of the same variable in predicates. Finally, it is possible to generate CNF outputs for every value of the horizon from 1 to a specified bound using the -a flag.