I am interested in the complexity of a special case of the boolean satisfiability problem:

We are given a boolean formula, consisting only of the logical operators $\land$ and $\lor$ (that can be arbitrarily nested) and one positive and one negative literal for every variable, arranged in the following way: $x_1$ is the first literal in the formula, $\lnot x_1$ is the last, $x_2$ is the second, $\lnot x_2$ the second last etc. The goal is to decide whether the formula is satisfiable.

Example: $(x_1\lor x_2)\land(x_3 \lor (x_4 \land x_5) \lor (\lnot x_5 \land (\lnot x_4 \lor (\lnot x_3 \land \lnot x_2)) ) ) \land \lnot x_1$

Note: I am not limiting the boolean formula to be a CNF. I already know that deciding satisfiability of a boolean formula where each variable has exactly one positive and one negative literal is NP-hard. This special case with the specific ordering doesn't seem much easier, but I can't think of a reduction.

  • $\begingroup$ What's the motivation for studying this problem? Can you share anything about the context in which you encountered it? $\endgroup$
    – D.W.
    Commented Apr 28 at 4:11
  • $\begingroup$ I was originally working on some routing problem and found a complicated reduction to this problem, which I am assuming to be NP-hard, but I can't find any literature to this specific problem. A related post would be mathoverflow.net/questions/9512/… and the results I know are from Peter Heusch's "The complexity of the falsifiability problem for pure implicational formulas" (doi.org/10.1016/S0166-218X(99)00036-0) $\endgroup$
    – SimonNW
    Commented Apr 28 at 15:16


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.