# Is there an instance of 3-SAT in less than 100 variables that no one has been able to solve?

In number theory, progress is sometimes guided by people stating a specific Diophantine equation that they don't know how to solve. Is there anything similar in the field of Boolean satisfiability?

More specifically, is there an instance of $$3$$-SAT in less than $$100$$ variables that people have tried to solve (by exhibiting a satisfiability or an unsatisfiability certificate) but no one has succeeded?

• From wikipedia reference: The hypothesis states that 3-SAT (or any of several, but not all, NP-complete problems) cannot be solved in subexponential time in the worst case. The exponential time hypothesis, if true, would imply that P ≠ NP... If the exponential time hypothesis is true, then 3-SAT would not have a polynomial time algorithm, and therefore it would follow that P ≠ NP.. So clearly 3-SAT problem in less than 100 variables is solvable at worst as a NP-hard problem. In practice resolution method is more efficient... Oct 11, 2021 at 18:45
• Find a 100-bit input that, when hashed twice with SHA-256, produces a value in which the topmost 98 bits are zero. The combined compute power of all the world's bitcoin miners currently takes roughly 10 minutes to solve the 76-bit version of this problem; the 98-bit version would take them around 100 years. Oct 13, 2021 at 5:31
• @j_random_hacker You can't describe that as a 3SAT instance with <= 100 variables. Oct 14, 2021 at 13:13
• @Tyilo: Ah, it could be expressed as a general SAT problem with 100 variables, but probably many of the clauses would have more than 3 literals, so the restriction to 3SAT would require extra "intermediate" variables to be introduced to express those clauses. After reencoding clauses this way, I don't know how many of the 100 variables will be still available to allocate to genuine input bits -- if it's much less than 76, then the problem is arguably solvable. Oct 15, 2021 at 5:08
• It's not even describable as a SAT problem with 100 variables, even if you allow arbitrarily many literals per clause. The problem is that the transformation from CircuitSAT to SAT via Tseytin's transform introduces one variable per wire in the circuit (i.e., per intermediate value), which will blow up the number of variables far above 100.
– D.W.
Oct 24, 2021 at 22:26

I don't think such a 100-variable 3-SAT problem exists. PPSZ can solve satisfiable 3-SAT problems in ~ $$O(1.321^n)$$, which equates to well under 2 trillion decisions for a 100-variable 3-SAT problem. A simple PC hardware setup ought to be able to work through that in a year or two. This is a lot of time (but not much trouble) to grind through a problem no one really cares about, but it is certainly doable. Most 100-variable 3-SAT problems are going to be much, much easier than that to solve, so creating a small instance of that difficulty would be the interesting part.