Comment by nextos

You'd need a fancy encoding for SAT to use a small DPLL implementation.

Otherwise, customize DPLL for this particular problem.