Experiments on ASSAT 1.3

We have experimented with ASSAT on a variety of benchmark domains and compared its performance with smodels and dlv.

The systems tested are as follows: For specialized answer set generators: Smodels version 2.27 and dlv (Jun 11, 2001 version); for ASSAT, we tried the following SAT solvers: Chaff2 (Mar 23, 2001 version), walksat 3.7, satz 2.13, satz-rand 4.7, and sato.

The following are some pointers to our experimental data on the blocks world planning domain, the graph coloring domain, and the Hamiltonian Circuit domain, all using the logic program encodings by Niemela for these problems.

All experiments were done on Sun Ultra 5 machines with 256M memory running Solaris. The reported times are in CPU seconds as reported by Unix ''time'' command, and include, for smodels the time for grounding, and for ASSAT the time for grounding, computing program completions, and checking that the returned assignment is indeed an answer set. We use 2 hours as the cut off limit. So if an entry is marked by ''---'', it means that the system in question did not return after it had used up 2 hours of the CPU time.

The Block's World Planning Domain 

The Graph Coloring Domain 

The Hamiltonian Circuit Domain 

Yuting Zhao
Last modified: Thursday December 5 2002