Heuristics for Hard ASP Programs

1 Introduction

Answer set programming (ASP) is a novel programming paradigm, which has been recently proposed in the area of nonmonotonic reasoning and logic programming. The idea of answer set programming is to represent a given computational problem by a logic program whose answer sets correspond to solutions, and then use an answer set solver to find such a solution [Lifschitz, 1999]. The knowledge representation language of ASP is very expressive in a precise mathematical sense; in its general form, allowing for disjunction in rule heads and nonmonotonic negation in rule bodies, ASP can represent every problem in the complexity class ΣP2 and ΠP2 (under brave and cautious reasoning, respectively) [Eiter et al., 1997]. Thus, ASP is strictly more powerful than SATbased programming, as it allows us to solve even problems which cannot be translated to SAT in polynomial time. The high expressive power of ASP can be profitably exploited in AI, which often has to deal with problems of high complexity. For instance, problems in diagnosis and planning under incomplete knowledge are complete for the the complexity class ΣP2 or ΠP2 , and can be naturally encoded in ASP [Baral, 2002; Leone et al., 2001].

∗This work was partially supported by the European Commission under projects IST-2002-33570 (INFOMIX) and IST-2001-37004 (WASP), and by FWF (Austrian Science Funds) under projects P16536-N04 and P17212-N04.

†Funded by APART of the Austrian Academy of Sciences.

Most of the optimization work on ASP systems has focused on the efficient evaluation of non-disjunctive programs (whose power is limited to NP/co-NP), whereas the optimization of full (disjunctive) ASP programs has been treated in fewer works (e.g., in [Janhunen et al., 2000; Koch et al., 2003]). In particular, we are not aware of any work concerning heuristics for ΣP2 /ΠP2 -hard ASP programs.

In this paper, we address the following two questions:

• ◮ Can the heuristics of ASP systems be refined to deal more efficiently with ΣP2 /ΠP2 -hard ASP programs?
• ◮ On hard ΣP2 /ΠP2 problems, can ASP systems compete with other AI systems, like QBF solvers?

We define a new heuristic hDS for the (disjunctive) ASP system DLV, aiming at improving the evaluation of ΣP2 /ΠP2 - hard ASP programs, but maintaining the benign behaviour of the heuristic of DLV on NP problems. We experimentally compare hDS against the DLV heuristic on hard 2QBF instances, showing a clear benefit. We also experiment the competitiveness of ASP w.r.t. QBF solvers on hard problems, indicating that ASP systems are very competitive with QBF systems on ΣP2 /ΠP2 -hard problems.

2 Answer Set Computation and Heuristics

We first recall the main steps of the computational process performed by ASP systems, in particular the DLV system, which will be used for the experiments.

An answer set program P in general contains variables. The first step of a computation of an ASP system eliminates these variables, then the following algorithm is invoked:

FunctionModelGenerator(I: Interpretation): Boolean; begin

I := DetCons(I); if I = L then return False; (* inconsistency *) if no atom is undefined in I then return IsAnswerSet(I); Select an undefined ground atom A according to a heuristic; if ModelGenerator(I ∪ {A}) then return True;

else return ModelGenerator(I ∪ {not A});

end;

Roughly, the Model Generator produces some "candidate" answer sets. The stability of each of them is subsequently verified by the function IsAnswerSet(I), which verifies whether the given "candidate" I is a minimal model of the GLtransformed program and outputs the model, if so. IsAnswer- Set(I) returns True if the computation should be stopped and False otherwise.

The function DetCons() computes an extension of I with the literals that can be deterministically inferred (or the set of all literals L upon inconsistency). If DetCons does not detect any inconsistency, an atom A is selected according to a heuristic criterion and ModelGenerator is called on I ∪{A} and on I ∪{not A}. The atom A plays the role of a branching variable of a SAT solver.

The heuristic hUT , proposed in [Faber et al., 2001] is currently employed in DLV. It is mostly based on the number of UnsupportedTrue (UT) atoms (called MBTs in [Faber et al., 2001]), i.e., atoms which are true in the current interpretation but miss a supporting rule, trying to minimize UT atoms and hence more likely arrive at supported models.

For hard ASP programs (i.e., non-HCF programs [BenEliyahu and Dechter, 1994] - they express ΣP2 -complete problems under brave reasoning), supported models are often not answer sets. Moreover, answer-set checking is computationally expensive (co-NP), and may consume a large portion of the resources needed for computing an answer set.

We therefore propose the new heuristic hDS, which tries in addition to maximize the degree of supportedness, the average number of supporting rules for non-HCF true atoms. Intuitively, if all true atoms have many supporting rules in a model M, then the elimination of an atom from the model would violate many rules, and it becomes less likely to find a subset of M which is a model of the reduct P M , disproving that M is an answer set. We define hDS as a refinement of the heuristic hUT (i.e., A <hUT B ⇒ A <hDS B). In this way, hDS keeps the behaviour of the well-assessed hUT on NP problems while, as we will see in Section 3, it sensibly improves over hUT on hard 2QBF problems (ΣP2 -complete).

3 Comparing hUT vs hDS: Experiments

We generated randomly a data set of 100 2QBF formulas, following [Gent and Walsh, 1999], and used the ASP encoding described in [Leone et al., 2005].

Experiments were performed on a PentiumIV 1500 MHz machine with 256MB RAM running SuSe Linux 9.0. For every instance, we allowed a maximum running time of 7200 seconds (two hours). The results of our experiments are displayed in the following graphs, in which a line stops whenever some instance was not solved within the time limit.

4 ASP vs QBF Solvers

The main goal of this paper is to improve the performance of ASP systems for problems located at the second level of the polynomial hierarchy. One may wonder whether, on such ΣP2 /ΠP2 -hard problems, ASP systems are competitive with other AI systems, like the QBF solvers. In order to give a first answer to this question, we have also performed a comparison with QBF solvers Quantor [Biere, 2004], Semprop [Letz, 2002], and yQuaffle [Zhang and Malik, 2002] on the set of all ΣP2 - and ΠP2 -complete QBF formulas of the last QBF competition. The results below report the number of instances solved within 660s and show that DLV (with heuristic hDS) generally outperformed the QBF solvers.