2-SAT4 Satisfiability Decision Problem

Definition

2-SAT4 Satisfiability Decision Problem

Instance: A Boolean formula $F={\bigwedge }_{j=1}^m{C}_j$ in conjunctive normal form satisfying

$$|\{j:|C_j|\ge 3\}|\le 4,$$

where $|C_j|$ counts the literals in clause $C_j$. The bound $4$ is fixed, not part of the input; the exceptional clauses may have arbitrary length.

Question: Does there exist a truth assignment $\alpha :\mathrm{Var}(F)\to \{\top ,\perp \}$ with $\alpha \models F$?

Equivalently, the allowed inputs become 2-SAT formulas after deleting at most four clauses. Satisfiability is still required for the entire original formula, including those clauses.