Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.
2 added 193 characters in body
source | link

Let's assume for simplicity that each negated literal appears exactly once. Let $C_i$ be the clause containing $\lnot x_i$. Consider the graph whose vertices are the variables, and $x_i$ is connected to $x_j$ if $x_j \in C_i$. This is a kind of implication graph: in order to deduce that $x_i$ is false from $C_i$, we must have first deduced that $x_j$ was false from $C_j$.

Show that $x_i$ is forced to be false (i.e., unit propagation shows that $x_i$ has to be false) iff the set of vertices reachable from $x_i$ contains no directed cycle, something which can be checked in NL (using coNL=NL). The formula is unsatisfiable iff there exists a positive clause in which all variables are forced to be false (and so unit propagation gets stuck at this clause).

This shows that your problem is in NL. To show that it is NL-complete, reduce from directed reachability. Encode all edges incoming to $x_i$ by a clause of the form $\lnot x_i \lor \cdots$.

Let's assume for simplicity that each negated literal appears exactly once. Let $C_i$ be the clause containing $\lnot x_i$. Consider the graph whose vertices are the variables, and $x_i$ is connected to $x_j$ if $x_j \in C_i$. This is a kind of implication graph: in order to deduce that $x_i$ is false from $C_i$, we must have first deduced that $x_j$ was false from $C_j$.

Show that $x_i$ is forced to be false (i.e., unit propagation shows that $x_i$ has to be false) iff the set of vertices reachable from $x_i$ contains no directed cycle, something which can be checked in NL (using coNL=NL). The formula is unsatisfiable iff there exists a positive clause in which all variables are forced to be false (and so unit propagation gets stuck at this clause).

Let's assume for simplicity that each negated literal appears exactly once. Let $C_i$ be the clause containing $\lnot x_i$. Consider the graph whose vertices are the variables, and $x_i$ is connected to $x_j$ if $x_j \in C_i$. This is a kind of implication graph: in order to deduce that $x_i$ is false from $C_i$, we must have first deduced that $x_j$ was false from $C_j$.

Show that $x_i$ is forced to be false (i.e., unit propagation shows that $x_i$ has to be false) iff the set of vertices reachable from $x_i$ contains no directed cycle, something which can be checked in NL (using coNL=NL). The formula is unsatisfiable iff there exists a positive clause in which all variables are forced to be false (and so unit propagation gets stuck at this clause).

This shows that your problem is in NL. To show that it is NL-complete, reduce from directed reachability. Encode all edges incoming to $x_i$ by a clause of the form $\lnot x_i \lor \cdots$.

1
source | link

Let's assume for simplicity that each negated literal appears exactly once. Let $C_i$ be the clause containing $\lnot x_i$. Consider the graph whose vertices are the variables, and $x_i$ is connected to $x_j$ if $x_j \in C_i$. This is a kind of implication graph: in order to deduce that $x_i$ is false from $C_i$, we must have first deduced that $x_j$ was false from $C_j$.

Show that $x_i$ is forced to be false (i.e., unit propagation shows that $x_i$ has to be false) iff the set of vertices reachable from $x_i$ contains no directed cycle, something which can be checked in NL (using coNL=NL). The formula is unsatisfiable iff there exists a positive clause in which all variables are forced to be false (and so unit propagation gets stuck at this clause).