# Non-reducible Unsatisfiable 3SAT instance example

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:

Example:

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.

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

## 1 Answer

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.

• 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 ? Commented May 14, 2017 at 15:52
• 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. Commented May 14, 2017 at 16:12
• Thanks. I agree that generating such an example is not difficult. I was more wondering what the smallest such example can be. Commented May 14, 2017 at 16:24