<p>See Jan Krajicek, &quot;<a href="https://doi.org/10.1016/j.ipl.2012.03.009" rel="nofollow noreferrer">A note on SAT algorithms and proof complexity</a>&quot;, 2012</p>
<p>I am not sure if we have any result for random unsat instances (how do you define a random unsat instance?).</p>

CC BY-SA 4.0
2021-08-23T12:15:15.483Z
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.
Kaveh
CC BY-SA 4.0
2021-08-23T23:38:16.620Z
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](https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/descr.html)
Zunchen Huang
CC BY-SA 4.0
2021-08-23T12:13:52.720Z
2021-08-23T12:13:52.720Z
Kaveh
<p>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 <a href="https://core.ac.uk/download/pdf/81968133.pdf" rel="nofollow noreferrer">Lower bounds for random 3-SAT via differential equations</a> but they focused on sat instances.</p>
<p>Background: I'm interested in using SAT solver to prove a formula unsat.</p>

<sat><random-k-sat>
Lower bound for proving a random 3-SAT formula is unsat?
Zunchen Huang
# Lower bound for proving a random 3-SAT formula is unsat?

(Asked by: username_0 on 2021-08-23)

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](https://core.ac.uk/download/pdf/81968133.pdf) but they focused on sat instances.

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

**Tags:** sat, random-k-sat


---

## 1 answers

### Answer by username_1 on 2021-08-23. Score: 1

See Jan Krajicek, "[A note on SAT algorithms and proof complexity](https://doi.org/10.1016/j.ipl.2012.03.009)", 2012

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

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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](https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/descr.html)  

---

