# Smallest 3-SAT problem 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 what is the smallest 3-SAT instance (measured by fewest number of variables) that people have tried to solve (by exhibiting a satisfiability or an unsatisfiability certificate) but no one has succeeded in solving either way?

If one could do $$10^{30}$$ operations per second (which I assume won't be possible for a long time) and if there was a 3-SAT algorithm with performance of $$1.1^n$$ (which I assume won't be available for a long time) then for $$n=1000$$ it would run for a millennium or so, so it seems plausible there might exist a concrete example of a 3-SAT instance with 1000 variables that no one knows how to solve. As indicated at Is there an instance of 3-SAT in less than 100 variables that no one has been able to solve?, it seems unlikely that such an instance exists for $$n=100$$, so it is likely that the smallest such instance uses more than 100 variables.

• Rather than posting multiple variants of this question with different values of the constant (100, 1000, etc.), I suspect it would be better to ask a question that is more general -- e.g., to ask about what is the smallest 3SAT instance that people have tried to solve and not succeeded (if any).
– D.W.
Oct 25 '21 at 15:43