Skip to main content

A simple wrapper for Z3 solver

Project description

Argyle_Sudoku

This project was partly based on the code from z3-sudoku

This project uses python z3-solver to benchmark encoding techniques to solving the same problem. It then compares the efficiency of each method and between different encoding techniques.

A demo of how to use the library is provided by solving sudoku in ./src/Sudokus

In Sudoku.py both traditional implementation of adding conditional constraints using if-else statements and our approach of adding conditional constraints using our custom solver is presented. An example of two different ways of querying if an index can be set to a number is presented.

Directory Structure

  • /analysis: Includes scripts and notebooks for analyzing solver performance and generating images for reports or presentations.

  • /problem_instances:

    • /particular_hard_instances_records: Particular hard instances identified during the generation process, in txt and SMT format
    • /whole_problem_records: Whole sudoku problems in txt and SMT format
    • Details of recording format explained here
  • /solvers: Houses executables and related files for various SMT solvers used in the project.

  • /src: Contains source code for core functionalities.

    • /Sudokus/Sudoku.py: Contains all functionalities of building sudoku with various constraints, logging sudoku instances to files in string format and smt format, /sudoku_database: Stores string descriptions of generated Sudoku puzzles, both full (solved) and holes (incomplete).
    • /Sudokus/run_sudoku_experiment.py: This file contains the main function. It takes in a sudoku file and solves it using the methods in sudoku.py. It then prints/ the solution and the time taken to solve it.
  • sudoku_database: Stores the already generated full and holes sudokus

    • currline.txt: stores the which line of the full sudokus file should the solver generating sudoku holes start loading from and solving when calling run_experiment
  • /tests: scripts for development testing

  • /time_records: Direct directory for storing time records from solver runs, highlighting the performance of different solvers.

The workflow is depicted in the following picture:

workflow

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

jz3-0.1.7.tar.gz (7.9 MB view details)

Uploaded Source

Built Distribution

jz3-0.1.7-py3-none-any.whl (7.9 MB view details)

Uploaded Python 3

File details

Details for the file jz3-0.1.7.tar.gz.

File metadata

  • Download URL: jz3-0.1.7.tar.gz
  • Upload date:
  • Size: 7.9 MB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/5.0.0 CPython/3.11.4

File hashes

Hashes for jz3-0.1.7.tar.gz
Algorithm Hash digest
SHA256 39269e8acfbb29a5c86e4617106edc0c518dd16048f0c6e595337b4fb28c9669
MD5 c006ff3e81ef9dc16b5081add06bb24d
BLAKE2b-256 664df6f6ad8002ecd2de26c5f90887b018ea02439f5a8f3250c74732b8d365af

See more details on using hashes here.

File details

Details for the file jz3-0.1.7-py3-none-any.whl.

File metadata

  • Download URL: jz3-0.1.7-py3-none-any.whl
  • Upload date:
  • Size: 7.9 MB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/5.0.0 CPython/3.11.4

File hashes

Hashes for jz3-0.1.7-py3-none-any.whl
Algorithm Hash digest
SHA256 04845e57f65b8d2ed010b63ce854b80930ca03d19d7c1eb82079f1bb55cc639b
MD5 8703e0df4daf2ac597c778a2a90fe9d3
BLAKE2b-256 da5f31e76542123dbd840d2b91aca0521d9f6080cde9d49779c1e42f5e4466cd

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page