Constructing Useful SAT Instances Given a set of binary strings, all of length $s$, is it possible to construct a SAT instance with s literals that is satisfied only by those binary strings as assignments?
For example, consider the set $\{101, 110\}$. Can we construct a SAT instance with literals $x_1$, $x_2$, and $x_3$ such that it is satisfied only by the assignments $x_1 = 1$, $x_2 = 0$, $x_3 = 1$ or $x_1 = 1$, $x_2 = 1$, $x_3 = 0$?
It would be even more useful if this instance is an instance of k-SAT for some k. 
 A: Every such set of strings determines a collection of rows in the truth table, and so you want an expression that is logically equivalent to the disjunction of those rows. This gives a logical expression in disjunctive normal form, but every propositional assertion can be put into conjunctive normal form, which makes it an instance of SAT.
A: I suppose by "literals" you mean variables.
If you allow additional temporary variables
there is explicit polynomial encoding in 4-SAT
by carefully constructing the CNF.
First we construct CNFs for the satisfying assignments,
then do disjunction of the CNFs.
Encode binary string $s$ this way.
For the $i$-th digit introduce boolean variable $v_i$.
$1$ is $v_i$, $0$ is $\lnot v_i$.
A satisfying assignment is conjunction $ v_1' \land v_2'\ \cdots \land v_n'$
where $v_i'$ is either $v_i$ or $\lnot v_i$.
To encode the conjunction, use AND gate in CNF encoding.
The CNF for $ AND(A,B,C) := C \iff (A \land B$) is 
$$
\begin{aligned}
& \lnot A \lor \lnot B \lor C \\
& A \lor \lnot C \\
& B \lor \lnot C
\end{aligned}
$$
By using the AND gate and fresh variables $w_i$, encode each
satisfying assignment $s_i$ to a 3-CNF $C_i$.
Basically $C_i = \{AND(v_1',v_2',w_1), \ldots AND(v_k',w_{k-1},w_k), w_n \}$
Remains to encode the disjunction of the CNFs $C_i$.
Define the transformation $F(C_i)$ by introducing boolean
variable $y_i$ and add $\lor y_i$ to each clause of $C_i$
(this is just adding $y_i$ to the CNF clause).
If $y_i$ is $False$, then $F(C_i)$ is just $C_i$ and it
is satisfiable only by $s_i$.
To force at least one $y_i$ to be $False$ add the clause
$$ \lnot y_1 \lor \lnot y_2 \cdots \lor \lnot y_n$$.
So the final CNF is $CN = \{F(C_1) \ldots F(C_n), \lnot y_1 \lor \lnot y_2 \cdots \lor \lnot y_n\}$.
which by construction is 4-SAT and is polynomial in the size of
the input.
Using an AND gate adds 3 clauses and one new variable
and this is polynomial.
