9
$\begingroup$

The standard problem 1-in-3 SAT (or XSAT or X3SAT) is:
Instance: a CNF formula with every clause containing exactly 3 literals
Question: is there a satisfying assignment setting precisely 1 literal per clause true?

The problem is NP-complete and remains hard even if no variable occurs negated. I wonder whether this problem becomes easy or remains hard if each variable is required to occur at least once positively and at least once negatively.

The usual reduction from 3SAT showing that 1-in-3 SAT is hard replaces a clause $(x\lor y \lor z)$ by clauses $(\lnot x \lor a \lor b)$, $(y\lor b\lor c)$, $(\lnot z \lor c \lor d)$ where $a,b,c,d$ are fresh for each clause. Thus, this reduction doesn't help in answering my question. I've had trouble coming up with a gadget showing hardness of this variant, since if exactly 1 literal in a clause is true, then non-symmetrically 2 literals are false. If it turns out to be easy, thinking in terms of partitions of the clause set might do it, but I can't see how.

$\endgroup$
  • $\begingroup$ Can it be reduced to 2 sat? $\endgroup$ – Joshua Herman Jul 11 '15 at 20:01
  • 4
    $\begingroup$ hint: for each var $X_i$, add clauses $(X_i\vee \overline X_i \vee W) \wedge (X_i\vee \overline X_i \vee Y)\wedge (X_i\vee \overline X_i \vee Z)$ and, say, $(W \vee Y \vee \overline Z)$. $\endgroup$ – Neal Young Jul 12 '15 at 2:43
  • $\begingroup$ Ha, that works (of course adding also $(\overline W \lor Y\lor Z)\land(W\lor\overline Y \lor Z)$). I'll leave the question open in case anyone can solve it without the ever-so-slightly unsatisfying $X_i\lor\overline X_i$ trick. $\endgroup$ – Dominik Peters Jul 12 '15 at 7:05
  • 3
    $\begingroup$ May I encourage you to write up a complete answer to your own question, perhaps based upon Neal young's idea? (Incidentally, I'm not sure why that is "unsatisfying". A reduction is a reduction.) $\endgroup$ – D.W. Jul 17 '15 at 22:46
  • 4
    $\begingroup$ If that special case is the one you really care about, then maybe it makes sense to edit your question to reflect that extra constraint? $\endgroup$ – D.W. Jul 18 '15 at 15:43
2
$\begingroup$

In a comment, OP expressed interest in a reduction which generated instances with 3 distinct variables per clause. Here's a simple approach:

The reduction is from 1-in-3 SAT with 3 distinct variables per clause:

  • First of all, include all the clauses in the input formula as clauses in the output formula.
  • Second, introduce three new variables $F_1$, $F_2$, and $F_3$ and add the following three clauses to the output formula: $(\neg F_1, F_2, F_3)$, $(F_1, \neg F_2, F_3)$, and $(F_1, F_2, \neg F_3)$.
  • Finally, for each variable $x$ in the original formula, introduce a new variable $x'$, and add the following two clauses to the output formula: $(x, x', F_1)$ and $(\neg x, \neg x', F_1)$.

Let's verify that this reduction does what we want. The following properties are what we want:

  1. Each clause always has three distinct variables.
  2. Each variable occurs in some clause positively and in some clause negatively.
  3. The input formula is equivalent to the output formula.

Property 1 is trivial to check. Property 2 is also easy to check: the variables $F_1$, $F_2$, and $F_3$ each occur both positively and negatively in the clauses added in the second bullet point, while every other variable in the formula occurs both positively and negatively in the clauses added in the third bullet point.

As for property 3, this is less trivial but still easy. You can easily argue that the only assignment for variables $F_1$, $F_2$, and $F_3$ that satisfies each clause from the second bullet point is to make all three $F_i$s false. But then assuming a value of false for $F_1$, the clauses $(x, x', F_1)$ and $(\neg x, \neg x', F_1)$ added in the third bullet point are satisfied if and only if $x' = \neg x$. Since there are no other constraints on $x'$, this means that it is always possible to extend a satisfying assignment for the input formula into a satisfying assignment for the output formula: simply set each $x'$ to be the negation of the corresponding $x$ and set each $F_i$ to false.

$\endgroup$

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.