# Effective problem solving using SAT solvers

arXiv: https://arxiv.org/abs/1906.06251 · HTML: https://mlsanity.com/paper/1906.06251/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Jun 2019.

## Built on by (most cited first, 2 of 2)

- [The Fifteen Puzzle- A New Approach through Hybridizing Three Heuristics Methods](https://mlsanity.com/paper/2302.02985/) (2023)
- [Nested Search versus Limited Discrepancy Search](https://mlsanity.com/paper/2210.00216/) (2022)

## Abstract (arXiv)

In this article we demonstrate how to solve a variety of problems and puzzles using the built-in SAT solver of the computer algebra system Maple. Once the problems have been encoded into Boolean logic, solutions can be found (or shown to not exist) automatically, without the need to implement any search algorithm. In particular, we describe how to solve the n-queens problem, how to generate and solve Sudoku puzzles, how to solve logic puzzles like the Einstein riddle, how to solve the 15-puzzle, how to solve the maximum clique problem, and finding Graeco-Latin squares.