Satisfiability modulo theories library, is the a grand title given to what we will refer to as SMT – Lib or even just SMT. This blog and its associated articles are the result of trying to find some software that would both complete every possible known Sudoku and provide a way forward for a problem solving project that was bogged down.
SMT has quite a high barrier to entry, the descriptions of how they work and what they can do are very mathematically orientated, using symbols and characters that are unfamiliar to most computer programming folks. However, with a little perseverance, trial and error, they can be a great stepping stone toward solving a multitude of different problems.
Starting out with solving Sudoku in mind. The initial step was understanding how to describe the rules of Sudoku in a way that can be presented to a general purpose, SMT solver. Unlike other programming approaches, the required effort is around describing the rules and conditions of the problem whilst completely ignoring how to progress those rules to reach an answer. The solver takes on all the effort of reconciling the constraints of the particular puzzle, giving a viable answer or rejecting the puzzle as unsatisfiable.
Gone is the complexity of implementing the many solving rules for Sudoku replaced by a simple text manipulation script that reads the input puzzle, generates a SMT language file, passes it to the solver then reads the solver results. This solution pipeline can be applied to many different puzzle types ( but not crosswords) with just minor adjustments to the scripts.
The stages of the puzzle solving pipeline are are :
- Image of Puzzle,
- Text representation of puzzle,
- Script to convert from text to SMT language,
- Solver,
- Script to convert results to a display.
A detailed writeup on Sudoku and some of its variants can be found here but the short description is as follows :
- Tell solver what type problem this is and that answer values will be required
- Declare 81 integers each of which can only have values between 1 and 9.
- Declare that each row, column and sub-square must have unique values,
- Set the known clue numbers,
- Ask for the answers
By describing the problem in this exact way the solver will find an answer. For sudoku puzzles of different shapes and answer values, the number of variables and their range can be simply adjusted in the conversion script.
The solver used is not artificial intelligence. They are entirely deterministic and driven purely by the input statements provided to them. By defining the problem in strict logical terms, that logic can be manipulated in order to find the answers. No guesswork or training is required by the solver. Every answer is logically deducted from the provided input statements.
Following on from the success of solving any type and shape of Sudoku, other puzzles were tackled using a similar techniques. The wrinkle being some of the problems require careful manipulation in order to create the required SMT language. The conversion of results into a displayable page image was mostly taken care of using generated HTML text displayed in a browser.
SMT solvers have traditionally been used in the rarefied areas of theorem proofing and program integrity, checking. There use here whilst less formal provides some insight into how deconstructing a problem into its core aspects, and then concentrating just on those features can provide a useful introduction to 1st order logic and getting the job done quickly.
Formal SMT-Lib reference material available here
The the solvers used are
This book does things a similar way but using different solvers and single example for each puzzle. ( This is the book I would have liked to write if Adrain hadn't got there first ( and better ))
" Illustrates the complete process of modelling and solving puzzles with theorem provers. Maximizes students insights into modelling with logic, interpretation models, or theorem proving
Shares many tips and examples on formalising natural language into logic"
Modelling puzzles in first order logic by Adrian Groza ISBN: 978-3-030-62547-4
No comments:
Post a Comment