A tool converting a given 9x9 sudoku into DIMACS CNF to be solved with a SAT solver, and reverting the solution from the SAT solver back into an easy readable sudoku visualitsation
## Installation
1. Clone the repository
2. Install [`Node.js`](https://nodejs.org/en) (>=20.14.0) and [`pnpm`](https://pnpm.io/)
3. Run `pnpm install` in the root directory of the repository
## Usage
1. Edit the `generateRules.ts` file to include the fixed numbers of the sudoku you want to solve
2. Run `pnpm run generate` to generate the DIMACS CNF file into `output.cnf`
3. Run the SAT solver of your choice with the generated DIMACS CNF file
4. Run `pnpm run visualize` to convert the solution of the SAT solver within a `result.cnf` file back into a readable sudoku.
## SAT Solver
I used the SAT solver [`CryptoMiniSat`](https://github.com/msoos/cryptominisat) for this project, but other ones should be fine as well as long as they can handle DIMACS CNF files.
## License
This software is licensed under GNU AGPLv3 License. For more information, see the `LICENSE` file.
Sudoku Solver - Aussagen und Prädikatenlogik Sommersemester 2024
Copyright (C) 2024 AstroGD® Lukas Weber
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published
by the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU Affero General Public License for more details.
You should have received a copy of the GNU Affero General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>
