# Sudoku Solver
_Aussagen und Prädikatenlogik Sommersemester 2024_

## Description
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/>

    You can contact me at hello@astrogd.eu