potato-sat

potato-sat

This is a very elementary SAT solver. I wrote it for a systems design course at my university in which we dealt a lot with formal verification (where solving SAT of course plays a huge role).

As a basic SAT solver, it works well enough. The course resulted in another small project that converted sudoku puzzles into boolean expressions (specifically in CNF written to DIMACS files). Using that tool potato-sat could be used to solve regular sudoku puzzles very nicely. But as their size increases, complexity of course explodes. And as I didn't get very far in implementing the SAT-solving improvements people have come up with since the sixties, my little solver is basically stuck back then and even on modern hardware is quickly overwhelmed by a bigger expression.

As you can tell from the little logo I made for it, I had a lot of fun with this project and learned a lot, especially as it was my first real C++ project.

potato-sat logo

Eventually™ I'll get back to this project, dig out my old notes from the course, and really implement it all properly. :^)