3
$\begingroup$

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.

$\endgroup$
1
  • 5
    $\begingroup$ 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). $\endgroup$
    – D.W.
    Oct 25, 2021 at 15:43

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ Instead of 1,000, OP could make the number variable, then generate problems with 100, 101, 102 etc variables, try to solve, record the times, and record at which size he gives up waiting. $\endgroup$
    – gnasher729
    Oct 28, 2021 at 2:55
  • $\begingroup$ Can't the unsatisfiability certificate in the Delete Resolution Asymmetric Tautologies format be short (thus allowing "lucky early termination")? $\endgroup$
    – halw
    Oct 28, 2021 at 6:40
  • $\begingroup$ I was hoping that someone did this relatively easy thing and showed the 3-SAT instance they got to their SAT solver buddies and they all couldn't solve it. $\endgroup$
    – halw
    Oct 28, 2021 at 6:41
  • $\begingroup$ @halw The DRAT proof might be short but still require exponential time to find. But given how poorly current solvers handle extended resolution or any comparably powerful proof system, the proof isn’t likely to be short either. $\endgroup$
    – Kyle Jones
    Oct 29, 2021 at 5:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.