2
$\begingroup$

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.

Improve this question
$\endgroup$
4
  • $\begingroup$ Are you familiar with Resolution? $\endgroup$
    – Yuval Filmus
    Apr 29, 2022 at 18:38
  • $\begingroup$ I am not, could you elaborate? $\endgroup$
    – PhPanda
    Apr 29, 2022 at 20:27
  • 1
    $\begingroup$ 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. $\endgroup$
    – Yuval Filmus
    Apr 29, 2022 at 21:08
  • $\begingroup$ 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. $\endgroup$
    – PhPanda
    May 13, 2022 at 21:02

1 Answer 1

Reset to default
2
$\begingroup$

Repeatedly perform the following simplification procedures:

  • If a variable appears only once, we can satisfy the unique clause containing it by setting the variable accordingly. Therefore we can remove the clause.
  • If a variable appears twice but with the same polarity, we can satisfy both clauses containing it by setting the variable accordingly. Therefore we can remove both clauses.
  • If a variable appears twice, with opposite polarity, at the same clause, then the clause is always satisfied, and so can be removed.
  • 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.

Eventually no variables will be left. Either no more clauses are left, in which case the formula is satisfiable, or some empty clauses are left, in which case the formula is unsatisfiable.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Oh I see, thank you for the clarification of the simplification procedure! What isn't entirely clear to me is the complexity of the procedure. Hence is the problem in P or in NP-complete like regular 3-SAT? $\endgroup$
    – PhPanda
    May 14, 2022 at 9:23
  • $\begingroup$ You'll have to work it out on your own, I'm afraid. $\endgroup$
    – Yuval Filmus
    May 14, 2022 at 10:20

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.