/Mastermind-SAT-solver

Using boolean SATisfiability to find a solution to a game of mastermind

Primary LanguagePython

Mastermind Solver using Z3 in Python

Using Z3 library to find a solution to a set of constraints given in a game of mastermind. Leveraging the pigeon-hole principle.

Usage

You can modify the constraints given at the beginning of the code (later to be set in a separate input file).

  1. In your console, cd into the directory where the python file mastermind-solver.py is,

  2. Install the required dependencies by running pip install -r requirements.txt,

  3. then run python mastermind-solver.py.

Documentation

Z3 for Python

Minisat for Cpp