Seeking nontrivial small SAT/UNSAT instances
To build a satisfiable instance, start by picking an assignment to the variables that will be a solution.  Then, randomly generate clauses that are satisfied by this assignment.  Add as many clauses as desired.  If you add enough clauses, then with high probability your chosen solution will be the only one, and the problem will be non-trivial.

For instance, suppose your assignment is $x_1=\text{True}$, $x_2=\text{False}$.  Then you could add any subset of the clauses $x_1 \lor x_2$, $x_1 \lor \neg x_2$, or $\neg x_1 \lor \neg x_2$.  For example, one random formula you could generate might be $(x_1 \lor x_2) \land (\neg x_1 \lor \neg x_2)$.

To build an unsatisfiable instance, proceed as above; then add one more clause that is violated by the solution you chose in advance.  If you added enough clauses, it is likely that there will be no other solution, so the problem will be unsatisfiable.  Check with a SAT solver just to be sure.