Answer Set Programming (ASP) is an established logic-based programming paradigm which has been successfully applied for solving complex problems since it features efficient implementations. In previous work we showed how to obtain ASPQ, a fairly effective 2QBF solver, by just resorting to state of the art ASP solvers. In this work we describe how we have optimized it to exploit some unexpressed potential of its solving strategy. The resulting empowered solver won the Hard Instances Track in the 2018 QBFEval.
Answer Set Programming (ASP) [
The core language of ASP, which features disjunction in rule heads and
nonmonotonic negation in rule bodies, can be used to solve all problems at the second level of
the polynomial hierarchy. Given the large progress measured in the last few years in
ASP solving, it is natural to ask whether this solving technology can applied profitably
also for solving 2QBFs, the canonical problem for the second level of the polynomial
hierarchy. Actually, we implemented a quite effective ASP-based 2QBF solver called
ASPQ [
The paper is structured as follows: In section 2 we overview quantified boolean formulas; in Section 3 we recall the ASP language; in Section 4 we describe the Eiter and Gottlob transformation; in Section 5 we describe the main algorithm of our solver; in Section 6 we comment on the performance of ASPQ at the 2018 QBFEval; we draw the conclusion in Section 7. 2
In this section, we introduce the logic of Quantified Boolean Formulas (QBFs), where
variables can be existentially or universally quantified. Hence, QBF extends
propositional logic, where all variables are existentially quantified, and the satisfiability
problem comes from NP-complete to PSPACE-complete [
A variable x is an element of a set G of propositional letters and a literal l is a variable (e.g., x) or the negation of a variable (e.g., :x). We denote by jlj the variable occurring in the literal l, and by :l the complement of l , i.e., :l = x, if l = :x, and :l = :x, if l = x. Given a natural number k > 0, a k-clause is a disjunction of k literals, and a propositional formula of arity k is a conjunction of k-clauses. A quantified Boolean formula F is an expression of the form Q1x1 : : : QnxnF (1) where, for each i = 1; : : : ; n, xi is a variable, Qi is either an existential quantifier, that is Qi = 9 or a universal quantifier, that is Qi = 8, and F is a propositional formula in the variables x1, ..., xn, called the matrix of F . We say that l is an existential literal, if jlj = xi and Qi = 9, for some i = 1; : : : ; n, otherwise we say that l is a universal literal. Finally, whenever there is 1 k n such that, Q1 = : : : = Qk = 9, and Qk+1 = : : : = Qn = 8, we say that F is a 2QBF formula. 2.2 First, given a literal l and a QBF formula of the form F = QxY , where Y is a QBF formula, we denote by Fl the QBF formula obtained from Y by removing all the conjuncts in which l occurs, and removing :l from the others. Moreover, we say that a clause is contradictory, whenever it does not contain existential literals.
Let F be a QBF formula of the form (1). We define the semantics of a QBF formula recursively as follows. If F contains a contradictory clause, then F is false; if F has no conjuncts, then F is true; if F = 9xY , and Fx or F:x are true, then F is true; if F = 8xY , and Fx and F:x are true, then F is true. The QBF satisfiability problem (QSAT) is to decide whether a given QBF formula is true or false.
Example 1. Consider the 2QBF formula F = 9x8yF, where F = (x _ y) ^ (:x _ :y). Therefore, Fx = 8y(:y) and F:x = 8y(y). Then, from Fx, we obtain (Fx)y = () and (Fx):y = 0/ ; and from F:x, we obtain (F:x)y = 0/ and (F:x):y = (). Hence, since (Fx):y is false and (Fx):y is true, thus Fx is false; and since (F:x)y is true and (F:x):y is false, thus F:x is also false. Therefore, we can conclude that F is false.
Example 2. Consider the 2QBF formula F = 9x8yF, where F = (x _ y) ^ (x _ :y). Therefore, Fx = 8y0/ and F:x = 8y(y) ^ (:y). Then, in particular, Fx is true. Therefore, we can already conclude that F is true. 3
Answer Set Programming (ASP) [
Following the traditional grounding view [
Example 3. Consider the disjunctive logic program
P = fa c; not b; b _ c not dg: Therefore, the set of all minimal model of P is given by MM(P) = ffdg; fbg; fa; cgg. Instead, the set of all answer sets is AS(P) = ffbg; fa; cgg. Hence, P is a coherent logic program. Note that I = fdg is not an answer set of P, since I is not a minimal model of PI = fa cg.
.
Therefore, the set of all minimal model of P is given by MM(P) = ffa; c; dg; fa; b; dg; fa; b; eg, fb; c; dg; fc; egg. However, fa; b; eg and fc; eg are not answer sets of P, as the rule d not e is deleted in the reduct, and e can not belong to a minimal model of the reduct. Moreover, Pfa;c;dg = fa; dg; Pfa;b;dg = fb; dg; and Pfb;c;dg = fc; dg. Therefore, also fa; c; dg, fa; b; dg, and fb; c; dg are not answer sets of P. Thus, P is an incoherent logic program. 4
In this section, we introduce the translation from 2QBFs to logic programs proposed by
Eiter and Gottlob [
To describe the translation, let F = 9X 8Y F be a quantified boolean formula, where we may assume that X = fx1; : : : ; xeg, Y = fy1; : : : ; yag and F = D1 _ : : : _ Dm, such that Di = Li;1 ^ : : : ^ Li;a+e and Li; j are literals over X [ Y . For every atom z 2 X [ Y , we introduce a fresh atom z0, and we set s (z) = z and s (:z) = z0. Finally, we introduce one more fresh atom, say w, and define a disjunctive logic program PF consisting of the following rules: z _ z0 y w w w and y0
w
s (Li;1); : : : ; s (Li;a+e)
not w
Eiter and Gottlob in [
Theorem 1. Let F be a 2QBF formula. Then, F is true if, and only if, PF is coherent.
We enlighten the translation described above through two examples.
F = 9x8y8z((x ^ y) _ (x ^ :y ^ :z) _ (:y ^ z)): >>>>8 yx _ xw0;; < z w; >> w x; y; w >:> w Hence, PF has as unique answer set fx; y; y0; z; z0; wg, corresponding to set x to true in F . So that, according to Theorem 1, F is true.
F = 9x9y8z((x ^ :z) _ (:x ^ y ^ :z)): Hence, PF is incoherent. Indeed, there are only two choices to infer w, fx; z0g and fx0; y; z0g. Therefore, an interpretation candidate must contain one of the two sets. In both cases, it cannot be an answer set. Indeed, we have three candidate models: I1 = fx; y; z; z0; wg; I2 = fx; y0; z; z0; wg; and I3 = fx0; y; z; z0; wg. However, none can be an answer set. Indeed, fx; y; zg is a minimal model of PI1 ; fx; y0; zg is a minimal model of PI2 ; and fx0; y; zg is a minimal model of PI3 . In conclusion, according to Theorem 1, F is false. 5
We first present the ASPQ main algorithm, and then introduce a result that allowed us to optimize ASPQ performance.
Input : A 2-QBF formula F
Output: SAT or UNSAT 1 begin 2 Tbloqqer := 120s; Tclasp := 60s 3 F := BLOQQER (Tbloqqer, F); 4 if F = > then return SAT; 5 if F = ? then return UNSAT; 6 P := QDimacs2ASP(F); 7 res := CLASP (Tclasp, P ); 8 if res = UNKNOWN then res := WASP (P ); 9 if res = COHERENT then return UNSAT; 10 if res = INCOHERENT then return SAT; 11 return UNKNOWN; // QBFEval settings; // solved by bloqqer // solved by bloqqer // encode the logic program // run clasp for Tclasp seconds // run wasp if unsolved 5.1
The main algorithm implemented in ASPQ is reported as Algorithm 1. The input
formula F is first simplified by the preprocessor BLOQQER [
We now abstract the ASPQ algorithm considering a setting in which more than two solvers have to be run in sequence, to draw a result that holds also in a more general setting.
Let fS1; : : : ; Sng be a set of n solvers, finst1; : : : ; instmg a set of m instances, Tj the maximal execution time given to the solver S j, and tijnstk the execution time to solve the instance instk by solver S j.
Given a topological ordering S = (S1; : : : ; Sn) to run the solvers in series, we denote by m j the number of solved instances by solver S j with respect to the topological ordering S, i.e., the number of instances solved by S j and not by Si, for each i < j. Let finst1j ; : : : ; inst mj j g be the set of instances solved by solver S j with respect to S.
Note that S can be seen as a new solver. Assume that T = T1 + : : : + Tn is the maximal execution time given to the solver S. Hence, the total number of solved instances by S is given by M = m1 + : : : + mn. We denote by TS the total execution time to solve the M instances by S. Hence, the following result holds.
Theorem 2. Let (S1; : : : ; Sn) be a topological ordering to run the solvers in series. Then,
n mk k n TS = å å tinstkh + å k=1 h=1 j=2
n ! Tj 1 å mi : i= j Proof. We give a constructive proof. Clearly, to solve instances in finst11; : : : ; inst1m1 g, the solver S spends the same time of the solver S1. Hence, ti1nst11 + : : : + ti1nst1m1 . Then, to solve instances in finst21; : : : ; inst2m2 g, the solver S spends the time of the solver S2 to which is added the maximal execution time given to the solver S1, that is T1. Hence, Tn 1)mn + (tinnstn1 + : : : + tinnstnmn ). (T1 + ti2nst21 ) + : : : + (T1 + ti2nst2m2 ) = T1m2 + (t2 inst21 + : : : + ti2nst2m2 ). At the end, to solve instances in finstn1; : : : ; instnmn g, the solver S spends the time of the solver Sn to which is added the maximal execution time given to the solvers S1, S2, ..., Sn 1, that is T1 + : : : + Tn 1. Hence, (T1 + : : : + Tn 1 +tinnstn1 ) + : : : + (T1 + : : : + Tn 1 +tinnstnmn ) = (T1 + : : : +
We have applied the result stated in Theorem 2 to optimize the performance of ASPQ. In particular, we have selected the time thresholds to minimize TS on a preliminary experiment, and then used the result to configure the solver. The details are provided in the next section.
In this section we describe the implementation of ASPQ and then we narrate the history of optimization of our system. Finally we comment on the official results of the 2QBFEvaluation where ASPQ performed well in the 2QBF Track and won the Hard Instances Track.
ASPQ was implemented as a bash script that calls its four main modules implemented
in separate commands, namely: Bloqqer, QDimacs2ASP, WASP and CLASP. The bash
script follows faithfully Algorithm 1. Bloqqer, WASP and CLASP are called as external
processes, and were obtained by downloading and compiling the sources from the
respective websites. The QDimacs2ASP component is a genuine Java implementation of
the Eiter-Gottlob transformation presented in Section 4 that takes as input an instance
of 2QBF in the standard QDIMACS format used in QBFEvaluations, and outputs a
grouns ASP program in lparse format. Time measurement are implemented resorting
to the standard time command, that interrupts the execution of a subprocess if the
computation exceeds the maximum allotted time. The intermediate results, produced by
Bloqqer and QDimacs2ASP are stored in temporary files, that are destroyed once the
system ends the computation. Tbloqqer, Tclasp , and Twasp can be specified by modifying
the three corresponding variables declared in the main bash script. The resulting
implementation can be easily updated with newer versions of the internal components, and
one can easily modify the maximum time thresholds by just editing the script with a
text editor.
ASPQ entered the 2016 QBFEval in the 2QBF track as non competing system (it was
submitted two days after the official solver submission deadline). We set Tbloqqer = 60s,
so that preprocessing never occupies more than 10% of the allotted time (the timeout
was set by the organizers to 600s); and we set Tclasp = 120s. This choice is motivated by
the results of a preliminary experiment on the QBF instances used in ASP competitions,
where CLASP solved the majority of instances within this time. After this experience,
for QBFEval 2017 the timeout was increased to 900 seconds by the organizers, and we
have updated the executables (with newer versions of Bloqqer, CLASP and WASP) and
submitted the system with Tbloqqer = 125s resulting in ASPQ v.2. The new setting was
suggested by observing that Bloqqer processing is always beneficial for our system,
and it terminates almost always in less than 125s in the QBFEval instances selected in
2016. An ugly bug limiting the execution to (the old timeout of) 600s influenced ASPQ
v.2 performance in 2017. Thus, in 2018 we have fixed the bug and submitted both a fixed
version of ASPQ (v.2) and a new one where we have optimized the thresholds by running
once a python procedure that optimizes TS of Theorem 2. We used as base the results
obtained running each single component solver paired with Bloqqer, configured with
different heuristics and choices of partial checks configurations (for the details on these
parameters see [
ASPQ entered both the 2QBF track and the Hard Instances Track of QBFEval 2018. 2QBF Track. The results in the 2QBF track are summarized in Table 1, reporting the list of participants ordered by the number of solved instances (reported in a separate column). This elaboration has been done on the official results published in the QBFEval 2018 website. The optimized ASPQ v.3 reached the fourth place in the competition, solving only three, five and eight instances less than predyndep, CADET, and depqbfvariants-QxQBH occupying the first three places, respectively. The unoptimized (but fixed) ASPQ v.2 solved 18 instances less than ASPQ v.3 occupying the 9th place. All in all the optimization criterion presented in this paper allowed to improve significantly our solver, and the resulting performance is basically aligned with the best options. It is worth noting that, all the other systems are based on native methods for solving QBF, whereas our implementation resorts to a translation, nonetheless it results to be very competitive.
Hard Instances Track. The results in the Hard Instances track are summarized in Figure 1, reporting a snapshot of the official slides presented at SAT 2018. Despite being able to solve only 2QBF instances (the track included also instances with more than two quantifiers) ASPQ v.3 could solve the majority of instances, more than twice as much as the solver in second position. Recall that, the Hard instances Track contained selected instances that no QBF solver could solve in previous edition from the CNF Track. This is an unexpected but impressive result that confirms the effectiveness of the optimized implementation of ASPQ and the efficiency of the ASP solvers employed by our system. 7
Answer Set Programming is an established logic-based programming paradigm that can
be used to solve complex problems. ASP solving technology has steadily improved in
the last few years, as demonstrated by ASP Competitions. Since the introduction of the
first version of ASPQ, it was clear that ASP solving technology can be used fruitfully
to solve 2QBF instances [
As far as future work is concerned, we are considering to tune our system by exploring the usage of the many different heuristics implemented by ASP solvers.