I wrote this in my own way to learn about this SAT problem, and therefore there may be mistakes in the article.
There are many good publications on this topic. I consult a few pages in Handbook of Satisfiability and The Art of Computer programming, Volume 4 Fascicle 6, for the theory part, and Z3 Guide for the use of Z3.
For CDCL programming, consult this link.
For a better visual of how hard SAT is, consult The SAT Game.
This article is written for 3Blue1Brown’s SoME3. It is inspired by a nice-looking article on CPU, Ciechanowski’s visual guides and 3Blue1Brown’s videos.
The conversation style probably comes from OSTEP, despite that I have only glanced at its first pages.
In the writing, I also referred to some AI generated materials, especially those from Claude and mirror links of ChatGPT and MidJourney. Their existence can be found among various css style blocks in my project, and a concept art folder that are removed due to SoME’s policy.
The font of conversations is im-fell-dw-pica, and the font of editable notes is indie-flower. I’m also not very familiar with how to use copyrighted fonts, so tell me if that is improper.
As I am a noob both in front-end developing and in English, there may be flaws among the pages. Report them in the github repo, either by discussions or by issues. (Why isn’t there a comment bar? Because this is a static site and I don’t expect much feedback.)
fix the link below, now only rely on the HTML-style link
Of course, you can always go back to read again.