Benchmarking Results for nomore++

This page gives benchmark instances and detailed results for selected problems demonstrating the features of nomore++. We have tested nomore++ and smodels on the classes below:

On the problem of finding Hamilton circles, we show the advantages of nomore++'s support-driven strategy in comparison to smodels. Lookahead examples "Body-Plus" and "Head-Minus" illustrate the superiority of nomore++'s hybrid lookahead strategy to uniform approaches, i.e. using either only literals or bodies (respectively rules). Further benchmarks and results concerning dlv can be found on the Asparagus site.

The instances of the so called Body-Plus example are solved choice-point optimally by body-based and hybrid lookahead. The wrong choices made by smodels (which uses a literal-based lookahead) increase exponentially with the instance number, whereas nomore++ does not make wrong choices. Owed to the large number of answer sets, computing one answer set is recommended.

The instances of the so called Head-Minus example are solved choice-point optimally by literal-based and hybrid lookahead. Here, body-based (or rule-based, respectively) lookahead, implemented in noMoRe and available in nomore++, leads to expontially many wrong choices, whereas smodels and nomore++ with hybrid lookahead perform choice-point optimal. Owed to the large number of answer sets, computing one answer set is recommended.

For results, please click on one of the links below:

To download the examples, please click on one of the links below: