I would like the know the complexity of a specific satisfiability problem. I have a feeling it could be solved in polynomial time, but I am not sure about it. The problem is described below.

Given $n$ boolean variables $v_1, v_2, \dots, v_n$ and two types of clauses.

  1. At most $n$ clauses of the form $v_a \to \neg v_i \land \neg v_j \land \dots$ where $v_a$ cannot be on both sides of the implication.
  2. At most $n$ clauses of the form $v_a \lor v_b \lor \dots$ where any combination of variables is possible (but no negations!).

The goal is to satisfy all the clauses. I have a feeling this can be done using limited backtracking just like with 2SAT as described on Wikipedia https://en.wikipedia.org/wiki/2-satisfiability#Limited_backtracking.

  • 1
    $\begingroup$ I think this is not a research-level question because the answer can be found in wikipedia en.wikipedia.org/wiki/Boolean_satisfiability_problem. $\endgroup$
    – Laakeri
    Dec 11, 2020 at 19:47
  • $\begingroup$ The "at most $n$" can be omitted (if you have too many clauses, pad with extra unused variables and then that constraint will be satisfied). I don't believe this is covered on Wikipedia; if you believe that, please provide more specifics. $\endgroup$
    – D.W.
    Dec 11, 2020 at 19:49
  • $\begingroup$ Wikipedia mentions the NP-completeness of one-in-three positive 3-SAT, which is straightforward to reduce to this problem (with the observation that the limit for clauses doesn't really matter). $\endgroup$
    – Laakeri
    Dec 11, 2020 at 20:34

1 Answer 1


This is NP-hard.

Here is a reduction from SAT. Suppose you have a CNF formula $\varphi$ with variables $x_1,\dots,x_n$. Add variables $x'_1,\dots,x'_n$ and clauses of the form $x_i \to \neg x'_i$ and $x_i \lor x'_i$. For each clause in $\varphi$, we add a corresponding $\cdots \lor \cdots$ clause: e.g., if $x_i \lor \neg x_j \lor x_k$ is a clause in $\varphi$, then we add the clause $x_i \lor x'_j \lor x_k$. Once you've added all these clauses, add up the total number of clauses; say you have at most $m$ of the first type of clause and at most $m$ of the second type of clause. Now add unused variables $x_{n+1},\dots,x_m$. The result is an instance of your problem with $m$ variables and at most $m$ clauses of each type. Now $\varphi$ is satisfiable iff this instance is satisfiable.

  • $\begingroup$ $x_i\to\neg x'_i$ and $x'_i\to\neg x_i$ are exactly the same clause ($\neg x_i\lor\neg x'_i$). There is no need to include it twice. $\endgroup$ Dec 11, 2020 at 20:37
  • $\begingroup$ @EmilJeřábek, oops, fixed, thank you! $\endgroup$
    – D.W.
    Dec 12, 2020 at 1:30

Your Answer

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

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