# Complexity of a restricted SAT problem

I am wondering about the complexity of the following SAT related problem:

Given a CNF with $$n$$ clauses containing exactly $$k$$ literals with the following properties:

• The intersection of any pair of different clauses only contains 1 variable.
• Every variable is only contained in one intersection. So every variable appears at most in two different clauses.

For example for $$k=3$$ : $$(x \vee y \vee z)\wedge(y \vee u \vee w)\wedge (x \vee w \vee v)$$ is a valid formula.

Is checking the satisfiability of this problem still NP-complete like 3-SAT? My gut tells me that the heavy restriction on the form may made it easier to solve this problem, but I'm not sure.

• Are you familiar with Resolution? Commented Apr 29, 2022 at 18:38
• I am not, could you elaborate? Commented Apr 29, 2022 at 20:27
• If $C,D$ are clauses, then $(C \lor x) \land (D \lor \lnot x)$ is logically equivalent to $C \lor D$. This is known as the cut rule, and underlies the proof system Resolution. Commented Apr 29, 2022 at 21:08
• I've looked a bit into this cut rule and such. I am beginning to think that it may be P but I am really unsure. My reasoning is that because of this cut rule we can reduce a clause which has a non-empty interesesction with three other clauses to a clause with 6 variables. This clause may still interesect other clauses and we can again reduce them with the cut rule. After reducing all of these clauses we are left with a single clause containing a lot of variables, which we can easily check for satisfiablitlity. My reason may be totally flawed as I am fairly new to the subject. Commented May 13, 2022 at 21:02

• If a variable appears twice, in a clause $$C \lor x$$ and in a clause $$D \lor \lnot x$$, replace both with their resolvent $$C \lor D$$, which is logically equivalent to them.