VU Knowledge Representation - SAT solving

This repo contains a group project from the course Knowledge Representation (2024-25) at the Vrije Universiteit Amsterdam (VU). The task was a) to create a Boolean Satisfiability (SAT) solver to resolve Sudoku Puzzles and b) to write a report answering an experimental research question related to the SAT solver.

SAT Solver

We implemented the SAT solver from scratch using the Davis Putnam Logemann-Loveland (DPLL) algorithm. The SAT solver can take any file in Clause Normal Form (CNF) with a constraint satisfaction problem in DIMACS format and returns whether it is satisfiable or unsatisfiable. In case the CNF is satisfiable, a satisfying assignment is also returned. For the purpose of our research, we additionally implemented seven branching heuristics: Random, MOMSf, one-sided and two-sided Jeroslow-Wang, DLIS, DLCS, and a custom-created Human heuristic. We used Sudokus of the classic 9x9 format to test and optimize the heuristics used for this SAT solver. You can find more details on the algorithm and heuristics in the attached report.

Research Experiment

Modern Sudoku puzzles are often created by automated systems. This means that their difficulty is assessed by a program (such as a SAT solver) rather than a human. While both SAT solvers and humans can solve Sudoku puzzles, their approaches are very different. Our research experiment investigated these differences by exploring whether using human-inspired heuristics in the SAT solver would lead to more human-like patterns in the difficulty metrics. For this purpose, we compared difficulty metrics for our SAT solver using all of the implemented heuristics mentioned above with the difficulty experienced by humans in a large Sudoku dataset. While the main findings suggest that human-inspired heuristics in an SAT solver do not lead to more human-like difficulty patterns compared to regular SAT solvers, an interesting outcome was the overall lack of available empirical data on human difficulty in solving Sudoku. Future research is thus encouraged to develop new metrics for measuring human difficulty, to empirically test them on a large number of players, and to allow open access to the resulting data sets.

Getting Started

These instructions will give you a copy of the project up and running on your local machine.

Prerequisites

Requirements for the software and other tools to build, test and push - Python 3.10 or higher

Installing

This codebase was programmed using python 3.10.1. The requirements.txt file contains all the need packages to run the code succesfully.

Download this code base by running the following line in your terminal:

git clone https://github.com/mklblm/KR-SAT-Solver

Install all required packages by running the following line in your terminal:

pip install -r requirements.txt

Running the SAT-solver

Run the SAT-solver by running the following line in terminal, inputing the relevant parameters.

python SAT.py -Sn -Pb inputfile

n = an integer from 1-9 representing the heuristic to run. See the 'heuristics' section below showing which integer represents which heuristc.

b = a boolean indicating whether a visualization of the final assignment should be shown (this only works for 9x9 sudokus).

inputfile = the path to a .cnf file containing problem to solve in DIMACS format.

Heuristics

All heuristics use the same standard DPLL algorithm including tautology solving, pure literal elimination, and unit propagation. The heuristics differ in the way a literal is chosen for branching:

1. DPLL (First available literal)
2. Random
3. DLCS (Dynamic Largest Combined Sum)
4. DLIS (Dynamic Largest Individual Sum)
5. Jeroslow-Wang one-sided
6. Jeroslow-Wang two-sided
7. MOMS (Maximum Occurrences in Minimum Size)
8. MOMSF (Maximum Occurrences in Minimum Size with a Frequency-based weighting factor)
9. Naked multiple (HUMAN)

Example

Below is an example command that can be used to solve a 9x9 sudoku puzzle.

python SAT.py -S1 -PTrue data/sudokus/DIMACS/9x9/sudoku_1_9x9.cnf

An outputfile will be created with the final assignment of all clauses in DIMACS format. A visualization of the solution to the sudoku puzzle will be plotted as well.

Authors

• Alexandra Genis github
• Daimy van Loo github
• Mikel Blom github

License

This project is licensed under the MIT License - see the LICENSE file for details