CNF formula for exactly one variable is true

Question

Given a list (array) of $n$ variables, what's the algorithm that creates a CNF Formula that will make the SAT solver return assignments in which exactly one variable is true?

I know I'm not 100% with the terms here, but I just got this assignment, having SAT explained to me today.

To make things clear I'll translate the text of the exerise:

Code a function that, given a list of variable names, returns a CNF formula for which its "list of satisfactory assignments" matches all the instances for which only one variable gets the value TRUE.

The function signature is as follows

public static int[][] exactlyOne(int[] varNames) {}

Answer 1

You want at least one variable to be true but no pair to be both true. That is, one clause of the CNF is $$v_1 \text{ or } v_2 \text{ or } \ldots \text{ or } v_n$$ and the others are of the form $\text{not } v_i \text{ or } \text{not } v_j$.

Answer 2

Hint: the DNF formula to assert this has one disjunct for each variable asserting that that variable is true and the other variables are false. Now put it into CNF.