# Effective problem solving using SAT solvers

## TL;DR

This paper demonstrates how to leverage Maple's built-in SAT solver to automatically solve a variety of problems and puzzles by encoding them into Boolean logic, eliminating the need for custom search algorithms.

## Contribution

It introduces a method for solving diverse problems using SAT encoding within Maple, showcasing its versatility and ease of use.

## Key findings

- Successfully solved the n-queens problem
- Generated and solved Sudoku puzzles automatically
- Solved logic puzzles like Einstein riddle and maximum clique

## Abstract

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.