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).

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

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

play

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.

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 🤓

Thanks @michaelblau for the python frame template and @df for the awesome-frames repo, super useful

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