Can someone provide with the smallest (as small as possible) 3SAT example (w.r.t. number of variables and the number of equations) that is:

  1. Unsatisfiable.
  2. Not provable unsatisfiable by simply reduction (successive simplification and rewriting) of the equations by the process similar to as described below:


Assuming a 3SAT Problem that includes 4 equations:

  1. ~a + b + c = 1
  2. ~a + ~b + c = 1
  3. b + d + ~e = 1
  4. b + d + e = 1

(1. and 2.) combined can be replaced with ~a+c=1. (3. and 4.) combined can be replaced with b+d=1. and so on..

Thus, we require a problem instance where such a successive reduction/simplification of the equations (containing either 2 or 3 variables) in the given problem do not automatically lead to the conclusion of unsatisfiability.

  • $\begingroup$ What prevents you from finding such an instance? $\endgroup$ Commented May 14, 2017 at 14:06

1 Answer 1


Resolution is a complete proof system for contradictions: if a given set of clauses is contradictory, then this fact is provable using resolution.

Since Resolution exactly corresponds to your "simple reduction", it follows that your question cannot be answered.

  • $\begingroup$ Prof., if we add an additional constraint: 3) All the resultant/emergent clauses (after application of the reduction to generate new clauses) are also of size 3 or less then i assume we can generate such an example (as the true source the exponential number of clauses is eliminated). If the above is correct could you help with such an example ? $\endgroup$ Commented May 14, 2017 at 15:52
  • $\begingroup$ I am sure you can find such an example yourself, by trying out a few cases. Alternatively, you are looking for an unsatisfiable 3CNF whose Resolution width is larger than 3. $\endgroup$ Commented May 14, 2017 at 16:12
  • $\begingroup$ Thanks. I agree that generating such an example is not difficult. I was more wondering what the smallest such example can be. $\endgroup$ Commented May 14, 2017 at 16:24

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.