# Fastest method of CNF equation solution verification

I am trying to find a way to mine bitcoin faster than an ASIC by using a CNF representation of sha(sha(hash)), which would be an equation containing a few hundred thousand clauses, let's call it n clauses. If I brute-force guess and check solutions, what is the fastest way to check if a given solution satisfies the equation? Currently my best idea is either a linear check $$O(n)$$ or put all the clauses in a treap which (might?) be $$O(\log n)$$, but I figure there must be standard methods for doing this that I can't find online.

Other question, I get that CNF-sat is NP, but is CNF-unsat (knowing there is/isn't a solution, but not knowing what a solution is) also NP?

• You might want to try these questions from cstheory-SE. General wisdom is that SAT theory can only break weak crypto. But then general wisdom is only mostly always right.
– fgrieu
Sep 20, 2022 at 16:53

## 1 Answer

You are asking about the algorithmic complexity of verifying a SAT solution with m clauses. Obviously if n is fixed and small, you can verify any solution in O(1) time-- just use a lookup table! So, let's assume that n is fixed but too large for a lookup table. Your CNF formula can be written as a 3-SAT problem so any clause can be checked in constant time.

Assuming no redundant clauses, you have to visit every clause so you won't be able to do better than O(m).

As for how to actually check solutions, the way you do it is you'd assign values to the variables representing the hash input. Then all other variables in your CNF would be solved through propagation for a valid input (and propagate to a conflicting state for an invalid input). A SAT solver does this by keeping track of which literals remain that can satisfy each clause and when only one literal remains due to the others being assigned the other way, the one literal that remains must be in the solution (see "watched literals").

Knowing there is a solution is as hard (in a complexity theoretical sense) as finding one. If you can tell a formula is unsat, you can use that to find a solution: just assign each variable a value and if at any step that makes the problem UNSAT, invert your assignment. This takes X steps where X is the number of variables. So if you had a polynomial UNSAT finder for x variables, you'd have a polynomial time solution finder that's x times slower and so still polynomial time (just one degree higher).