Abstract | ||
---|---|---|
HEX programs extend logic programs with external computations through external atoms, whose answer sets are the minimal models of the Faber-Leone-Pfeifer-reduct. As already reasoning from Horn programs with nonmonotonic external atoms of polynomial complexity is on the second level of the polynomial hierarchy, answer set checking needs special attention; simply computing reducts and searching for smaller models does not scale well. We thus extend an approach based on unfounded sets to HEX and integrate it in a Conflict Driven Clause Learning framework for HEX program evaluation. It reduces the check to a search for unfounded sets, which is more efficiently implemented as a SAT problem. We give a basic encoding for HEX and show optimizations by additional clauses. Experiments show that the new approach significantly decreases runtime. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-33353-8_13 | JELIA |
Keywords | Field | DocType |
polynomial complexity,hex program,unfounded set,answer set,hex program evaluation,polynomial hierarchy,hex-program evaluation,new approach,nonmonotonic external atom,external computation,external atom,nonmonotonic reasoning,answer set programming | Polynomial hierarchy,Conflict-Driven Clause Learning,Minimal models,Computer science,Theoretical computer science,Non-monotonic logic,Answer set programming,Program evaluation,Encoding (memory),Computation | Conference |
Citations | PageRank | References |
6 | 0.41 | 15 |
Authors | ||
5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Thomas Eiter | 1 | 7238 | 532.10 |
Michael Fink | 2 | 1145 | 62.43 |
Thomas Krennwallner | 3 | 468 | 29.14 |
Christoph Redl | 4 | 137 | 13.76 |
Peter Schüller | 5 | 192 | 22.61 |