### 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.

- Open and interactive Computational Thinking with Julia and Pluto
- Calculating a million stationary points in a second on the GPU
- Introduction to metaprogramming in Julia
- Set Propagation Methods in Julia: Techniques and Applications
- Global constrained nonlinear optimisation with interval methods
- Publish your research code: The Journal of Open Source Software