2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ What prevents you from finding such an instance? $\endgroup$ – Yuval Filmus May 14 '17 at 14:06
6
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\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$ – TheoryQuest1 May 14 '17 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$ – Yuval Filmus May 14 '17 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$ – TheoryQuest1 May 14 '17 at 16:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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