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.