Suite Letz

Download(30 Kb)
Submitter: Letz
Description: Formulas generated according to the pattern \forall x_1 x_3 ... x_{n-1} \exists x_2 x_4 ... x_n (c_1 \and c_n)$ where c_1 = x_1 \and x_2, $c_2 = \not x_1 \and \not x_2, c_3 = x_3 \and x_4, c_4 = \not x_3 \and \not x_4$ , and so on. The instances consists of simple variable-independent subproblems but they should be hard for standard (i.e., without non-chronological backtracking) QBF solvers.
Number of families: 1