Partial Quantifier Elimination And Property Generation

One generates properties by PQE until an unwanted property exposing a bug is produced. (Like in testing one runs tests until a bug-exposing test is encountered.) The benefit of property generation by PQE is fourfold. First, by property generation one can identify bugs that are hard or simply impossible to find by testing. Second, using PQE makes property generation efficient. Third, by taking out different clauses one can generate properties covering different parts of the design. This increases the probability of discovering a bug. Fourth, every property generated by PQE specifies a large set of high-quality tests.

In this paper (Sections 7, 9), we consider cases where identifying an unwanted property is easy. However, in general, such identification is not trivial. A detailed discussion of this topic is beyond the scope of this paper. (Nevertheless, in Appendix 0.D, we give the main idea of the procedure for deciding if a property is unwanted.)

The behavior of $M$ corresponding to a single test can be cast as a property. Let $w_{i}\in W$ be an output variable of $M$ and $\vv{v}$ be a test, i.e., a full assignment to the input variables $V$ of $M$. Let $B^{\vec{v}}$ denote the longest clause falsified by $\vv{v}$, i.e., $\mbox{$\mathit{Vars}(\mbox{$B^{\vec{v}}$})$}=V$. Let $l(w_{i})$ be the literal satisfied by the value of $w_{i}$ produced by $M$ under input $\vv{v}$. Then the clause $\mbox{$B^{\vec{v}}$}\vee l(w_{i})$ is satisfied by every assignment satisfying $F$, i.e., $\mbox{$B^{\vec{v}}$}\vee l(w_{i})$ is a property of $M$. We will refer to it as a single-test property (since it describes the behavior of $M$ for a single test). If the input $\vv{v}$ is supposed to produce the opposite value of $w_{i}$ (i.e., the one falsifying $l(w_{i})$), then $\vv{v}$ exposes a bug in $M$. In this case, the single-test property above is an unwanted property of $M$ exposing the same bug as the test $\vv{v}$.

A single-test property can be viewed as a weakest property of $M$ as opposed to the strongest property specified by $\exists{X}[F]$. The latter is the truth table of $M$ that can be computed explicitly by performing QE on $\exists{X}[F]$. One can use PQE to generate properties of $M$ that, in terms of strength, range from the weakest ones to the strongest property inclusively. (By combining clause splitting with PQE one can generate single-test properties, see the next subsection.) Consider the PQE problem of taking a clause $C$ out of $\exists{X}[F]$. Let $H(V,W)$ be a solution to this problem, i.e., $\mbox{$\exists{X}[F]$}\equiv H\wedge\mbox{$\exists{X}[F\setminus\mbox{$\{C\}$}]$}$. Since $H$ is implied by $F$, it can be viewed as a property of $M$. If $H$ is an unwanted property, $M$ has a bug. (Here we consider the case where a property of $M$ is obtained by taking a clause out of formula $\exists{X}[F]$ where only the internal variables of $M$ are quantified. Later we consider cases where some external variables of $M$ are quantified too.)

We will assume that the property $H$ generated by PQE has no redundant clauses (see Remark 1). That is, if $D\in H$, then $F\setminus\mbox{$\{C\}$}\not\Rightarrow D$. Then one can view $H$ as a property that holds due to the presence of the clause $C$ in $F$.

If a property $H$ is obtained by taking only one clause out of $\exists{X}[F]$, its computation is much easier than performing QE on $\exists{X}[F]$. If computing $H$ still remains too time-consuming, one can use the two methods below that achieve better performance at the expense of generating weaker properties. The first method applies when a PQE solver forms a solution incrementally, clause by clause (like the algorithms described in Sections 5 and 6). Then one can simply stop computing $H$ as soon as the number of clauses in $H$ exceeds a threshold. Such a formula $H$ is still implied by $F$ and hence specifies a property of $M$.

The second method employs clause splitting. Here we consider clause splitting on input variables $v_{1},\dots,v_{p}$, i.e., those of $V$ (but one can split a clause on any subset of variables from $\mathit{Vars}(F)$). Let $F^{\prime}$ denote the formula $F$ where a clause $C$ is replaced with $p+1$ clauses: $C_{1}=C\vee\overline{l(v_{1})}$,…, $C_{p}=C\vee\overline{l(v_{p})}$, $C_{p+1}=C\vee l(v_{1})\vee\dots\vee l(v_{p})$, where $l(v_{i})$ is a literal of $v_{i}$. The idea is to obtain a property $H$ by taking the clause $C_{p+1}$ out of $\exists{X}[F^{\prime}]$ rather than $C$ out of $\exists{X}[F]$. The former PQE problem is simpler than the latter since it produces a weaker property $H$. One can show that if $\mbox{$\{v_{1},\dots,v_{p}\}$}\!=\!V$, then a) the complexity of PQE reduces to linear; b) taking out $C_{p+1}$ actually produces a single-test property. The latter specifies the input/output behavior of $M$ for the test $\vv{v}$ falsifying the literals $l(v_{1}),\dots,l(v_{p})$. (See Appendix 0.E for more details.)

Arguably, testing is so effective in practice because one verifies a particular design. Namely, one probes different parts of this design using some coverage metric rather than sampling the truth table (which would mean verifying every possible design). The same idea works for property generation by PQE for the following two reasons. First, by taking out a clause, PQE generates a property inherent to the specific circuit $M$. (If one replaces $M$ with an equivalent but structurally different circuit, PQE will generate different properties.) Second, by taking out different clauses of $F$ one generates properties corresponding to different parts of $M$ thus “covering” the design. This increases the chance to take out a clause corresponding to the buggy part of $M$ and generate an unwanted property.

In this subsection, we show that a property $H$ generated by PQE, in general, specifies a large set of high-quality tests. Let $H(V,W)$ be obtained by taking $C$ out of $\exists{X}[F(X,V,W)]$. Let $Q(V,W)$ be a clause of $H$. As mentioned above, we assume that $F\setminus\mbox{$\{C\}$}\not\Rightarrow Q$. Then there is an assignment ($\vv{x}$,$\vv{v}$,$\vv{w}$) satisfying formula $(F\setminus\mbox{$\{C\}$})\wedge\overline{Q}$ where $\vv{x}$,$\vv{v}$,$\vv{w}$ are assignments to $X,V,W$ respectively. (Note that by definition, ($\vv{v}$,$\vv{w}$) falsifies $Q$.) Let $(\mbox{$\vv{x}$}^{*},\mbox{$\vv{v}$},\mbox{$\vv{w}$}^{*})$ be the execution trace of $M$ under the input $\vv{v}$. So, $(\mbox{$\vv{x}$}^{*},\mbox{$\vv{v}$},\mbox{$\vv{w}$}^{*})$ satisfies $F$. Note that the output assignments $\vv{w}$ and $\mbox{$\vv{w}$}^{*}$ must be different because $(\mbox{$\vv{v}$},\mbox{$\vv{w}$}^{*})$ has to satisfy $Q$. (Otherwise, $(\mbox{$\vv{x}$}^{*},\mbox{$\vv{v}$},\mbox{$\vv{w}$}^{*})$ satisfies $F\wedge\overline{Q}$ and so $F\not\Rightarrow Q$ and hence $F\not\Rightarrow H$.) So, one can view $\vv{v}$ as a test “detecting” disappearance of the clause $C$ from $F$. Note that different assignments satisfying $(F\setminus\mbox{$\{C\}$})\wedge\overline{Q}$ correspond to different tests $\vv{v}$. So, the clause $Q$ of $H$, in general, specifies a very large number of tests. One can show that these tests are similar to those detecting stuck-at faults and so have very high quality (see Appendix 0.F for more details).

Let $N$ be a sequential circuit and $S$ denote the state variables of $N$. Let $I(S)$ specify the initial state $\vv{s}\!_{\mathit{ini}}$ (i.e., $I(\mbox{$\vv{s}\!_{\mathit{ini}}$})\!=\!1$). Let $T(S^{\prime},V,S^{\prime\prime})$ denote the transition relation of $N$ where $S^{\prime},S^{\prime\prime}$ are the present and next state variables and $V$ specifies the (combinational) input variables. We will say that a state $\vv{s}$ of $N$ is reachable if there is an execution trace leading to $\vv{s}$. That is, there is a sequence of states $\mbox{$\vv{s_{0}}$},\dots,\mbox{$\vv{s_{k}}$}$ where $\mbox{$\vv{s_{0}}$}=\mbox{$\vv{s}\!_{\mathit{ini}}$}$, $\mbox{$\vv{s}\!_{k}$}\!=\!\mbox{$\vv{s}$}$ and there exist $\vv{v}\!_{i}$ $i=0,\dots,k\!-\!1$ for which $T(\mbox{$\vv{s}\!_{i}$},\mbox{$\vv{v}\!_{i}$},\mbox{$\vv{s}\!_{i+1}$})=1$. Let $N$ have to satisfy a set of invariants $P_{0}(S),\dots,P_{m}(S)$. That is, $P_{i}$ holds iff $P_{i}(\mbox{$\vv{s}$})=1$ for every reachable state $\vv{s}$ of $N$. We will denote the aggregate invariant $P_{0}\wedge\dots\wedge P_{m}$ as $\mathit{P}_{\mathit{agg}}$. We will call $\vv{s}$ a bad state of $N$ if $\mbox{$\mathit{P}_{\mathit{agg}}$}(\mbox{$\vv{s}$})=0$. If $\mathit{P}_{\mathit{agg}}$ holds, no bad state is reachable. We will call $\vv{s}$ a good state of $N$ if $\mbox{$\mathit{P}_{\mathit{agg}}$}(\mbox{$\vv{s}$})=1$.

Typically, the set of invariants $P_{0},\dots,P_{m}$ is incomplete in the sense that it does not specify all states that must be unreachable. So, a good state can well be unreachable. We will call a good state operative (or op-state for short) if it is supposed to be used by $N$ and so should be reachable. We introduce the term an operative state just to factor out “useless” good states. We will say that $N$ has an op-state reachability bug if an op-state is unreachable in $N$. In Section 7, we consider such a bug in a FIFO buffer. The fact that $\mathit{P}_{\mathit{agg}}$ holds says nothing about reachability of op-states. Consider, for instance, a trivial circuit $\mathit{N}_{\mathit{triv}}$ that simply stays in the initial state $\vv{s}\!_{\mathit{ini}}$ and $\mbox{$\mathit{P}_{\mathit{agg}}$}(\mbox{$\vv{s}\!_{\mathit{ini}}$})=1$. Then $\mathit{P}_{\mathit{agg}}$ holds for $\mathit{N}_{\mathit{triv}}$ but the latter has op-state reachability bugs (assuming that the correct circuit must reach states other than $\vv{s}\!_{\mathit{ini}}$).

Let $R_{\vv{s}}(S)$ be the predicate satisfied only by a state $\vv{s}$. In terms of CTL, identifying an op-state reachability bug means finding $\vv{s}$ for which the property $EF.R_{\vv{s}}$ must hold but it does not. The reason for assuming $\vv{s}$ to be unknown is that the set of op-states is typically too large to explicitly specify every property $ET.R_{\vv{s}}$ to hold. This makes finding op-state reachability bugs very hard. The problem is exacerbated by the fact that reachability of different states is established by different traces. So, in general, one cannot efficiently prove many properties $EF.R_{\vv{s}}$ (for different states) at once.

In practice, there are two methods to check reachability of operative states for large circuits. The first method is testing. Of course, testing cannot prove a state unreachable, however, the examination of execution traces may point to a potential problem. (For instance, after examining execution traces of the circuit $\mathit{N}_{\mathit{triv}}$ above one realizes that many operative states look unreachable.) The other method is to check unwanted invariants, i.e., those that are supposed to fail. If an unwanted invariant holds for a circuit, the latter has an op-state reachability bug. For instance, one can check if a state variable $s_{i}\in S$ of a circuit never changes its initial value. To break this unwanted invariant, one needs to find an operative state where the initial value of $s_{i}$ is flipped. (For the circuit $\mathit{N}_{\mathit{triv}}$ above this unwanted invariant holds for every state variable.) The potential unwanted invariants are formed manually, i.e., simply guessed.

The two methods above can easily overlook an op-state reachability bug. Testing cannot prove that an op-state is unreachable. To correctly guess an unwanted invariant that holds, one essentially has to know the underlying bug. Below, we describe a method for invariant generation by PQE that is based on property generation for combinational circuits. The appeal of this method is twofold. First, PQE generates invariants “inherent” to the implementation at hand, which drastically reduces the set of invariants to explore. Second, PQE is able to generate invariants related to different parts of the circuit (including the buggy one). This increases the probability of generating an unwanted invariant. We substantiate this intuition in Section 7.

Let formula $F_{k}$ specify the combinational circuit obtained by unfolding a sequential circuit $N$ for $k$ time frames and adding the initial state constraint $I(S_{0})$. That is, $F_{k}=I(S_{0})\wedge T(S_{0},V_{0},S_{1})\wedge\dots\wedge T(S_{k-1},V_{k-1},S_{k})$ where $S_{j},V_{j}$ denote the state and input variables of $j$-th time frame respectively. Let $H(S_{k})$ be a solution to the PQE problem of taking a clause $C$ out of $\exists{\mbox{$X_{k}$}}[F_{k}]$ where $\mbox{$X_{k}$}=S_{0}\cup V_{0}\cup\dots\cup S_{k-1}\cup V_{k-1}$. That is, $\exists{\mbox{$X_{k}$}}[F_{k}]$ $\equiv H\wedge$ $\exists{\mbox{$X_{k}$}}[F_{k}\setminus\mbox{$\{C\}$}]$. Note that in contrast to Section 3, here some external variables of the combinational circuit (namely, the input variables $V_{0},\dots,V_{k-1}$) are quantified too. So, $H$ depends only on state variables of the last time frame. $H$ can be viewed as a local invariant asserting that no state falsifying $H$ can be reached in $k$ transitions.

One can use $H$ to find global invariants (holding for every time frame) as follows. Even if $H$ is only a local invariant, a clause $Q$ of $H$ can be a global invariant. The experiments of Section 8 show that, in general, this is true for many clauses of $H$. (To find out if $Q$ is a global invariant, one can simply run a model checker to see if the property $Q$ holds.) Note that by taking out different clauses of $F_{k}$ one can produce global single-clause invariants $Q$ relating to different parts of $N$. From now on, when we say “an invariant” without a qualifier we mean a global invariant.

Before describing the pseudocode of $\mathit{EG}$-$\mathit{PQE}$, we explain how it solves the PQE problem of Example 1. That is, we consider taking clause $C_{1}$ out of $\exists{X}[F(X,Y)]$ where $F=C_{1}\wedge\dots\wedge C_{4}$, $C_{1}=\overline{x}_{3}\vee x_{4}$, $C_{2}\!=\!y_{1}\!\vee\!x_{3}$, $C_{3}=y_{1}\vee\overline{x}_{4}$, $C_{4}\!=\!y_{2}\!\vee\!x_{4}$ and $Y=\mbox{$\{y_{1},y_{2}\}$}$ and $X=\mbox{$\{x_{3},x_{4}\}$}$.

$\mathit{EG}$-$\mathit{PQE}$ iteratively generates a full assignment $\vv{y}$ to $Y$ and checks if $(C_{1})_{\vec{y}}$ is redundant in $\exists{X}[\mbox{$F_{\vec{y}}$}]$ (i.e., if $C_{1}$ is redundant in $\exists{X}[F]$ in subspace $\vv{y}$). Note that if $(F\setminus\mbox{$\{C_{1}\}$})_{\vec{y}}$ implies $(C_{1})_{\vec{y}}$, then $(C_{1})_{\vec{y}}$ is trivially redundant in $\exists{X}[\mbox{$F_{\vec{y}}$}]$. To avoid such subspaces, $\mathit{EG}$-$\mathit{PQE}$ generates $\vv{y}$ by searching for an assignment ($\vv{y}$,$\vv{x}$) satisfying the formula $(F\setminus\mbox{$\{C_{1}\}$})\wedge\overline{C}_{1}$. (Here $\vv{y}$ and $\vv{x}$ are full assignments to $Y$ and $X$ respectively.) If such ($\vv{y}$,$\vv{x}$) exists, it satisfies $F\setminus\mbox{$\{C_{1}\}$}$ and falsifies $C_{1}$ thus proving that $(F\setminus\mbox{$\{C_{1}\}$})_{\vec{y}}$ does not imply $(C_{1})_{\vec{y}}$.

Assume that $\mathit{EG}$-$\mathit{PQE}$ found an assignment$(y_{1}\!=\!0,y_{2}\!=\!1,x_{3}\!=\!1,x_{4}\!=\!0)$ satisfying $(F\setminus\mbox{$\{C_{1}\}$})\wedge\overline{C}_{1}$. So $\vv{y}$ = $(y_{1}\!=\!0,y_{2}\!=\!1)$. Then $\mathit{EG}$-$\mathit{PQE}$ checks if $F_{\vec{y}}$ is satisfiable. $F_{\vec{y}}$ = $(\overline{x}_{3}\vee x_{4})\wedge x_{3}\wedge\overline{x}_{4}$ and so it is unsatisfiable. This means that $(C_{1})_{\vec{y}}$ is not redundant in $\exists{X}[\mbox{$F_{\vec{y}}$}]$. (Indeed, $(F\setminus\mbox{$\{C_{1}\}$})_{\vec{y}}$ is satisfiable. So, removing $C_{1}$ makes $F$ satisfiable in subspace $\vv{y}$.) $\mathit{EG}$-$\mathit{PQE}$ makes $(C_{1})_{\vec{y}}$ redundant in $\exists{X}[\mbox{$F_{\vec{y}}$}]$ by adding to $F$ a clause $B$ falsified by $\vv{y}$. The clause $B$ equals $y_{1}$ and is obtained by identifying the assignments to individual variables of $Y$ that made $F_{\vec{y}}$ unsatisfiable. (In our case, this is the assignment $y_{1}=0$.) Note that derivation of clause $y_{1}$ generalizes the proof of unsatisfiability of $F$ in subspace $(y_{1}\!=\!0,y_{2}\!=\!1)$ so that this proof holds for subspace $(y_{1}\!=\!0,y_{2}\!=\!0)$ too.

Now $\mathit{EG}$-$\mathit{PQE}$ looks for a new assignment satisfying $(F\setminus\mbox{$\{C_{1}\}$})\wedge\overline{C}_{1}$. Let the assignment $(y_{1}=1,y_{2}=1,x_{3}=1,x_{4}=0)$ be found. So, $\vv{y}$ = $(y_{1}\!=\!1,y_{2}\!=\!1)$. Since $(y_{1}\!=\!1,y_{2}\!=\!1,x_{3}=0)$ satisfies $F$, the formula $F_{\vec{y}}$ is satisfiable. So, $(C_{1})_{\vec{y}}$ is already redundant in $\exists{X}[\mbox{$F_{\vec{y}}$}]$. To avoid re-visiting the subspace $\vv{y}$, $\mathit{EG}$-$\mathit{PQE}$ generates the plugging clause $D=\overline{y}_{1}\vee\overline{y}_{2}$ falsified by $\vv{y}$.

$\mathit{EG}$-$\mathit{PQE}$ fails to generate a new assignment $\vv{y}$ because the formula$D\wedge(F\setminus\mbox{$\{C_{1}\}$})\wedge\overline{C}_{1}$ is unsatisfiable. Indeed, every full assignment $\vv{y}$ we have examined so far falsifies either the clause $y_{1}$ added to $F$ or the plugging clause $D$. The only assignment $\mathit{EG}$-$\mathit{PQE}$ has not explored yet is $\mbox{$\vv{y}$}\!=\!(y_{1}\!=\!1,y_{2}\!=\!0)$. Since $\mbox{$(F\setminus\mbox{$\{C_{1}\}$})_{\vec{y}}$}=x_{4}$ and $(C_{1})_{\vec{y}}$ = $\overline{x}_{3}\vee x_{4}$, the formula $(F\setminus\mbox{$\{C_{1}\}$})\wedge\overline{C}_{1}$ is unsatisfiable in subspace $\vv{y}$. In other words,$(C_{1})_{\vec{y}}$ is implied by $(F\setminus\mbox{$\{C_{1}\}$})_{\vec{y}}$ and hence is redundant. Thus, $C_{1}$ is redundant in $\exists{X}[\mbox{$\mathit{F}_{\mathit{ini}}$}\wedge y_{1}]$ for every assignment to $Y$ where $\mathit{F}_{\mathit{ini}}$ is the initial formula $F$. That is, $\exists{X}[\mbox{$\mathit{F}_{\mathit{ini}}$}]$ $\equiv y_{1}\wedge$ $\exists{X}[\mbox{$\mathit{F}_{\mathit{ini}}$}\setminus\mbox{$\{C_{1}\}$}]$ and so the clause $y_{1}$ is a solution $H$ to our PQE problem.

The pseudo-code of $\mathit{EG}$-$\mathit{PQE}$ is shown in Fig. 1. $\mathit{EG}$-$\mathit{PQE}$ starts with storing the initial formula $F$ and initializing formula $\mathit{Plg}$ that accumulates the plugging clauses generated by $\mathit{EG}$-$\mathit{PQE}$ (line 1). As we mentioned in the previous subsection, plugging clauses are used to avoid re-visiting the subspaces where the formula $F$ is proved satisfiable.

All the work is carried out in a while loop. First, $\mathit{EG}$-$\mathit{PQE}$ checks if there is a new subspace $\vv{y}$ where $\exists{X}[\mbox{$(F\setminus\mbox{$\{C\}$})_{\vec{y}}$}]$ does not imply $F_{\vec{y}}$. This is done by searching for an assignment ($\vv{y}$,$\vv{x}$) satisfying $\mbox{$\mathit{Plg}$}\wedge(F\setminus\mbox{$\{C\}$})\wedge\overline{C}$ (lines 3-4). If such an assignment does not exist, the clause $C$ is redundant in $\exists{X}[F]$. (Indeed, let $\vv{y}$ be a full assignment to $Y$. The formula $\mbox{$\mathit{Plg}$}\wedge(F\setminus\mbox{$\{C\}$})\wedge\overline{C}$ is unsatisfiable in subspace $\vv{y}$ for one of the two reasons. First, $\vv{y}$ falsifies $\mathit{Plg}$. Then $C_{\vec{y}}$ is redundant because $F_{\vec{y}}$ is satisfiable. Second, $\mbox{$(F\setminus\mbox{$\{C\}$})_{\vec{y}}$}\wedge\overline{\mbox{$C_{\vec{y}}$}}$ is unsatisfiable. In this case, $(F\setminus\mbox{$\{C\}$})_{\vec{y}}$ implies $C_{\vec{y}}$.) Then $\mathit{EG}$-$\mathit{PQE}$ returns the set of clauses added to the initial formula $F$ as a solution $H$ to the PQE problem (lines 5-6).

If the satisfying assignment ($\vv{y}$,$\vv{x}$) above exists, $\mathit{EG}$-$\mathit{PQE}$ checks if the formula $F_{\vec{y}}$ is satisfiable (line 7). If not, then the clause $C_{\vec{y}}$ is not redundant in $\exists{X}[\mbox{$F_{\vec{y}}$}]$ (because $(F\setminus\mbox{$\{C\}$})_{\vec{y}}$ is satisfiable). So, $\mathit{EG}$-$\mathit{PQE}$ makes $C_{\vec{y}}$ redundant by generating a clause $B(Y)$ falsified by $\vv{y}$ and adding it to $F$ (line 9). Note that adding $B$ also prevents $\mathit{EG}$-$\mathit{PQE}$ from re-visiting the subspace $\vv{y}$ again. The clause $B$ is built by finding an unsatisfiable subset of $F_{\vec{y}}$ and collecting the literals of $Y$ removed from clauses of this subset when obtaining $F_{\vec{y}}$ from $F$.

If $F_{\vec{y}}$ is satisfiable, $\mathit{EG}$-$\mathit{PQE}$ generates an assignment $\mbox{$\vv{x}$}^{*}$ to $X$ such that $(\mbox{$\vv{y}$},\mbox{$\vv{x}$}^{*})$ satisfies $F$ (line 7). The satisfiability of $F_{\vec{y}}$ means that every clause of $F_{\vec{y}}$ including $C_{\vec{y}}$ is redundant in $\exists{X}[\mbox{$F_{\vec{y}}$}]$. At this point, $\mathit{EG}$-$\mathit{PQE}$ uses the longest clause $D(Y)$ falsified by $\vv{y}$ as a plugging clause (line 11). The clause $D$ is added to $\mathit{Plg}$ to avoid re-visiting subspace $\vv{y}$. Sometimes it is possible to remove variables from $\vv{y}$ to produce a shorter assignment $\mbox{$\vv{y}$}^{*}$ such that $(\mbox{$\vv{y}$}^{*},\mbox{$\vv{x}$}^{*})$ still satisfies $F$. Then one can use a shorter plugging clause $D$ involving only the variables assigned in $\mbox{$\vv{y}$}^{*}$.

$\mathit{EG}$-$\mathit{PQE}$ is similar to the QE algorithm presented at CAV-2002 [11]. We will refer to it as $\mathit{CAV02}$-$\mathit{QE}$. Given a formula $\exists{X}[F(X,Y)]$, $\mathit{CAV02}$-$\mathit{QE}$ enumerates full assignments to $Y$. In subspace $\vv{y}$, if $F_{\vec{y}}$ is unsatisfiable, $\mathit{CAV02}$-$\mathit{QE}$ adds to $F$ a clause falsified by $\vv{y}$. Otherwise, $\mathit{CAV02}$-$\mathit{QE}$ generates a plugging clause $D$. (In [11], $D$ is called “a blocking clause”. This term can be confused with the term “blocked clause” applied to a completely different kind of a clause. So, we use the term “a plugging clause” instead.) To apply the idea of $\mathit{CAV02}$-$\mathit{QE}$ to PQE, we reformulated it in terms of redundancy based reasoning.

The main flaw of $\mathit{EG}$-$\mathit{PQE}$ inherited from $\mathit{CAV02}$-$\mathit{QE}$ is the necessity to use plugging clauses produced from a satisfying assignment. Consider the PQE problem of taking a clause $C$ out of $\exists{X}[F(X,Y)]$. If $F$ is proved unsatisfiable in subspace $\vv{y}$, typically, only a small subset of clauses of $F_{\vec{y}}$ is involved in the proof. Then the clause generated by $\mathit{EG}$-$\mathit{PQE}$ is short and thus proves $C$ redundant in many subspaces different from $\vv{y}$. On the contrary, to prove $F$ satisfiable in subspace $\vv{y}$, every clause of $F$ must be satisfied. So, the plugging clause built off a satisfying assignment includes almost every variable of $Y$. Despite this flaw of $\mathit{EG}$-$\mathit{PQE}$, we present it for two reasons. First, it is a very simple SAT-based algorithm that can be easily implemented. Second, $\mathit{EG}$-$\mathit{PQE}$ has a powerful advantage over $\mathit{CAV02}$-$\mathit{QE}$ since it solves PQE rather than QE. Namely, $\mathit{EG}$-$\mathit{PQE}$ does not need to examine the subspaces $\vv{y}$ where $C$ is implied by $F\setminus\mbox{$\{C\}$}$. Surprisingly, for many formulas this allows $\mathit{EG}$-$\mathit{PQE}$ to completely avoid examining subspaces where $F$ is satisfiable. In this case, $\mathit{EG}$-$\mathit{PQE}$ is very efficient and can solve very large problems. Note that when $\mathit{CAV02}$-$\mathit{QE}$ performs complete QE on $\exists{X}[F]$, it cannot avoid subspaces $\vv{y}$ where $F_{\vec{y}}$ is satisfiable unless $F$ itself is unsatisfiable (which is very rare in practical applications).

The pseudocode of $\mathit{EG}$-$\mathit{PQE}^{+}$ is shown in Fig 2. It is different from that of $\mathit{EG}$-$\mathit{PQE}$ only in line 11 marked with an asterisk. The motivation for this change is as follows. Line 11 describes proving redundancy of $C$ for the case where $C_{\vec{y}}$ is not implied by $(F\setminus\mbox{$\{C\}$})_{\vec{y}}$ and $F_{\vec{y}}$ is satisfiable. Then $\mathit{EG}$-$\mathit{PQE}$ simply uses a satisfying assignment as a proof of redundancy of $C$ in subspace $\vv{y}$. This proof is unnecessarily strong because it proves that every clause of $F$ (including $C$) is redundant in $\exists{X}[F]$ in subspace $\vv{y}$. Such a strong proof is hard to generalize to other subspaces.

The idea of $\mathit{EG}$-$\mathit{PQE}^{+}$ is to generate a proof for a much weaker proposition namely a proof of redundancy of $C$ (and only $C$). Intuitively, such a proof should be easier to generalize. So, $\mathit{EG}$-$\mathit{PQE}^{+}$ calls a procedure PrvClsRed generating such a proof. $\mathit{EG}$-$\mathit{PQE}^{+}$ is a generic algorithm in the sense that any suitable procedure can be employed as PrvClsRed. In our current implementation, the procedure $\mathit{DS}$-$\mathit{PQE}$ [1] is used as PrvClsRed. $\mathit{DS}$-$\mathit{PQE}$ generates a proof stating that $C$ is redundant in $\exists{X}[F]$ in subspace $\mbox{$\vv{y}$}^{*}\subseteq\mbox{$\vv{y}$}$. Then the plugging clause $D$ falsified by $\mbox{$\vv{y}$}^{*}$ is generated. Importantly, $\mbox{$\vv{y}$}^{*}$ can be much shorter than $\vv{y}$. Appendix 0.G gives a brief description of $\mathit{DS}$-$\mathit{PQE}$.