We present an overview of models of random quanti ed boolean formulas and their natural random disjunctive ASP program counterparts that we have recently proposed. The models have a simple structure but also theoretical and empirical properties that make them useful for further advancement of the SAT, QBF and ASP solvers.
The study of theoretical and practical properties of random models has received
substantial attention in Computer Science. The results obtained in these studies
have had major practical impact especially in boolean satis ability (SAT) [
Previous work in this area mainly focused on random formulas in the
conjunctive normal form (CNF), and random prenex-form QBFs with the matrix in
CNF or disjunctive normal form (DNF) (depending on the quanti er sequence).
The xed-length clause model of k-CNF formulas and its 2QBF extension have
been the subjects of extensive studies. Formulas in the xed-length clause model
consist of m clauses over a ( xed) set of n variables, each clause with k
noncomplementary literals. All formulas are assumed to be equally likely. For that
model it is known that there are reals l(k) and u(k) such that if m=n < l(k),
a formula from the model is almost surely satis able (SAT), and if m=n > u(k),
almost surely unsatis able (UNSAT). It is conjectured that l(k) = u(k). That
conjecture is still open. However, it holds asymptotically, i.e., the two bounds
converge to each other with k ! 1 [
The xed-length clause model was extended to QBFs by Chen and Interian
[
In [
In this paper we give an overview of the random models presented in [
In this section, we recall the xed-length clause model for random CNF formulas
and the Chen-Interian model for random QBF formulas. We then describe the
models of QBFs and programs proposed by [
The xed-length clause model. The model is given by the set C (k; n; m) of CNF formulas, with all formulas assumed equally likely. Formulas from the model can be generated by selecting m k-literal clauses over a set of n variables uniformly, independently and with replacement. Let us denote by p(k; n; m) the probability that a random formula in C (k; n; m) is SAT. We de ne l(k) to be the supremum over all real numbers x such that for every < x, it holds that limn!1 p(k; n; b nc) = 1. Similarly, we de ne u(k) to be the in mum over all real numbers x such that for every > x, limn!1 p(k; n; b nc) = 0. It is known that l(k) and u(k) are well de ned. Moreover, l(k) u(k) and, it is conjectured that l(k) = u(k). The conjecture holds asymptotically, that is, limk!1 l(k) = limk!1 u(k).
The Chen-Interian model. The model generates QBFs of the form 8X9Y F , where sets X and Y are disjoint, jXj = A, jY j = E, and F is a CNF formula with m clauses, each containing a literals with variables in X and e literals with variables in Y . We write Q(a; e; A; E; m) for the set of all such QBFs. The Chen-Interian model generates QBFs from Q(a; e; A; E; m), with all formulas equally likely. Let q(a; e; A; E; m) be the probability that a random QBF from Q (a; e; A; E; m) is true. Let r > 0 be a xed real. We set l(a; e; r) to be the supremum over all real numbers x such that for every < x, limn!1 q(a; e; A; E; b nc) = 1, where A = brEc and n = A + E. Similarly, we set u(a; e; r) to be the in mum over all real numbers x such that for every > x, limn!1 q(a; e; A; E; b nc) = 0, again with A = brEc and n = A + E. Chen and Interian proved that l(a; e; r) and u(a; e; r) are well de ned. Clearly, l(a; e; r) u(a; e; r). Whether l(a; e; r) = u(a; e; r) is an open problem. The quantities l(a; e; r) and u(a; e; r) delineate the phase-transition region. For QBFs generated from the model Q(a; e; brEc; E; b nc) (with xed r), Chen and Interian experimentally observed the easy-hard-easy pattern as grows, showed that the hard region is aligned with the phase transition, and that the same behavior emerges no matter what concrete r is xed as the ratio A=E. 3
Random SAT and QBF. Let F be a class of propositional formulas (or a model of
random formula). By t-F we denote the class of all disjunctions of t formulas from
F (or a model generating disjunctions of random formulas from F ). Similarly,
if Q is a class (model) of QBFs of the form 8X9Y F , where F 2 F , we write
t-Q for the class (model) of all QBFs of the form 8X9Y F , where F 2 t-F . We
refer to models t-F and t-Q as multi-component. For QBFs we also consider the
dual model to t-Q, based on conjunctions of t DNF formulas. It gives rise to
the multi-component model of disjunctive logic programs via the Eiter-Gottlob
translation [
In our work we focus on models based on the model C(k; n; m). First, we note that the corresponding multi-component model t-C (k; n; m) has similar satis ability properties and that the phase transition regions in the two models are closely related. Let pt(k; n; m) be the probability that a random formula in t-C (k; n; m) is SAT.
Theorem 1 Let t 1 be a xed integer. Then, for every < l(k), it holds that limn!1 pt(k; n; b nc) = 1, and for every > u(k), limn!1 pt(k; n; b nc) = 0.
The proof follows from the identity pt(k; n; m) = 1 (1 p(k; n; m))t.Thus, if the phase transition conjecture holds for the single component model C (k; n; m), it also holds for the multi-component model t-C (k; n; m), and the threshold value is the same for every t.
We also considered the multi-component model t-Q(a; e; A; E; m) of QBFs, with the Chen-Interian model as its single-component. Let qt(a; e; A; E; m) be the probability that a random QBF from t-Q(a; e; A; E; m) is true (in particular, q1(a; e; A; E; m) = q(a; e; A; E; m)). Extending Chen and Interian's work, we can prove that the phase transition for di erent values of t coincide (and coincide with the phase transition in the Chen-Interian model).
Theorem 2 For every integer t 1 and real number r > 0: if < l(a; e; r), it holds that limn!1 qt(a; e; A; E; b nc) = 1, and if > u(a; e; r), it holds that limn!1 qt(a; e; A; E; b nc) = 0 (where A = brEc and n = A + E).
The theorems above describe the situation when t is xed and n is large. When n is xed and t grows, the analysis of pt(k; n; m) and qt(a; e; A; E; m) shows that the region of the transition from SAT to UNSAT shifts to the right. Of course, once we stop growing t and start increasing n again, the phase transition region will move back to the left.
Random Disjunctive Programs. Our model of random disjunctive programs is
based on the translation from QBFs to programs due to Eiter and Gottlob [
The Eiter-Gottlob translation has a simple extension to QBFs obtained from the multi-component models. We write t-Ddlp(e; a; E; A; m) for the set of programs consisting of the following xed part: z _ z0, for each z 2 Z; y w, and y0 w, for each y 2 Y ; w w1; : : : ; wt, and w not w. And the core of mt Horn rules of the form wh z1; : : : ; z`, where h = 1; : : : ; t, each wh is the head of exactly m rules, ` = e + a, and the body of each rule has e atoms z and z0 with z 2 X (and so, also a atoms of the form z and z0 with z 2 Y ). Note that programs in 1-Ddlp(e; a; E; A; m) coincide with those in Ddlp(e; a; E; A; m) modulo a rewriting, where the rule w w1 is removed and w1 is replaced by w.
Programs in t-Ddlp (e; a; E; A; m) correspond to 98 QBFs whose matrix belongs to t-D (e; a; E; A; m). They can be seen as the results of translating QBFs into logic programs dlp , where we use variables wi to represent component DNF formulas in the matrix of . The correspondence 7! dlp preserves the semantics in the following sense.
Theorem 3 Let = 9X8Y F , for F 2 t-D (e; a; E; A; ; m). Then is true if and only if dlp has an answer set, where dlp is the disjunctive logic program in t-Ddlp (e; a; E; A; m) corresponding to .
Empirical properties and conclusion. The experimental results on satis ability [