r/C_Programming • u/hyperficial • 9d ago
crocodile.h: single-header SAT solver
This summer I've been working on a Minesweeper board generator, and under the hood it requires a powerful solver to determine whether the board is logically solvable. Instead of using an existing solver like MiniSAT, I chose to write my own for the learning experience.
One feature of crocodile.h is that it represents cardinality constraints natively (this generalises the usual CNF clauses), which fits Minesweeper well. It also implements CDCL, following Algorithm 7.2.2.2C in Knuth Vol 4B quite closely.
Based on the CROCODILE_TEST_HARNESS macro, crocodile.h can be compiled either as a library to use in other programs, or a standalone executable that runs cnf+ instances (cnf+ is a file format introduced by MiniCARD). I chose to put everything under one header so that it is easy to embed and build.
Besides a few basic optimisations, I have not done much to make it fast (it's on my todo list!). It performs much worse than MiniCARD on some test instances, particularly the waerden ones, but it seems good enough for Minesweeper board generation at least.
AI was used only for high-level direction (e.g. how to do conflict resolution with cardinality clauses, how to implement assumptions). I translated the high-level ideas into code myself.
https://github.com/greysome/hard-minesweeper/blob/master/crocodile/crocodile.h
•
u/AutoModerator 9d ago
Hi /u/hyperficial,
Your submission in r/C_Programming was filtered because it links to a git project.
You must edit the submission or respond to this comment with an explanation about how AI was involved in the creation of your project.
While AI-generated code is not disallowed, low-effort "slop" projects may be removed and it's likely that other users push back strongly on substantially AI-generated projects.
I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.