I'm noodling around with making a hardware SAT solver on an FPGA, and I'm wondering if there are any interesting SAT problems smaller than, say, 50 variables both to stay within the limits of the FPGA board (namely the number of LEDs) and so I can brute-force if needed to get all possible solutions. I looked into factorizing small integers, but it seems that even relatively small numbers quickly get in to the hundreds of variables. Is there anything else I can look at besides random-SAT?
In general, you can look at hard combinatorial instances. If 50 variables is not a hard limit, try e.g., an instance arising from combinatorial block design having 105 variables described in . The actual instance in DIMACS format is here provided by the authors. For the instance, the authors write in  that: "We issue a challenge for any solver to solve it in less than one day."
Something that will be not as hard, but still not entirely trivial is coloring Mycielski graphs. These are graphs with clique number 2, but the chromatic number can be arbitrarily large. Again, if 50 variables is really a hard limit, it seems the largest Mycielski graphs you can consider is the Grötzsch graph if you use the obvious encoding to CNF. The obvious encoding will have 33 variables if you test for 3-colorability (UNSAT), and 44 variables if you test for 4-colorability (SAT).
See the international SAT solver competition. It's a competition that tests various solvers by running them on a library of hard SAT instances. You can download the instances they used to evaluate the SAT solvers. I would suggest you look at these competitions and see if any of the instances they've used would meet your needs.