Solving discrete problems via Boolean satisfiability with Julia
2021-07-28, 13:10–13:20 (UTC), Red

Many discrete problems in mathematics and computer science can be encoded into Boolean satisfiability (SAT) problems, and then solved by one of the many SAT "solvers" written in C or C++, which are now capable of solving problems with millions of variables.

In order to understand the algorithms and trade-offs involved, we developed a simple SAT solver in pure Julia that is performant for small systems. We also have developed simple tools to encode discrete problems like sudoku into SAT.


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.

Professor of Computational Science at the Universidad Nacional Autónoma de México and visiting professor at MIT.

Interested in computational science, interval arithmetic, and numeric-symbolic computing.

Author of the JuliaIntervals suite of packages for interval arithmetic, and various tutorials on Julia.

This speaker also appears in: