Comments are moderated. It may take a few minutes before your comment appears.
Markdown is supported in your comments.
Consider how you would write a solver for n-queens (not just 4-queens) and sudoku. Sudoku is almost a perfect fit for SAT, being little more than 81-rooks on a 3.09D 9x9x9 grid. A basic sudoku example is in the github repo.