Seeking nontrivial small SAT/UNSAT instances I need SAT instances, involving 9 to 20 variables. They need to be hard to solve for humans. Both SAT and UNSAT instances are needed.

I tried random-SAT generators on the web, but the results were not satisfactory because they are trivial. A good example of what I'm looking for is the following 4-variable instance from The Art of Computer Programming: $$12\bar3, 23\bar4, 134, \bar124, \bar1\bar23, \bar2\bar34, \bar1\bar3\bar4, 1\bar2\bar4.$$
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.