So, the question is to know whether anything that can be verified quickly, can also be found quickly.

Is there anyone interested to work on this subject? The world believes P!=NP but I would like to bid for P=NP. Here’s my reasoning: If P != NP, then cryptography and bitcoin are an unstoppable force. However I don’t believe that such an unstoppable force (one way functions) can actually exist at this level.

So the goal is to find the missing algorithm, to solve an NP-complete problem, and steal 1 trillion in bitcoin. I’m working on it, but the algorithm still lacks some finishing touch. Is anyone interested in talking about this here?

The dark side of the force is a pathway to many abilities some consider to be unnatural

… So, according to Schaefer’s dichotomy theorem, 2SAT is in P, XOR-SAT is in P, the combination of both is NP-complete.

Starting with a formula with 2SAT clauses, in the form (A=1 or B=0) and XOR relations, in the form (A+C+D=1), we can use the XOR relations to eliminate the variables one by one and put the formula in row echelon form. In this example, we can eliminate A, the formula becomes (C+D=0 or B=0). All the XOR relations are gone, taking away 1 variable each time, and all the remaining binary clauses have a XOR relation on each side. Then from this formula, I extract exhaustively all true XOR statements, until all the variables all eliminated or there is nothing left to prove. The extraction method is of course the relevant part (too difficult for a weak jedi like Obiwan) which I’m going to keep secret for now.

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.