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.

  • $\begingroup$ ⊕Rtw-Opp-CNF is as hard as ⊕Rtw-Mon-CNF. You can build the negation gadget: (i0 v x0 v x1)(x1 v x2)(i1 v x0 v x2) . If i0 = i1, then weight = 0 (in modulo 2). Otherwise weight = 1. $\endgroup$
    – user39044
    May 19 '16 at 7:37
  • $\begingroup$ I cannot find reduction from ⊕Rtw-Mon-CNF to ⊕Rtw-Opp-CNF, but I found polynomial algorithm for solving ⊕Rtw-Opp-CNF. So ⊕Rtw-Opp-CNF is simpler. $\endgroup$
    – user39044
    May 19 '16 at 11:40
  • $\begingroup$ I can't find a mention of ⊕Rtw-Opp-CNF in Valiant's paper. He claims that ⊕Pl-Rtw-Opp-3CNF is "degenerate", but that involves several additional restrictions. $\endgroup$ May 20 '16 at 8:35
  • $\begingroup$ @EmilJeřábek: You are definitely right. I was misleaded by my ignorance of the meaning of "degenerate", and I applied the same sort of reasoning that is normally applied in presence of completeness results: if a certain problem is complete for some class, removing restrictions from it obviously preserves completeness. Even if I still do not know what "degenerate" exactly means, it is at least clear to me now that such term is somehow a synonym of weakness (i.e. lack of expressive power), hence the aforementioned reasoning cannot be applied. I've corrected the question accordingly. $\endgroup$ May 29 '16 at 13:53
  • 1
    $\begingroup$ @Maciej: Really? How does your polynomial algorithm work? $\endgroup$ May 29 '16 at 15:46

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:

  1. $\Phi$ is totally defined (every admissible orientation is mapped somewhere)
  2. $\Phi$ sends admissible orientations to admissible orientations
  3. $\Phi$ is an involution ($\Phi \circ \Phi$ is the identity)
  4. $\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:

  1. Every directed graph can be partitioned into strongly connected components.
  2. 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.
  3. This follows from the fact that the quotient structure of $\Phi(\vec G)$ coincides with the quotient structure of $\vec G$.
  4. By admissibility, $\vec G$ has a cycle, and hence some SCC with an edge inside it.
  • $\begingroup$ Nice observation! A simpler way of seeing this (as you say, "eliminate the graph-theoretic terminology") is to observe that if an assignment a satisfies F then the assignment a'(x) = 1-a(x) satisfies F too. This can be shown easily by induction on the number of variables of F. $\endgroup$
    – holf
    Oct 26 '16 at 9:02
  • $\begingroup$ I don’t think $\Phi$ as given is an involution. For instance, consider the 4-element graph with directed edges $0\to1\to2\to0\to3\to1$. This is an admissible orientation. Assume its first cycle is $0\to1\to2\to0$; then, after reversing this cycle, a new cycle springs into existence, viz. $0\to3\to1\to0$. If this cycle is ordered before the original one, we are in trouble. $\endgroup$ Oct 26 '16 at 10:23
  • $\begingroup$ @holf Your observation is wrong, too. Consider the CNF with clauses $x$, $\neg x\lor y\lor\neg z$, and $\neg y\lor z$. This is satisfied by the assignment $(1,1,1)$, but not by $(0,0,0)$. $\endgroup$ Oct 26 '16 at 10:27
  • $\begingroup$ I think the following definition of $\Phi$ might work. Let $M$ be the set of vertices $x$ with the property that for every $y$ reachable by a (directed) path from $x$, $x$ is reachable by a path from $y$. (As a modal logician I’d describe this as the union of final clusters of the transitive reflexive closure of the directed graph, I don’t know what would graph theorists call it.) Then reverse all edges with source (hence also target) in $M$. $\endgroup$ Oct 26 '16 at 10:32
  • $\begingroup$ @Emil: Ah yes, you're right. If I understand your suggestion right, you're saying break the orientation into strongly connected components and reverse the edges within components. I think this works. I'll update my answer accordingly. Thanks a lot!! $\endgroup$ Oct 26 '16 at 13:35

I'm not sure if my idea is understandable, so I will explain on Giorgio's example:

$( x_1 \lor x_2 \lor x_3 ) \land ( \lnot x_1 \lor \lnot x_3 \lor x_4 ) \land ( \lnot x_4 \lor x_5 ) \land ( \lnot x_2 \lor \lnot x_5 \lor \lnot x_6 )$.

First I need to change this on DNF form:

$( x_1 \land x_2 \land x_3 ) \lor ( \lnot x_1 \land \lnot x_3 \land x_4 ) \lor ( \lnot x_4 \land x_5 ) \lor ( \lnot x_2 \land \lnot x_5 \land \lnot x_6 )$ .

This should give the same answer. And no matter if I calc number of solutions modulo 2 for this:

$( x_1 \land x_2 \land x_3 ) \lor ( \lnot x_1 \land \lnot x_3 \land x_4 ) \lor ( \lnot x_4 \land x_5 ) \lor ( \lnot x_2 \land \lnot x_5 \land \lnot x_6 )$ = 0

or for this:

$( x_1 \land x_2 \land x_3 ) \lor ( \lnot x_1 \land \lnot x_3 \land x_4 ) \lor ( \lnot x_4 \land x_5 ) \lor ( \lnot x_2 \land \lnot x_5 \land \lnot x_6 )$ = 1 .

So I'm choosing the second. I have implicants:

$i_0$ = $( x_1 \land x_2 \land x_3 )$

$i_1$ = $( \lnot x_1 \land \lnot x_3 \land x_4 )$

$i_2$ = $( \lnot x_4 \land x_5 )$

$i_3$ = $( \lnot x_2 \land \lnot x_5 \land \lnot x_6 )$

Now I'm building system of equations:

${j_0}\oplus{j_1} = 1$

${j_0}\oplus{j_3} = 1$

${j_0}\oplus{j_1} = 1$

${j_2}\oplus{j_3} = 1$

${j_3} = 1$

This system has one solution. 1 mod 2 = 1, so answer is 1. But $x_6$ occurs only once. If every variable occurs two times, there is possible to have answer = 1?

  • $\begingroup$ If my thinking is OK, then the answer is "no". Of course I assume that variable occurs once in positive and once in negation. $\endgroup$
    – Maciej
    Jul 27 '16 at 17:38
  • $\begingroup$ I forgot about equation for $x_4$: ${j_1}\oplus{j_2}$ = 1. But result if the same. One solution: $j_3$ = 1, $j_2$ = 0, $j_1$ = 1, $j_0$ = 0. $\endgroup$
    – Maciej
    Jul 27 '16 at 17:58

sorry for big delay. Until now probably the problem was solved. If not, I will present my polynomial algorithm for solving $\oplus\text{Rtw-Opp-CNF}$. First let's try to calculate number of solutions modulo 2 of this equation: ${f(X)}\oplus{g(X)}$ . Where f and g are logic functions and X is a vector of variables. Common part, $f(X) \wedge g(X)$, occurs two times (one time in f(X) and one time in g(X)). So in modulo 2 common part is not important. We can calculate number of solutions modulo 2 of $f(X)$ and number of solutions modulo 2 of $g(X)$ and then sum this results modulo 2. Now let's assume that function is presented in this form:


where $i_j$ is an implicant (I mean variables connected by AND operator; for example: $x_0\wedge{x_1}\wedge{\neg{x_2}}$).

To calculate number of solutions of this function modulo 2 we can simply calc number of solutions each implicant modulo 2 and sum all results modulo 2. If we have vector of variables X and in implicant there is no all variables from this vector, then we know that number of solutions modulo 2 for this implicant is 0, because there is $2^k$ solutions, where k is number of missing variables. If implicant has all variables, then number of solutions is 1 (k = 0). So calculating number of solutions modulo 2 of $i_0\oplus{i_1}\oplus{i_2}\oplus{...}\oplus{i_{n-1}}$ is easy. Now let's consider:


We know that $a\vee{b} = a\oplus{b}\oplus({a\wedge{b}})$. In general, OR operation can be replaced by XOR of every subset of implicants connected by AND operator. And this is important step: we are interested in only those subsets that:

1) has all variables,

2) every variable occurs exacly one (if variable occurs two times, then we have positive and negative in one implicant, so this will give as 0).

Let's say that we have positive $x_0$ in implicant $i_0$ and negative $x_0$ in implicant $i_1$. Then we can write and equation:

${j_0}\oplus{j_1} = 1$.

In this equation variables ${j_0}$ and ${j_1}$ corresponds with implicants $i_0$ and $i_1$. I mean if, for example, implicant $i_0$ occurs in subset, then $j_0$ = 1. Otherwise $j_0$ = 0. If we make this for all variables, we will get set of XOR equations and we have to calculate number of solutions of this set. This problem is easy. Number of soltions if always $2^l$, when l is some value to find. That's all. I know that this is not formal proof, but I hope it is understandable.

  • $\begingroup$ Hmmm.... Is there any case when $\oplus\text{Rtw-Opp-CNF}$ = 1? $\endgroup$
    – Maciej
    Jul 27 '16 at 13:07
  • $\begingroup$ @AndrewMorgan But a formula with a unique clause containing all the variables exactly once would not be a read-twice formula. The restriction is exactly twice, not at most twice. $\endgroup$ Jul 27 '16 at 15:41
  • $\begingroup$ @AndrewMorgan The following formula (which is not read-twice because $x_6$ appears only once) has an odd number of satisfying assignments: $( x_1 \lor x_2 \lor x_3 ) \land ( \lnot x_1 \lor \lnot x_3 \lor x_4 ) \land ( \lnot x_4 \lor x_5 ) \land ( \lnot x_2 \lor \lnot x_5 \lor \lnot x_6 )$. All the variables of such formula, except $x_6$, obey to the read-twice opposite restrictions, and the number of satisfying assignments is odd inspite the formula does not "have a unique clause containing all the variables exactly once". $\endgroup$ Jul 27 '16 at 15:51
  • $\begingroup$ @GiorgioCamerani I meant that among all clauses containing all the variables, there is a unique clause present in the input formula. ie in a formula like $(x_1 \vee x_2) \wedge (\bar{x_1}) \wedge (\bar{x_2})$, there is a unique clause with all the variables present once, while in $(x_1 \vee x_2) \wedge (\bar{x_1} \vee \bar{x_2})$ or $(x_1) \wedge (\overline{x_1}) \wedge (x_2) \wedge (\overline{x_2})$ there is not. I didn't mean to exclude the presence of other clauses in the input. But in any case I think I was misunderstanding Maciej's answer, so I deleted my previous comment. $\endgroup$ Jul 27 '16 at 16:03
  • $\begingroup$ @AndrewMorgan OK, now I see. However consider that also in the family of cases you meant, the number of satisfying assignments seems to remain even. The question posed by Maciej in his comment turns out to be challenging. $\endgroup$ Jul 27 '16 at 16:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.