Saturn
Status: Pre-release
Version: N/A
License: Unlicensed
Saturn is a complete SAT solver built in C++20. It is currently educational material meant to teach others how SAT solvers operate and how they are implemented at a low level. While it is good enough to be used as a standalone solver, it is most likely not competition worthy, and we suggest other solvers to be used while we develop it further.
As of now, Saturn isn't ready for release, and is unlicensed. Since it is unlicensed, creating derivatives, distributing, and reproducing any and all files is prohibited. However, since it's an educational project, this doesn't mean we disallow downloading/viewing/using any of the files. You are 100% allowed to download, view, and use any and all of the files, but only for personal use. If you are to download anything from the GitHub, you can do anything you want but it must stay on your machine at all times.
Credits
Developer: Oliver Lie
Educational Material Writer: Oliver Lie
Support the Development
Here are some ways you can support the development of Saturn:
1. Ask Questions
Read through the educational materials and ask questions. Questions like "why is X implemented this way," or "what happens if we change X," would greatly help as we aim to answer them in our educational materials. Reviewing the educational materials and suggesting changes/revisions would be greatly appreciated.
2. Propose new Features
The world of SAT solving is very big and what is covered (DPLL and CDCL) is just scratching the surface. If you have an algorithm or heuristic you'd like to see implemented, let us know and we will do our best to research, implement, and report our findings.
3. Financial Support
Making a SAT solver isn't easy and it takes a lot of work, neither is writing education materials on building your own. By donating to the development of Saturn, we can invest more time in its implementation as well as its accompanying research report to make this knowledge more accessible.