Generating Hard Random Boolean Formulas and Disjunctive Logic Programs

1 Introduction

Models for generating random instances of search problems have received much attention from the artificial intelligence community in the last twenty years. The results obtained for boolean satisfiability (SAT) [Achlioptas, 2009] and constraint satisfaction (CP) [Mitchell, 2002] have had major impact on the development of fast and robust solvers, significantly expanding their range of effectiveness as general purpose tools for solving hard search and optimization problems arising in AI, and scientific and engineering applications. They also revealed an intriguing phase-transition phenomenon often associated with the inherent hardness of instances, and provided theoretical and experimental basis for a good understanding of the phase-transition phenomenon.

Models of random propositional formulas and QBFs that can reliably generate large numbers of instances of a desired hardness are important [Gent and Walsh, 1999]. Inherently hard instances for SAT and QBF solvers are essential for designing and testing search methods employed by solvers [Achlioptas, 2009], and are used to assess their performance in solver competitions [J¨arvisalo et al. 2012; Narizzano et al. 2006; Calimeri et al. 2016]. On the flip side, large collections of easy instances support the so-called fuzz testing, used to reveal problems in solver implementation, as well as defects in solver design [Brummayer et al. 2010].

Previous work mainly focused on random CNF formulas and random prenex-form QBFs with the matrix in CNF or DNF (depending on the quantifier sequence). The fixedlength clause model of k-CNF formulas and its 2QBF exten-

Miroslaw Truszczynski

University of Kentucky, USA mirek@cs.uky.edu

sion have been especially well studied. Formulas in the fixedlength clause model consist of m clauses over a (fixed) set of n variables, each clause with k non-complementary 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 satisfiable (SAT), and if m/n > ρu(k), almost surely unsatisfiable (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 → ∞ [Achlioptas and Moore, 2002]. For the best studied case of k = 3, we have ρl(3) ≥ 3.52 and ρu(3) ≤ 4.49 [Achlioptas, 2009], and experiments show that the phase transition ratio m/n is close to 4.26 [Crawford and Auton, 1996]. Important for the solver design and testing is that instances from the phase transition region are hard and those from regions on both sides of the phase transition are easy, a property called the easy-hardeasy pattern [Selman et al., 1996] or, more accurately, the "easy-hard-less hard" pattern [Coarfa et al., 2003]. Empirical studies suggest that SAT solvers devised for solving random formulas are usually not effective with real world instances; vice versa solvers for industrial instances are less efficient on random formulas [J¨arvisalo et al., 2012]. This is often attributed to some form of (hidden) structure present in industrial problems that solvers designed for industrial applications can exploit [Ans´otegui et al., 2009]. Finding models to generate random formulas with "structure" that behave similarly to those arising in practice is an important challenge [Kautz and Selman, 2003]. Ans´otegui et al. [2009] presented the first model that may have this property: despite the "randomness" of its instances, they are better solved by solvers tuned to industrial applications. More recently, Gir´aldez-Cru and Levy [2016] proposed a model of random SAT based on the notion of modularity, and showed that formulas with high modularity behave similarly to industrial ones.

The fixed-length clause model was extended to QBFs by Chen and Interian [2005]. In addition to n and m (understood as above), their model includes parameters controlling the structure of formulas. Once these parameters are fixed, similar properties as in the case of the k-CNF model emerge. There is a phase transition region associated with a specific value of the ratio m/n (that does not depend on n) and the easy-hard-easy pattern can be experimentally verified.

These two models are based on formulas in normal forms.

However, many applications give rise to formulas in nonnormal forms motivating studies of solvers of non-normal form formulas and QBFs, and raising the need of models of random non-normal form formulas. The fixed-shape model proposed by Navarro and Voronkov [2005], and studied by Creignou et al. [2012], is a response to that challenge.

Motivated by the work on random SAT and QBF models, researchers proposed models of random logic programs, and obtained empirical and theoretical results concerning their properties [Zhao and Lin 2003; Namasivayam and Truszczynski 2009; Wang et al. 2015; Wen et al. 2016]. Those results are limited to non-disjunctive logic programs. No models for disjunctive logic programs have been proposed so far. Such results would be of substantial interest to answer set programming (ASP) [Brewka et al., 2011], a popular computational formalism based on disjunctive logic programs.

In this paper, we propose and study models of random nonnormal form formulas and 2QBFs. Specifically, we consider disjunctions of t k-CNF formulas (in the case of QBFs, using them as matrices). We call models generating such formulas multi-component. Instances we obtain in this way are not formulas from the fixed-shape model of Navarro and Voronkov, as their building blocks (k-CNF formulas) do not have a fixed size. Importantly, via the encoding by Eiter and Gottlob [1995], the multi-component models of QBFs give rise to a model of random disjunctive logic programs. Our models exhibit the phase transition and, aligned with it, easy-hard-easy pattern. We obtain theoretical bounds on the location of the phase transition, and conduct a comprehensive experimental study. In experiments, we considered several ASP, SAT and QBF solvers to exclude a possibility of a bias being an artifact of committing to a specific solver. For a fixed t, we study hardness as a function of the ratio m/n and show that the regions of hardness for the models lie within their phase transition regions. Importantly, we study hardness as a function of t, the number of components, and show that as t grows generated instances get orders of magnitude harder. As Ans´otegui et al. [2009], we compare SAT solvers designed for random instances with those designed for real-world ones. We find that for t ≥ 2 our models generate instances better solved by SAT solvers for real-world instances, and that the difference grows as t grows. We measure the effect of t on processing disjunctive programs, and show that t allows us to control the amount of computation dedicated to stable model checking [Koch et al., 2003].

Our results provide new ways to generate hard and easy instances of propositional formulas, QBFs and disjunctive programs. Our models can generate instances of increasing hardness with properties affecting solver performance in a similar way real-world instances do. The results are particularly important to the development of disjunctive ASP solvers, as no models for generating random disjunctive programs of desired hardness have been known before.

2 Preliminaries

A clause is a set of literals that contains no pair of complementary literals. A CNF formula is a set of clauses. Disjunctions of CNF formulas are also understood as sets of their constituents. The dual concepts (e.g., DNF formulas) are defined similarly. By C (k, n, m) we denote the set of all k-CNF formulas with m clauses over (some fixed) set of n propositional variables. Similarly, D(k, n,m) is the set of all kDNF formulas, i.e., disjunctions of m conjunctions of k noncomplementary literals over an n-element set of variables.

The fixed-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. As we noted, the model is well understood. In particular, let us denote by p(k, n,m) the probability that a random formula in C(k, n,m) is SAT. We define ρl(k) to be the supremum over all real numbers x such that for every ρ < x, limn→∞p(k, n, ⌊ρn⌋) = 1. Similarly, we define ρu(k) to be the infimum over all real numbers x such that for every ρ > x, limn→∞ p(k, n, ⌊ρn⌋) = 0. As we mentioned, ρl(k) and ρu(k) are well defined. Moreover, ρl(k) ≤ ρu(k) and, it is conjectured that ρl(k) = ρu(k). Experimental results agree with these theoretical predictions.

The Chen-Interian model. The model generates QBFs of the form ∀X∃Y F . Sets X and Y are disjoint and contain all propositional variables that may appear in F. The sizes of X and Y are prescribed to some specific integers A and E, respectively. Moreover, each clause in F contains a literals over X and e literals over Y for some specific values a and e. We denote the set of all such CNF formulas F with m clauses by C(a, e;A,E;m). Clearly, C(a, e;A,E;m) ⊆ C(a + e,A + E,m). We write Q(a, e;A,E;m) for the set of all QBFs ∀X∃Y F, where F ∈ C(a, e;A,E;m). The ChenInterian model generates QBFs from Q(a, e; A, E; m), with all formulas equally likely.

Chen and Interian [2005] presented a comprehensive experimental study of the model. 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 fixed real. We set νl(a, e; r) to be the supremum over all real numbers x such that for every ν < x, limn→∞ q(a, e;A,E; ⌊νn⌋) = 1, where A = ⌊rE⌋ and n = A + E. Similarly, we set νu(a, e; r) to be the infimum over all real numbers x such that for every ν > x, limn→∞ q(a, e;A,E; ⌊νn⌋) = 0, again with A = ⌊rE⌋ and n = A + E. Chen and Interian proved that νl(a, e; r) and νu(a, e; r) are well defined. 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; ⌊rE⌋, E; ⌊νn⌋) (with fixed 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 fixed as the ratio A/E.

3 Multi-component Models

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 ∀X∃Y F, where F ∈ F, we write tQ for the class (model) of all QBFs of the form ∀X∃Y F, where F ∈ t-F. We refer to models t-F and t-Q as multicomponent. 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 all cases, we assume that formulas (QBFs, respectively) are equally likely.

In our work we focus on models based on the model C(k, n,m). First, we note that the corresponding multicomponent model t-C(k, n,m) has similar satisfiability 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 fixed integer. Then, for every ρ < ρl(k), limn→∞ pt(k, n, ⌊ρn⌋) = 1, and for every ρ > ρu(k), limn→∞ pt(k, n, ⌊ρn⌋) = 0.

The proof follows from the identity pt(k, n, m) = 1-(1p(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 tQ(a, e;A,E;m) of QBFs, with the Chen-Interian model as its single-component specialization. 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 different values of t coincide (and coincide with the phase transition in the Chen-Interian model).

Theorem 2 For every integer t ≥ 1 and real r > 0, if ν < νl(a, e; r), then limn→∞ qt(a, e; A, E; ⌊νn⌋) = 1, and if ν > νu(a, e; r), limn→∞ qt(a, e;A,E; ⌊νn⌋) = 0 (where A = ⌊rE⌋ and n = A + E).

The theorems above describe the situation when t is fixed and n is large. When n is fixed 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.

The experimental results on satisfiability we present later agree with this theoretical analysis; we will also see the easyhard-easy pattern and a strong dependence of hardness on t.

4 RandomDisjunctive Programs

Our results on QBFs imply a model of random disjunctive logic programs. This is important as disjunction increases the expressive power of answer set programming posing, at the same time, a computational challenge [Brewka et al., 2011].

Our model of random disjunctive programs is based on the translation from QBFs to programs due to Eiter and Gottlob [1995]. It works on the model dual to the one we discussed above. The model consists of QBFs Φ = ∃X∀Y F, where F ∈ D(e, a;E,A;m), the set of formulas dual to C(e, a;E,A;m). The model clearly has the same properties (modulo a switch between true and false). To describe the translation, let us assume that X = {x1, . . . , xE}, Y = {y1, . . . , yA} and F = D1 ∨ . . . ∨ Dm, where Di = Li,1 ∧. . .∧Li,a+e and Li,j are literals over X∪Y . For every atom z ∈ X ∪ Y we introduce a fresh atom z′ . For every z ∈ X ∪ Y , we set σ(z) = z and σ(¬z) = z′ . Finally, we introduce one more fresh atom, say w, and define a disjunctive logic program PΦ to consist of the following rules:

Eiter and Gottlob proved that Φ is true if and only if PΦ has an answer set. Thanks to this correspondence, the model D(a, e;A,E;m) gives rise to a model of disjunctive logic programs. We denote it (and, with some abuse of notation, the set of programs it consists of) by Ddlp(e, a; E, A; m).

The set of atoms of programs in Ddlp(e, a;E,A;m) is {w}∪Z ∪Z ′ , where Z = X∪Y and Z ′ = {z′ : z ∈ Z}. The structure of these programs is quite simple. Each program has a fixed part (the same in all programs)

and its unique core consisting of m Horn rules

where ℓ = e + a and the body of each rule has e atoms z and z′ with z ∈ X (and so, also a atoms z and z′ with z ∈ Y ).

This structure can be generalized. Assuming an additional set of t fresh atoms w1, . . . ,wt, we write tDdlp(e, a; E, A; m) for the set of programs consisting of:

as the fixed part, and the core of mt Horn rules of the form

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 z′ with z ∈ X (and so, also a atoms of the form z and z′ with z ∈ 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 ∃∀ 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 Φ ↦→ Φdlp preserves the semantics in the following sense.

Theorem 3 Let Φ = ∃X∀Y F , for F ∈ 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 Φ.

5 Empirical Analysis

We now present an experimental analysis of the behavior of our models and discuss their properties.

(g) Combined effect of variables and components (SAT)

(h) Combined effect of variables and components (QBF)

Figure 1: Behavior of multi-component model: phase transition and hardness.

Experiment Setup. To claim that properties and patterns are inherent to a model and not an artifact of a solver used, we performed our experiments with several well-known SAT, QBF and ASP solvers: the SAT solvers GLUCOSE 4.0 [Audemard et al., 2013] LINGELING, version of 2015 [Biere, 2014], and KCNFS, version of SAT'07 competition [Dequen and Dubois, 2006]; the QBF solvers BQ-CEGAR 1 , AIGSOLVE [Pigorsch and Scholl, 2010]; RAREQS [Janota et al., 2016], and AQUA-S2V 2 and the ASP solvers CLASP 3.1.3 [Gebser et al., 2007] and WASP 2.1 [Alviano et al., 2015], both paired with gringo 4.5.3.All solvers were run in their default configurations. We stress that we did not aim at comparing solver performance, instead our goal was to identify solver-independent properties inherent to a model.

Formulas generated according to the multi-component model with t > 1 are non-clausal, whereas the (Q)DIMACS format requires the formulas to be in CNF. Therefore, the generator transforms non-clausal formulas to CNF using the standard Tseitin transformation. Once a formula Φ is generated, it is stored in two files: one with an encoding of Φ in the (Q)DIMACS numeric format of (Q)SAT solvers [J¨arvisalo et al., 2012; Narizzano et al., 2006], and the other one with the disjunctive logic program corresponding to Φ in the ASPCore 2.0 syntax [Calimeri et al., 2016]. Since the formulas we generate are of the form ∀X∃Y F, the programs are obtained from their negations ∃X∀Y ¬F. They have answer sets if and only if the original formulas are false. Thus, when we analyze satisfiability we plot only the curves obtained by evaluating either the formulas or the corresponding logic programs (plots are symmetric). Experiments were run on a Debian Linux with 2.30GHz Intel Xeon E5-4610 v2 CPUs and 128GB of RAM. Each execution was constrained to one single core by using the taskset command. Time measurements were performed by using the runlim tool. Formulas were generated with a tool we developed in Java.The results are averaged over 128 samples of the same size.

Behavior of Multi-component Model. To study the satisfiability of multi-component model instances (the location of the phase transition), we considered the setting with the number of variables (propositional atoms) fixed. Figure 1(a) shows the results for the t component model t-C(3, 200,m), with t ∈ {1, 3, 5, 7, 9, 11}. The x-axis gives the ratio of the numbers of clauses and variables (m/200), the y-axis shows the frequency of SAT. Consistently with our theoretical results, the phase transition shifts from left to right, and it sharpens for growing values of t. The same can be observed in Figure 1(b), showing the frequency of QBFs from t-Q(1, 3, 24, 12, m) that are true, for t ∈ {1, 3, 5, 7, 9, 11}.

To study the hardness of the multi-component model we computed the average solver running times. The results (on the same instances as before) for the GLUCOSE SAT solver and the BQ-CEGAR QBF solver are in Figures 1(c) and 1(d). The plots show a strong dependency of the hardness on the number of components: the peak of hardness moves right and grows visibly with t. In more detail, the CNF formulas

1 A combination of bloqqer preprocessor [Heule et al., 2015] and ghostq [Klieber et al., 2013] solver from QBF gallery 2014.

2 www.qbflib.org/DESCRIPTIONS/aqua16.pdf

(one component) are solved by GLUCOSE in less than 0.42s, whereas instances with 11 components require about 7 minutes, i.e, they are more than 3 orders of magnitude harder. Analogous behavior is observed when running BQ-CEGAR on QBF formulas. Those from the one-component model are solved instantaneously (average time ≤ 0.01s), those from the 11-component model requires about one minute. The experiments with other solvers gave similar results.

To underline the dependency of the hardness on the number of components, for each solver we compute the average time over samples of the same size and plot its maximum (for simplicity maximum execution time) for several values of t in Figures 1(e) (SAT) and 1(f) (QBF, programs). In particular, Figure 1(e) reports the results obtained by running GLUCOSE and LINGELING, and Figure 1(f) - the results obtained by running BQ-CEGAR, AIGSOLVE, AQUA-S2V, RAREQS and the results obtained by running CLASP and WASP on the corresponding programs. The picture shows that the peak of difficulty grows with the number of components no matter the implementation or the representation roughly, at a rate that is more than quadratic with t (y-axis in logarithmic scale).

Next, we discuss the behavior of formulas when both the number of variables and the number of components grow. Figure 1(g) reports on the behavior of CNF formulas with n ∈ {100, 200} and t ∈ {1, 10}. Formulas with 100 variables are plotted in grey, and those with 200 variables in black. We use squares to identify graphs for formulas with one component and stars for graphs concerning formulas with ten components. Figure 1(g) shows that when the number of variables grows the phase transition moves to the left, and the transition becomes sharper. By Theorem 1, we expect that the bounds on (un)satisfiability do not depend on t, indeed when the number of variables grows the right shift due to an increase in the number of components is compensated, and becomes negligible. Our experiments also confirm that hardness grows with both the number of components and the number of variables. This is seen in Figure 1(g) in the bottom, which plots the average number of choices taken by CLASP (we consider choices since execution times are negligible). Note that CNF formulas with 100 variables and 10 components are already harder than formulas with 200 variables and one component. Figure 1(h) shows the same picture for QBFs in tQ(1, 3, 50, 25, m) (plotted in grey) and t-Q(1, 3, 100, 50, m) (plotted in black), with t ∈ {1, 3}. These results were obtained by running CLASP on the corresponding programs.

Impact on SAT Solving. A desirable property of a random model is to generate instances that behave similarly to real-world ones [Kautz and Selman, 2003; Ans´otegui et al., 2009]. This similarity has been measured empirically by comparing the performance of solvers for random and industrial instances. Following [Ans´otegui et al., 2009], we measure the ratio of the execution times of solvers. We compared KCNFS (a well-known SAT solver specialized in random instances) with GLUCOSE and LINGELING (both specialized in real-world instances) to assess whether our model allows to generate instances that are better solved by solvers for realworld instances. In particular, Figure 2(a) shows the results for the model t-C(3, 100,m), while varying the number of components t ∈ {1, 2, 3, 4, 5}. The x-axis gives the ratio of the numbers of clauses and variables (m/100), the y-axis shows GLUCOSE versus KCNFS (top) and LINGELING versus KCNFS (bottom). We observe that, KCNFS is faster (ratios > 1) than both GLUCOSE and LINGELING when t = 1, i.e., when our model coincides with the classical one for random formulas. Once we increase the number of components the result is reverted, GLUCOSE and LINGELING are faster than KCNFS (ratios < 1), and the difference grows significantly with t. This is independent of the clauses/variables ratio.

The difference between random and real-world instances is often attributed to the presence of some hidden structure in the latter [Ans´otegui et al., 2009]. We observed that multicomponent models yield instances that are solved faster by solvers designed for real-world instances. We conjecture this is due to the component structure introduced by the model. This structure can be controlled by varying the number of components, yielding instances of varying hardness.

Impact on QBF and ASP Solving. An analysis distinguishing the behavior of random and industrial instances is not possible for ASP and QBF solvers. Indeed, no QBF/ASP solvers have ever been designated as (or known to be) specialized to random instances in ASP and QBF Evaluations so far (cf. [Calimeri et al., 2016; Narizzano et al., 2006] and http://www.qbflib.org). Nonetheless our model has other interesting implications for QBF and ASP solvers.

To assess the validity of our model for QBF, we submitted several instances to the QBF Evaluation 2016. All our instances (with n = 100 only, and t ≤ 6) were classified as hard by the organizers, and helped identify a bug in one of the participating solvers, demonstrating the efficacy of our model in performance analysis and in correctness testing.

For ASP solvers, Figure 2(b) outlines the impact of our model on answer set search for programs corresponding to QBF formulas t-Q(1, 3, 24, 12,m) with t ∈ {1, 3, 5, 7, 9, 11}. ASP solvers evaluate disjunctive programs by first computing a candidate model, and then checking its stability (the latter task is co-NP complete). Thus, we plot (i) the ratio between the number of choices made during the search phase and the number of stable model checks performed by WASP and CLASP, and (ii) the ratio between the time spent in stable model checking and the total execution time for the solver WASP (results for CLASP are analogous) both for growing t. The ratio between the numbers of choices and model checks decreases when the number of components grows, following a similar behavior for both solvers. This is a machineindependent measure of the impact of the two activities, and we observe that the role of the model checker grows with t. Specifically, the impact of the model checking on the total solving time grows from about about 3% (t = 1) to 88% (t = 11). It is known that, on available benchmarks, ASP solvers spend more time in the model search phase than in the model checking phase (this also happens when t = 1). However, our model allows to generate in a controllable way instances that put emphasis also the model checking phase.

6 Conclusions

In this paper we proposed the multi-component models for random propositional formulas, and disjunctive logic programs. Despite their simple structure the models have theoretical and empirical properties that make them important for further advancement of the SAT, QBF and ASP solvers. First, the hardness of formulas/programs can be controlled and, unlike in the earlier models, not only in terms of the ratio of clauses to variables. Our experiments showed that the hardness strongly depends on the number of components, and even a small number of components can lead to very hard instances. Further, the multi-component model generates formulas that in at least one aspect are similar to instances arising in practice: they are solved better by solvers specialized in industrial benchmarks than by solvers specialized in random ones. This makes them useful for development and testing of solvers intended for practical applications. Finally, our model of random disjunctive programs is the first model for that class of logic objects. This and the fact that it allows us to control the role of the stable model checking phase point to its potential for the development of ASP solvers.

Acknowledgments

This work was partially supported by the Italian Ministry MISE under projects "PIUCultura" (n. F/020016/0102/X27), and "Smarter Solutions in the Big Data World" (PON 2014-2020), and by EPSRC grant N023056.