#Notes: Proving Exact 4-SAT problem as NP Complete

Problem : Exact 4-SAT

Statement :

In the Exact 4-SAT problem, the input is a set of clauses, each of which is a disjunction of exactly four literals, and such that each variable occurs at most once in each clause. The goal is to find a satisfying argument, if one exists. Prove that Exact 4-SAT is NP-complete.

Reference - DPV 8.8

Solution:

We will try to solve the problem by proving EXACT-4-SAT problem as NP Complete in following steps:

1. EXACT-4-SAT problem is NP Problem.

   Argument → For a given solution S of the problem, for each clause, it will take O(1) time to verify if any one literal of the clause is satisfied, and we will check for all m clauses. Thus in O(m) time we can verify the solution S which is in polynomial time.

2. EXACT-4-SAT problem is as hard as the 3-SAT problem. We will apply reduction 3-SAT → EXACT-4-SAT.

   1. Input to 3-SAT can be converted into input to EXACT-4-SAT in polynomial time.

      Argument → We can convert the input of 3-SAT problem by taking the following action for each clause length -

      if clause length is 3, we can replace it by new clauses with one more variable x₁

      (a∨ b∨ c) → (a∨ b∨ c∨ x₁) ∧ (a∨ b∨ c∨ ~x₁) —- (1)

      If clause length is 2, we can use 2 new variables and replace the clause by 4 new clauses.

      (a∨ b) → (a∨ b∨ x₁∨ x₂) ∧(a∨ b∨ x₁∨ ~x₂) ∧(a ∨ b∨~x₁∨x₂)∧ (a∨ b∨ ~x₁∨ ~x₂) — (2)

      For length 1, we can use 3 new variables and replace by 8 new clauses.

      (a) → (a∨x₁∨x₂∨x₃) ∧ (a∨x₁∨x₂∨~x₃) ∧ (a∨x₁∨~x₂∨x₃) ∧ (a∨x₁∨~x₂∨~x₃) ∧ (a∨~x₁∨x₂∨x₃) ∧ (a∨~x₁∨x₂∨~x₃) ∧ (a∨~x₁∨~x₂∨x₃) ∧ (a∨~x₁∨~x₂∨~x₃) —– (3)

      Each of clause C can be converted into new clause C₁ in polynomial time O(n) and we have m such clauses. Thus we can convert into O(nm), which is polynomial time.

   2. Solution to the EXACT-4-SAT problem can be converted to solution for 3-SAT in polynomial time.

      Argument → For the solution found S, for EXACT-4-SAT problem, we can convert to solution of 3-SAT by simply dropping the extra new variables from each clause that we added in step(a). This can be done in polynomial time as well as we have m clauses, and constant time to remove the extra variables added - O(m)

   3. Solution to EXACT-4-SAT exists iff solution to 3-SAT problem.

      Argument → We can prove that if there is a solution to EXACT-4-SAT solution then there is a solution to 3-SAT problem and vice versa.

      If we check for clause (1) , if the EXACT-4-SAT is true, that is (a∨ b∨ c∨ x₁ ) ∧ (a∨ b∨ c∨ ~x₁ ) is true, the reduced clause for 3-SAT (a∨ b∨ c) will always be true as value for new variable x₁ can be either True or False, which satisfies either one of the clauses.

      We can also prove that if (a∨ b∨ c) is satisfied, then by adding a new variable x₁, the clause (a∨ b∨ c∨ x₁) ∧ (a∨ b∨ c∨ ~x₁) will be true as well, as value of x₁ can be either True or False, which will satisfy either of one of the clause, thus satisfying the clause.

      We can do similar exercise for –(2) and –(3) clauses.

      Thus, Solution to EXACT-4-SAT exists iff solution to 3-SAT problem.

Thus EXACT-4-SAT is a NP Complete problem.