===========================================================================
CSC 363                     Homework Exercise 6                   Fall 2008
===========================================================================

Due: by 2pm on Wed 19 Nov
Worth: 1.5%

For each question, please write up detailed answers carefully: make sure
that you use notation and terminology correctly, and that you explain and
justify what you are doing.  Marks *will* be deducted for incorrect or
ambiguous use of notation and terminology, and for making incorrect,
unjustified, ambiguous, or vague claims in your solutions.


1.  A propositional formula F is in "exact 4-CNF" if it is in 4-CNF (i.e.,
    each clause of F contains exactly 4 literals) and in addition, each
    clause of F contains no repeated variable (negated or otherwise).

    Give a detailed proof that the following language is NP-complete.

        X4SAT = { <F> : F is a satisfiable formula in exact 4-CNF }

    For example:

     -  (x_4 \/ ~x_2 \/ x_1 \/ x_3) /\ (~x_1 \/ ~x_2 \/ x_3)
        does *not* belong to X4SAT -- it is not in 4-CNF.

     -  (x_3 \/ ~x_2 \/ x_1 \/ x_3) /\ (~x_3 \/ x_1 \/ x_2 \/ ~x_4)
        does *not* belong to X4SAT -- it is not in exact 4-CNF because
        variable x_3 is repeated in the first clause.

     -  (x_4 \/ ~x_2 \/ x_1 \/ x_3) /\ (~x_2 \/ x_1 \/ x_2 \/ ~x_4)
        does *not* belong to X4SAT -- it is not in exact 4-CNF because
        variable x_2 is repeated in the second clause.

     -  (x_4 \/ ~x_2 \/ x_1 \/ x_3) /\ (~x_3 \/ x_1 \/ x_2 \/ ~x_4)
        *does* belong to X4SAT -- it is in exact 4-CNF and can be satisfied
        by setting x_1 = true, x_2 = false, x_3 = false, x_4 = false.

    Hint:  To begin, read and understand the reduction CNF-SAT <=p 3SAT
    posted on the course website.