|
|
Experiments on ASSAT 2.0We 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.27DLV (May 16, 2003 version);for ASSAT, we tried the following SAT solvers:zchaff (Dec 4, 2003 version),mchaff (Chaff2) (Mar 23, 2001 version),Walksat 41,Satz 215.2,Sato 4.1.In most of the experiments, we use the logic program encodings by Niemela for these problems, for all of the three ASP solvers. Lparse 1.0.13 are used, for Smodels and ASSAT, to ground a logic program (DLV has its own built-in grounding routine). we also tested Smodels on 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 following are some pointers to our experimental data on the Block's World Planning Domain, the Graph Coloring Domain, and the Hamiltonian Circuit Domain. The Block's World Planning DomainThe Graph Coloring DomainThe Hamiltonian Circuit DomainThe Hamiltonian Circuit Domain (Comparison between different encodings) |