1. To show this is in NP, we will use a verifier. Our certificate will be the two satisfying assignments.

On input <I,c1,c2>...
1. Check if c1 satisfies boolean formula I. If not, REJECT.
2. Check if c2 satisfies boolean formula I. If not, REJECT.
3. ACCEPT

Runtime/Correctness: Follows directly from what we've seen from SAT.

Now to show that DCS is NP-hard, we will reduce from 3SAT. Note that 3SAT has formulas in CNF form whereas SAT does not.

Our reduction follows via the following computible function:

On input <Phi>... // This is our input to 3SAT
1. Let Phi_2 = Phi with the added clause (x OR x'), where x' is the negation of x and x is a literal NOT container in Phi. Formally, Phi_2 = Phi AND (x OR x')
2. Output <Phi_2>. // This is our input to DCS

Note that the reduction is indeed computed in polytime: we need not even modify the input tape, but simply add on to its end a clause in an appropriate encoding.

Claim: If Phi is satisfiable, then Phi_2 has at least two satisfying truth assignments.
Proof: Let T be the truth assignment for Phi. Then one verifies that T with x=TRUE satisfies Phi_2. Similarly, T with x=FALSE satisfies Phi_2. These two assignments are unique, so the result follows.

Claim: If Phi is not satisfiable, then Phi_2 is not satisfiable.
Proof: Suppose otherwise, let T be the truth assignment satisfying Phi_2. Let T' be the subset of T containing all truth assignments to literals excluding x. Then T' satisfies Phi. 

Then we see that 3SAT reduces to DCS. Since every language in NP reduces to 3SAT, we conclude that all languages in NP reduce to DCS and hence DCS is NP-hard. Since DCS is also in NP, DCS is NP-complete by definition.