1
$\begingroup$

For a random 3-CNF formula with n variables and m clauses, assume this formula is unsat, what is the lower bound for proving it to be unsat? Some results posted in Lower bounds for random 3-SAT via differential equations but they focused on sat instances.

Background: I'm interested in using SAT solver to prove a formula unsat.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

See Jan Krajicek, "A note on SAT algorithms and proof complexity", 2012

I am not sure if we have any result for random unsat instances (how do you define a random unsat instance?).

Improve this answer
$\endgroup$
2
  • $\begingroup$ We were at a BRIS workshop in 2012 with a bunch of proof complexity folks and lowerbounds for unsat insurances came up as an open problem. Jan couldn't attend the workshop. The following week we returned to Prague and were having launch with Jan and mentioned this problem. Jan was surprised that was open and wrote the paper over the weekend. $\endgroup$
    – Kaveh
    Commented Aug 23, 2021 at 12:15
  • $\begingroup$ Wow that's an interesting story :) P.S. Suppose we use uniform random-3-SAT and draw n instances from them. Is it reasonable/sufficient to say that the unsat ones in them are random unsat instances? If not, what could be wrong. Cite from here: Uniform Random-3-SAT $\endgroup$
    – hddmss
    Commented Aug 23, 2021 at 23:38

Your Answer

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

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