4
$\begingroup$

I'm trying to solve a question which requires me to

  1. prove that an instance of 3SAT where each literal appears in exactly 3 clauses (positive and negative appearances combined) and each clause contains exactly 3 literals is always satisfiable.

  2. Find a polynomial time algorithm to find a satisfying assignment for it.

My Solution

I'm not sure how to prove part 1. I'm trying to solve 2 by reducing it to an instance of Vertex Cover in which each literal has 2 nodes - one positive, one negative - and each node is connected to the other literals its in a clause with. A vertex cover of size m = # of literals will give us the assignment needed.

Im not sure of I'm along the right path or not? Any help would be appreciated!

$\endgroup$
  • $\begingroup$ "each clause contains exactly 3 literals". It looks like it actually means "each clause contains exactly 3 variables". We are talking about 3SAT, anyway. $\endgroup$ – John L. Mar 14 '19 at 5:52
  • $\begingroup$ @Apass: If a 3-literal clause contains two variables, then the clause is trivially satisfied and can be dropped. Ex. The clause $(a ∨ \bar{a} ∨ b)$ contains 3 literals and 2 variables. It is always satisfied because either $a$ or $\bar{a}$ will always be true. Same goes for a clause with 3 literals and one variable. So, I think the original statement with "3 literals" is correct ;) $\endgroup$ – Oleg Melnikov Jul 25 '19 at 2:07
  • 1
    $\begingroup$ @Apass. I don't think the statement "exactly 3 literals"is redundant, since there are various versions of 3SAT. The DPV textbook tends to use 3SAT defined with up to 3 literals. CLRS textbook defines 3SAT as containing exactly 3 literals. These two versions are reducible to one another, but it's important to state which one is used in the problem. $\endgroup$ – Oleg Melnikov Jul 25 '19 at 2:10
  • 1
    $\begingroup$ @OlegMelnikov Thanks for your clarification, "since there are various versions of 3SAT". $\endgroup$ – John L. Jul 25 '19 at 2:12
4
$\begingroup$

It looks like you missed the promising reformulation of this 3SAT. The simple idea is to select a different variable for each clause.

Always satisfiable

Let the variables be $V=\{v_1, v_2, \cdots, v_n\}$ and the clauses be $C=\{c_1,c_2,\cdots, c_m\}$.

Construct a bipartite graph $G=(C,V)$, where $(c,v)$ is an edge if $v$ or $\neg v$ is a literal of $c$. The given conditions mean the degree of each clause and the degree of each variable are 3.

For a subset $W$ of $C$, let $N(W)$ denote the set of all variables adjacent to some clause in $W$. Consider the edges that have one endpoint in $W$. The number of them is exactly $3|W|$ and at most $3|N(W)|$. Hence $|W|\leq |N(W)|.$ By Hall's marriage theorem, for each clause $c$, we can select a distinct variable $m(c)$ such that $(c,m(c))$ is an edge.

For all clause $c$ do the following. If $m(c)$ is a literal of $c$, set $m(c)$ to be true. Otherwise, $\neg m(c)$ is a literal $c$ and we set $m(c)$ to be false. In either case, $c$ becomes true.

Polynomial algorithm

The proof above actually gives the outline of an algorithm. Each step of the algorithm takes polynomial time. In particular, the application of Hall's marriage theorem can be implemented in polynomial time as, for example shown here.

A generalization

Here is a natural generalization.

Exercise. Generalize to the case when each variable appears in at most $r$ clauses and each clause contains at least $r$ distinct variables, where $r\ge1$.

$\endgroup$
  • $\begingroup$ I disagree with "the degree of each variable is 3". Consider $(a ∨ c ∨ d) ∧ (a ∨ ¬b ∨ ¬c) ∧ (b ∨ ¬c ∨ ¬d)$, which has 3 clauses and 4 variables. In particular, $a,b,d$ have degree 2. $\endgroup$ – Oleg Melnikov Jul 25 '19 at 2:06
  • 1
    $\begingroup$ @OlegMelnikov It occurs to me that the problem says "each literal appears in exactly 3 clauses". Does $a$ appear in exactly 3 clauses? $\endgroup$ – John L. Jul 25 '19 at 2:15
  • $\begingroup$ Good catch. My bad :) You are correct. Basically, addition of any literal implies it's three appearances across clauses. $\endgroup$ – Oleg Melnikov Jul 25 '19 at 2:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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