Verification Of Partial Quantifier Elimination

A high-level view of $\mathit{VerPQE}$ is given in Fig. 1. $\mathit{VerPQE}$ accepts formula $\exists{X}[F]$, a subset $G\in F$ of clauses to take out of the scope of quantifiers and a solution $H$ to this PQE problem. That is $\exists{X}[F]$ is supposed to be logically equivalent to $H\wedge\mbox{$\exists{X}[F\setminus G]$}$. $\mathit{VerPQE}$ returns true if this equivalence holds and so, $H$ is a correct solution. Otherwise, $\mathit{VerPQE}$ returns false.

$\mathit{VerPQE}$ consists of two parts separated by a solid line. In the first part (lines 1-4), $\mathit{VerPQE}$ just checks if $H$ is implied by $F$. This is done by checking for every clause $C\in H$ if $F\wedge\overline{C}$ is satisfiable. If so, $C$ is not implied by $F$ and the solution $H$ is incorrect. Hence, $\mathit{VerPQE}$ returns false (line 4). In the second part (lines 5-9), for every clause $C\in G$, the algorithm checks if $C$ is redundant in $\exists{X}[F\wedge H]$ by calling the function $\mathit{ChkRed}$ (line 6). Namely, $\mathit{ChkRed}$ checks if $\mbox{$\exists{X}[F\wedge H]$}\equiv\mbox{$\exists{X}[(F\setminus\mbox{$\{C\}$})\wedge H]$}$. If so, $C$ is removed from $F$ (line 8). Otherwise, $C$ is not redundant in $\exists{X}[F\wedge H]$ and $\mathit{VerPQE}$ returns false (line 7). If all clauses of $G$ can be removed from $\exists{X}[F\wedge H]$, then $H$ is a correct solution and $\mathit{VerPQE}$ returns true.

The pseudocode of $\mathit{ChkRed}$ is shown in Fig. 2. $\mathit{ChkRed}$ accepts the formula $\exists{X}[F(X,Y)\wedge H(Y)]$ and a quantified clause $C$ to be checked for redundancy. $\mathit{ChkRed}$ returns true if $C$ is redundant in $\exists{X}[F\wedge H]$. Otherwise, it returns false. To verify redundancy of $C$, $\mathit{ChkRed}$ checks if $F\wedge H$ has a $Y$-removable $C$-boundary point. If not, $C$ is redundant. Otherwise, $C$ is not redundant.

$\mathit{ChkRed}$ starts with computing the set $Y$ of unquantified variables (line 1). Then it initializes the set of “plugging” clauses (see below). The main work is done in the while loop (lines 3-12). $\mathit{ChkRed}$ starts with checking if formula $F\wedge H$ has a $C$-boundary point (lines 4-5) i.e. checking if there is an assignment ($\vv{x}$,$\vv{y}$) satisfying $\mathit{Plg}\wedge(F\setminus\mbox{$\{C\}$})\wedge H\wedge\overline{C}$. The formula Plg is used here to exclude the $C$-boundary points examined in the previous iterations of the loop. If no ($\vv{x}$,$\vv{y}$) exists, the clause $C$ is redundant and $\mathit{ChkRed}$ returns true (line 7).

If the assignment ($\vv{x}$,$\vv{y}$) above exists, $\mathit{ChkRed}$ checks if formula $\mbox{$F_{\vec{y}}$}\wedge\mbox{$H_{\vec{y}}$}$ is satisfiable i.e. whether $F\wedge H$ is satisfiable in subspace $\vv{y}$ (lines 8-10). If not, the $C$-boundary point ($\vv{x}$,$\vv{y}$) is $Y$-removable. This means that $C$ is not redundant in $\exists{X}[F\wedge H]$ and $\mathit{ChkRed}$ returns false (line 10). Otherwise, ($\vv{x}$,$\vv{y}$) is a $Y$-unremovable boundary point and $\mathit{ChkRed}$ calls the function PlugCls to build a plugging clause $D(Y)$. The latter is falsified by $\vv{y}$ and so excludes re-examining $C$-boundary points in the subspace $\vv{y}$. After that, $\mathit{ChkRed}$ adds $D$ to the formula Plg and starts a new iteration of the loop.

The simplest way to build $D$ is to form the longest clause falsified by $\vv{y}$. One can try to make $D$ shorter to exclude a greater subspace from future considerations. Suppose there is $\mbox{$\vv{y}$}^{*}\subset\mbox{$\vv{y}$}$ such that the assignment $\mbox{$\vv{x}$}^{*}$ satisfying $\mbox{$F_{\vec{y}}$}\wedge\mbox{$H_{\vec{y}}$}$ (found in line 8) still satisfies $F_{\vec{y}^{*}}\wedge H_{\vec{y}^{*}}$. This means that every $C$-boundary point of the larger subspace $\mbox{$\vv{y}$}^{*}$ is $Y$-unremovable too. So, one can add to Plg a shorter plugging clause $D$ falsified by $\mbox{$\vv{y}$}^{*}$ rather than $\vv{y}$.

As we mentioned earlier, $\mathit{VerPQE}$ consists of two parts. The first part of $\mathit{VerPQE}$ checks if every clause of the solution $H$ is implied by $F$. In the second part, for every clause $C\in G$, the function $\mathit{ChkRed}$ checks if $C$ is redundant in $\exists{X}[F\wedge H]$. (Recall that $G$ is the subset of clauses that one must take out of $\exists{X}[F]$.) The first part reduces to $|H|$ calls to a SAT-solver. So, it is as scalable as SAT-solving (unless $H$ blows up as the size of the PQE problem grows). The second part of $\mathit{VerPQE}$ scales much poorer. The reason is that this part requires enumeration of $Y$-unremovable $C$-boundary points and the number of such points is typically grows exponentially. Besides, the plugging clauses produced by $\mathit{ChkRed}$ are long. So, adding a plugging clause cannot exclude a big chunk of $C$-boundary points at once. So, the size of formulas that can be efficiently handled by $\mathit{VerPQE}$ is limited by 70-80 variables.

There is however an important case where $\mathit{VerPQE}$ can efficiently verify large formulas. This is the case where $F\wedge H$ does not have any $Y$-unremovable $G$-boundary points. (Since $F$ and $F\wedge H$ have the same $Y$-unremovable $G$-boundary points, this means that $F$ has no such boundary points either.) Then for every clause $C\in G$, the function $\mathit{ChkRed}$ immediately finds out that the formula $(F\setminus\mbox{$\{C\}$})\wedge H\wedge\overline{C}$ is unsatisfiable. So, the verification of solution $H$ reduces to $|H|+|G|$ SAT-checks.

In this subsection, we consider the PQE problems of taking $C$ out of $\exists{X}[F(X,Y)]$ where all $C$-boundary points of $F$ are $Y$-removable. In [5], we generated 3,736 of such formulas. In Table 1, we give a sample of 7 formulas. The first column of the table gives the name of the circuit of the HWMCC-13 set used to generate the PQE problem. (The real names of circuits exmp1, exmp2 and examp3 in the HWMCC-13 set are mentorbm1, bob12m08m, and bob12m03m respectively.)

The second and third co-lumns give the number of clauses and variables of formula $F$. The fourth column shows the size of the set $Y$ i.e. the number of unquantified variables in $\exists{X}[F(X,Y)]$. The next column gives the number of clauses in the solution $H$ found by $\mathit{EG}$-$\mathit{PQE}^{+}$. The last two columns show the time taken by $\mathit{EG}$-$\mathit{PQE}^{+}$ and $\mathit{VerPQE}$ (in seconds) to finish the PQE problem and verify the solution. As we mentioned in Subsection 4.3, if all $C$-boundary points of $F$ are $Y$-removable the same applies to formula $F\wedge H$. So, $\mathit{VerPQE}$ should be very efficient even for large formulas. Table 1 substantiates this intuition.

Here we consider the same PQE problems as in the previous subsection. The only difference is that the formula $F$ contains $C$-boundary points that are $Y$-unremovable. In [5], we generated 3,094 of such formulas. In Table 2, we give a sample of 7 formulas. The name and meaning of each column is the same as in Table 1.

Table 2 shows that $\mathit{VerPQE}$ failed to verify 6 out of 7 solutions in the time limit of 600 sec. whereas the corresponding problems were easily solved by $\mathit{EG}$-$\mathit{PQE}^{+}$. (The reason is that $\mathit{EG}$-$\mathit{PQE}^{+}$ uses a more powerful technique of proving redundancy of $C$ than plugging unremovable boundary points as $\mathit{VerPQE}$ does.) So, solutions $H$ obtained for large formulas $\exists{X}[F]$ where $F$ has a lot of unremovable boundary points cannot be efficiently verified by $\mathit{VerPQE}$.

In this subsection, we continue consider formulas with $Y$-unremovable $C$-boundary points. Only, in contrast to the previous subsection, here we consider small random formulas. In this experiment we verified solutions obtained for formulas whose number of variables ranged from 70 to 85. To get more reliable data, for each size we generated 100 random PQE problems and computed the average result. For each example, the formula $F$ had 20% of two-literal and 80% of three-literal clauses.

The results of this experiment are shown in Table 3. Let us explain the meaning of each column of this table using its first line. The first column indicates that we generated 100 PQE problems of the same size shown in the next three columns. That is for all 100 problems corresponding to the first line of Table 3 the number of clauses, variables and the size of the set $Y$ was 140, 70 and 35 respectively. The last three columns of the first line show the average results over 100 examples. For instance, the first column of the three says that the average size of the solution $H$ found by $\mathit{EG}$-$\mathit{PQE}^{+}$ was 28 clauses. Table 3 shows that the performance of $\mathit{VerPQE}$ drastically drops as the number of variables grows due to the exponential blow-up of the set of $Y$-unremovable $C$-boundary points.