The construction of \(\Pi _2 = (\mathcal {A}, \mathcal {E}, \mathcal {R}_2)\)  differs from \(\Pi _1\)  in
only one respect: for \(\Pi _2\) , \(\ell ^*\)  converts literals into \(\top \) . Note
that, therefore, \(\Pi _2\)  contains the fact \({\mathit {sat}}\) . This completes
the main part of our construction. Let us now explore how our construction
works. From [1]}, we have that program \(\Pi _1\)  has a CWV iff the
3-QBF \(\exists {\mathbf {X}}\forall {\mathbf {Y}}\exists {\mathbf {Z}}\Psi \)  is satisfiable, and
hence, conversely, \(\Pi _1\)  has no CWVs iff the QBF is unsatisfiable (since, in
this case, in the GL-reduct, the atom \({\mathit {sat}}\)  is always derived, and
hence, constraint (REF ) destroys any potential CWV). Note that any
CWV \(\mathcal {M}\)  for \(\Pi _1\)  has the following structure: a guess \(\Phi \)  leading to
\(\mathcal {M}\)  will contain a subset of \(\lbrace  \mathbf {not}\,x, \mathbf {not}\,\overline{x} \mid x \in {\mathbf {X}}\rbrace \)  representing an assignment on the variables of \({\mathbf {X}}\) . Further,
\(\Phi \supseteq \lbrace  \mathbf {not}\,y, \mathbf {not}\,\overline{y} \mid y \in {\mathbf {Y}}\rbrace \) , since
each answer set in the CWV represents precisely one assignment on the
variables \({\mathbf {Y}}\) , and all possible such assignments must appear in the CWV.
Finally, \(\mathbf {not}\,{\mathit {false}} \in \Phi \)  and \(\mathbf {not}\,\lnot {\mathit {sat}}\notin \Phi \) , via constraint (REF ). For the precise reasoning behind
this construction, please see [1]}.
