Skip to content
/ sat Public

python implementations of algorthims for the boolean satisfiability problem, including one to solve 3SAT in polynomial time

Notifications You must be signed in to change notification settings

Quiggleson/sat

Repository files navigation

Usage

Benchmarks

A list of benchmark problems can be found here

Run readcnf.py to iterate through the files in /inputs or /UUF50.218.1000 (you have to unzip satisfiable instances into /inputs or unsatisfiable instances into /UUF50.218.1000 and call the function at the bottom of the file)

Currently there's a bug with the unsatisfiable benchmark problems with the optimize.py solution, but it's being looked into

Script Usage

checkimplications.py is the main script to check if algorithms work

  • the bottom is hecka messy right now, but gen_random_instance() will generate a list of random instances of 3SAT and you can try different functions using that list
  • solve_gen() and solve_expand() are old solve functions that use lists of lists, they should be accurate, but slow (8 hours for 1000 10-terminal instances iirc?)

optimize.py is the newest script to attempt a O(n^6) runtime

  • pass the instance as a list of lists into process() and it will return a bool: False for unsatisfiable, True for satisfiable

main.py

  • write_blockages() will write a md file of the assignment table and instance as well as return True (satisfiable) or False (unsatisfiable) for the input instance
    • it will overwrite existing files, it was not made for robustness in that regard

most other functions are depracated, I haven't had the chance to clean it up yet

About

python implementations of algorthims for the boolean satisfiability problem, including one to solve 3SAT in polynomial time

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published