# Proving a reformulation of the $(\ge k)\mathit{-SAT}$ problem is in P

Consider the $$(\ge k)\mathit{-SAT}$$ problem, where you are given a CNF (conjunctive normal form) formula $$F$$ such that each clause has at least $$k$$ literals, and the goal is to determine whether $$F$$ is satisfiable. A literal can occur at most once in a clause.

Prove that the $$(\ge n)\mathit{-SAT}$$ problem is in $$\mathsf{P}$$, where $$n$$ is the number of input variables in the input formula.

I am having a lot of issue setting up this proof, can anyone help or guide me?

• What's the context where you encountered this task? Can you credit the original source where you saw this?
– D.W.
Commented Mar 1, 2022 at 6:14

The problem statement doesn't make clear whether literals are allowed to repeat in clauses. If literals are allowed to repeat then you can reduce 3SAT to your problem, which is thus NP-complete. This suggests that the intended interpretation is that each literal appears at most once.

Clauses which contain both a variable and its negation are always satisfied, so we can remove them. Any clause that remains forbids exactly one truth assignment. You take it from here.

• I do not understand what you mean by saying that any clause that remains forbids exactly one truth assignment... Are you referring to the fact that from every clause to which its variable and its negation are present, it is always satisfied, thus we do not have to consider that truth assignment or are you referring to something entirely different? I am assuming once I understand this, I can simplify every truth assignment to every clause in a manner I will be able to reduce the problem?
– Guts
Commented Feb 28, 2022 at 18:50
• For example, the clause $x_1 \lor \cdots \lor x_n$ rules out the all-false assignment. Commented Feb 28, 2022 at 20:07
• OH I believe I know what to do from here, thank you!
– Guts
Commented Feb 28, 2022 at 20:47