karmacoma pfp
karmacoma
@karma
Play it while it's hot: SAT or NOT. The first frame game where *you* figure out if a random 3SAT instance is satisfiable (or not). https://sat-or-not.onrender.com
21 replies
49 recasts
125 reactions

karmacoma pfp
karmacoma
@karma
3SAT is an instance of the Boolean Satisfiability Problem, where each clause has 3 terms. Sounds simple, but it's actually an NP-complete problem. You get a formula made of boolean terms a, b, c and their negation, and you need to figure out if there is an assignment that makes the formula true aka SATisfiable
1 reply
0 recast
4 reactions

karmacoma pfp
karmacoma
@karma
Some technical details: - written in Python with FastAPI and Z3 as a solver backend - hosted on Render - everytime you hit /play, you get a fresh new random 3SAT instance generated and rendered on the fly - in /verify, Z3 checks your answer
1 reply
0 recast
3 reactions

karmacoma pfp
karmacoma
@karma
If you play a couple rounds, you will quickly realize that almost every generated problem is SAT (spoiler alert I guess). My intention was to generate 50-50 SAT/UNSAT, but it would actually require a lot more clauses. 18 to be exact, not very game like.
1 reply
1 recast
2 reactions

karmacoma pfp
karmacoma
@karma
With the current settings, problems have a 98.6% probability of being SAT. Make sure to take a screenshot if you get a rare UNSAT 🤓
1 reply
0 recast
3 reactions

karmacoma pfp
karmacoma
@karma
Thanks @michaelblau for the python frame template and @df for the awesome-frames repo, super useful
0 reply
0 recast
3 reactions