Don’t take offense, but the argument about “unstoppable force” is more of philosophical consequence than a practical one.
This topic is highly academic, and is about computer science (which is not the same as programming). There are way too many failed attempts by top-tier researchers, many attempts in the queue for revision, and is way, way, beyond what we can achieve here (in the sense that people around here tend to be more interested about sharping their coding skills, programming bots and such than in such highly theoretical topics). If someone’s going to settle it, it will be Andrew Wiles style, with almost an entire lifetime of dedication, and with people force-feeding this person. Chances are the final proof (in either direction) will be 200+ pages long of heavy mathematics and without a single line of code.
What you say about 2SAT and XOR-SAT (and, to that matter, also Horn-SAT) breaks down in spectacular fashion when you upgrade to 3SAT. There you’ll find the real beast, and the approaches for solving 2SAT (either using resolution or causal graphs) no longer work.
[EDIT]: if you really want to pursue this endeavor, I warn you that this is not a weekend Arduino project. If you want people to work with you on this, I’d suggest researchgate. There you’ll find the most recent research on the topic, and people willing to share their findings with you. If you take this route, I’d advise you to make everything in you education and work (and probably your personal life too) revolve around this particular topic: if you’re going to uni, make you bachelor’s projects and thesis be about it, do a Ph.D/postdoct on the topic, and so on.