A Benchmark for Knowledge Compilation

This page is a first attempt at building up a benchmark for evaluating different knowledge compilation (KC) methods. So far, this is a joint work by

• P. Marquis, B.Mazure, L. Sais (CRIL)
• P. Mathieu, O. Roussel (LIFL)

In a few words, a knowledge compilation method is a technique which improves the behaviour of an inference method by preprocessing the knowledge base. Today, there exist several knowledge compilation methods

• Vivification (Dalal)
• FPI0,FPI1,FPI2 (del Val)
• KC using Horn approximations (Kautz and Selman, del Val)
• KC using theory prime implicates (Marquis)
• KC using theory prime implicants (Mazure and Marquis)
• KC for forward chaining (Mathieu and Roussel)
• KC using implicants (Schrag)

Each method has its strengthes and weaknesses. Furthermore, the different inference algorithms addressed by these methods make it difficult to establish a benchmark for comparing them objectively. For example, Schrag's KC method is more suitable when the base has few implicants while other methods are more suitable when the base has many implicants.

However, there's a number of points which are likely to meet everyone's agreement

• interesting bases must have several models, and more precisely more than a few ones. Therefore, unsatisfiable bases are of no interest.
• interesting bases must be neither too easy nor too hard to reason with. If the base is too easy, direct inference methods will be very efficient and KC method won't prove useful. On the other hand, if the base is too hard (that is direct inference methods are unable to give an answer within a reasonable amount of time), no KC method is likely to complete the compilation of such a base.

To assess the hardness of a base, it's been decided to evaluate the number of nodes explored by a SAT algorithm and to compare it to the number of possible interpretations. If the SAT algorithm explores few nodes, direct inference methods are likely to be efficient and therefore, the base is believed to be easy.

To evaluate the performances of a KC method, we will compare the inference speed using a direct inference method or a KC method. The direct inference method will be based on a SAT test. Several quantities will be measured:

• n : number of inferences in the test
• Tsat : time needed for performing the n inferences on the initial base using a SAT test
• Tkc : time needed for performing the n inferences using the compiled knowledge base
• Tcomp : time needed to compile the base

From these figures, we can compute

• S=Tsat/Tkc : mean speedup obtained using KC
• B=n.Tcomp/(Tsat-Tkc) : break even point ; this is the mean number of inferences to perform to amortise the compilation cost

Of course, these figures heavily depend on the efficiency of the chosen SAT test. However, it's difficult to choose a suitable SAT test for our experiments. Choosing the fastest SAT is not satisfactory since a) this efficiency may come in part from some tricks in the implementation b) the sources of the program may be unavailable or impossible to reuse. For these reasons, it was decided to use a SAT test reasonably fast and simple. This test has been implemented in C language by B.Mazure. You can download its source code.

The DIMACS format has been adopted to represent the bases. This choice results from the ease with which this format can be parsed. However, one of its drawbacks is that it is more adapted to random bases than to bases with a clear semantics. For such bases, we have decided to store the base in the DIMACS format as well as in its original format.

For each base, we detail

• its name. When the base is an instance of a general family of bases, the parameters used to produce this instance are appended to the base name and separated by dashes.
• a pointer to more information on the base (when available)
• its number of variables
• its number of clauses
• the number of nodes developed by the SAT test to prove satisfiability
• the number of unit literal propagations performed during this test
• the time in seconds required for this test (measured on a Sun UltraSparc-1 workstation)