Many discrete problems in computer science can be encoded into Boolean satisfiability (SAT) problems. In such problems, all variables are Boolean (true or false), but are restricted by constraints between the Boolean variables.

Over the last 50 years there have been remarkable developments in understanding how to solve these constraint satisfaction problems, and many open-source solvers have been developed, some of which have been wrapped in Julia, which are capable of solving problems with millions of variables. However, their code is often difficult to understand and modify.

In order to increase the awareness and accessibility of SAT solvers in the community, and to encourage experimentation, we developed a simple solver in pure Julia that is performant for small systems.

We also have developed a tool that allows us to write down discrete problems, such as sudoku, symbolically in Julia, and encode them into SAT.