Smallest 3-SAT problem that no one has been able to solve?

Question

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.

Answer 1

Small and hard SAT instances in the literature typically are crafted benchmarks, instances generated specifically to exploit weaknesses of existing SAT solvers and solving methods. As such, unlike a tough Diophantine equation plucked from the mathematical firmament, the satisfiability or unsatisfiability of such crafted instances is already known. So there's no smallest instance with no known resolution. The instances are interesting only in how they highlight either the weakness of existing solver methods or a weakness in how we encode some conceptually simple problems.

Creating a smallish infeasibly hard SAT instance is relatively easy. Generate a random 3-SAT instance of 1,000 variables with a clause/variable ratio a little bit above the critical ratio to ensure the instance is unsatisfiable with high probability. You might want to avoid triangles, as in "Generating Difficult SAT Instances by Preventing Triangles", but you probably won't need to. The instance's unsatisfiability ensures there will be no lucky early termination and the variable count is high enough to push the expected runtime well beyond human lifetimes for even the best solvers.