Skip to content

Encode knot mosaics as a SAT formula and solve with a SAT solver.

License

Notifications You must be signed in to change notification settings

HM0880/knot-mosaics

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

24 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Knot Mosaics README

Intro

Encode knot mosaics as a SAT formula and solve with a SAT solver.

Files

  • ./encode.py : Encode knot mosaics as a SAT formula.
  • ./solve.py : Get all solutions of a knot mosaic SAT formula with PySAT bindings [1,2].

Other

As of September 2022, for solving boards larger than 4x4, the best solver that we have found is Toda’s BDD-based ALLSAT solver [3].

My publications

References

[1] https://pysathq.github.io/

[2] https://github.com/pysathq/pysat

[3] https://www.disc.lab.uec.ac.jp/toda/code/allsat.html

About

Encode knot mosaics as a SAT formula and solve with a SAT solver.

Topics

Resources

License

Stars

Watchers

Forks

Languages