Complexity of computing the parity of read-twice opposite CNF formula ($\oplus\text{Rtw-Opp-CNF}$) In a read-twice opposite CNF formula each variable appears twice, once positive and once negative.

I'm interested in the $\oplus\text{Rtw-Opp-CNF}$ problem, which consists in computing the parity of the number of satisfying assignments of a read-twice opposite CNF formula.

I was unable to find any reference about the complexity of such problem. The closest I was able to find is that the counting version $\#\text{Rtw-Opp-CNF}$ is $\#\text{P}$-complete (see section 6.3 in this paper).

Thanks in advance for your help.



Update 10th April 2016


In this paper, the $\oplus\text{Rtw-Opp-SAT}$ problem is shown to be $\oplus\text{P}$-complete, however the formula produced by reduction from $3\text{SAT}$ is not in CNF, and as soon as you try to convert it back into CNF you get a read-thrice formula.
The monotone version $\oplus\text{Rtw-Mon-CNF}$ is shown to be $\oplus\text{P}$-complete in this paper. In such paper, $\oplus\text{Rtw-Opp-CNF}$ is quickly mentioned at the end of section 4: Valiant says it is degenerate. It is not clear to me what being degenerate exactly means, nor what does it imply in terms of hardness.




Update 12th April 2016

It would be also very interesting to know if anyone has ever studied the complexity of the $\Delta\text{Rtw-Opp-CNF}$ problem. Given a read-twice opposite CNF formula, such problem asks to compute the difference between the number of satisfying assignments having an odd number of variables set to true and the number of satisfying assignments having an even number of variables set to true. I've not found any literature about it.



Update 29th May 2016

As pointed out by Emil Jeřábek in his comment, it is not true that Valiant said that the problem $\oplus\text{Rtw-Opp-CNF}$ is degenerate. He only said that a more restricted version of such problem, $\oplus\text{Pl-Rtw-Opp-3CNF}$, is degenerate. In the meanwhile, I continue to not know what degenerate exactly means, but at least now it seems clear that it is a synonym of lack of expressive power.
It turns out that every opposite-read-twice formula has an even number of satisfying assignments. Here's a nice proof of it, though one could probably eliminate the graph-theoretic terminology.

Let $\phi$ be an opposite-read-twice CNF formula. Without loss of generality, no clause contains both a variable and its negation.

Consider the graph $G$ whose vertex set is the clauses of $\phi$, and for each variable $x$, we add an (undirected) edge that is incident on the two clauses containing $x$. Our WLOG assumption in $\phi$ says this graph has no self-loops. Moreover, think of labeling each edge by the variable defining it; this way we can distinguish between parallel edges.

An orientation of $G$ is a directed graph whose edges are formed by assigning a direction to each edge in $G$. Call an orientation of $G$ admissible if every vertex of $G$ has an outgoing edge. It's easy to see that satisfying assignments to $\phi$ are in bijective correspondence with admissible orientations of $G$.

Now I claim that the number of admissible orientations of $G$ is even. The argument is "by involution": I construct a map $\Phi$ with the following properties:


$\Phi$ is totally defined (every admissible orientation is mapped somewhere)
$\Phi$ sends admissible orientations to admissible orientations
$\Phi$ is an involution ($\Phi \circ \Phi$ is the identity)
$\Phi$ has no fixed points


Once these are established, we can observe that the orbits of $\Phi$ have size 2 and partition the admissible orientations of $G$. It follows that the number of admissible orientations is even.

To define $\Phi$, let $\vec{G}$ be an admissible orientation, and consider breaking $\vec{G}$ into it's strongly connected components. $\Phi$ then sends $\vec{G}$ to the orientation formed by reversing all the edges within the strongly connected components. The properties are then straightforwardly checked:


Every directed graph can be partitioned into strongly connected components.
Consider the "DAG of strongly connected components" in $\vec G$; call it the quotient graph. Note that $\Phi(\vec G)$ will have the same quotient structure, since $\Phi$ doesn't affect the edges between SCCs, and strongly connected graphs remain strongly connected when reversing all their edges. Additionally, if a SCC has more than one vertex, then all its constituent vertices have an incoming edge. If an SCC has just a single vertex and isn't a source in the quotient, then all its constituent vertices have an incoming edge. So to show $\Phi(\vec G)$ is admissible, it suffices to show that the SCCs which are sources in the quotient have multiple vertices. But this follows by the fact that every vertex in the component has an incoming edge, which must come from another vertex in the component since $G$ has no self-loops and the component is a source in the quotient.
This follows from the fact that the quotient structure of $\Phi(\vec G)$ coincides with the quotient structure of $\vec G$.
By admissibility, $\vec G$ has a cycle, and hence some SCC with an edge inside it.