1
$\begingroup$

Let we have a 3CNF under following restriction: each variable occurs 3 times.

Then I apply generalized resolution (GR) (I don't know which name would fit more) technique (number of clauses can be arbitrary large, just an example):

$(x\lor A)\land(x\lor B)\land(\overline x\lor C)=(A\lor C)\land(B\lor C)$. Here $A,B,C$ are some clauses. Neither $A$ and $C$ nor $B$ and $C$ have opposing literals (like in original resolution, the reason is not to exponentially increase length of formula).

Is it an open problem if there is such a sequence of choices (which variable to choose for GR) that will return 'NO' if formula is unsatisfiable? Or there is a proof that some unsatisfiable formulas (with given restrictions) have no such sequences? Meaning that for every pair of literals $x,y$ on some step it will be possible to find a clause $(A\lor x\lor y)\land(B\lor\overline x\lor\overline y)$.

We assume that we can use any known polynomial technique such as unit propagation, absorption rules $(x\lor A)\land(\overline x\lor A)=A; A\land(x\lor A)=A$, pure literal rule (if variable always occur as positive or negative, remove all clauses where it is contained), changing equal literals, finding strongly connected components in a graph for 2-clauses, etc.

$\endgroup$
  • $\begingroup$ Resolution's completeness guarantees that once you've used it to reduce the formula to monotone form you will have produced an empty clause iff the formula is unsatisfiable. So you can always use it to determine satisfiability. $\endgroup$ – Kyle Jones Aug 31 '17 at 1:33
  • $\begingroup$ @KyleJones, of course, but I don't know if we always can find such a sequence of choices (or another that will give an opposing singletons, as example). Or every formula is reducible to monotone using this trick? $\endgroup$ – rus9384 Aug 31 '17 at 1:36
  • $\begingroup$ I guess I'm not understanding what you're asking because the simplest way to go about it is 1) choose any variable that appears both positively and negatively in the formula and apply resolution to all such pairs of clauses. 2) keep the resulting resolvent clauses and discard the original clauses you used in the resolutions, which you can do without affecting satisfiability. Repeat 1 and 2 until there are no more variables that appear both positively and negatively in the formula. This process works for any CNF formula, and looks like exactly what you did with x, A, B, and C above. $\endgroup$ – Kyle Jones Aug 31 '17 at 1:45
  • $\begingroup$ @KyleJones, we can't apply resolution here: $(x\lor y\lor z)\land(\overline x\lor\overline y\lor\overline z)$. So, I don't understand how we can apply GR in any formula. $\endgroup$ – rus9384 Aug 31 '17 at 1:48
  • $\begingroup$ You can apply the rule, you just end up with a tautology, which isn't an empty clause, so the formula is satisfiable. $\endgroup$ – Kyle Jones Aug 31 '17 at 1:54
2
$\begingroup$

Resolution is refutation-complete. This means that if $S$ is a set of unsatisfiable clauses, then you can use resolution to derive the empty clause. Moreover, Resolution is sound, so you can only derive the empty clause if $S$ is unsatisfiable. Summarizing, given a set $S$ of clauses, you can use Resolution to derive the empty clause if and only if $S$ is unsatisfiable.

Unfortunately, sometimes generating the empty clause takes an exponential number of steps. Let $G$ be a random 4-regular graph on an odd number of vertices $n$, and let us associate with each of the $2n$ edges a variable. Consider the set of $\Theta(n)$ clauses stating that for every vertex, the XOR of the four variables corresponding to edges touching the vertex is 1. Since the number of vertices is odd, this set of clauses, known as a Tseitin contradiction, is unsatisfiable. Urquhart showed that with high probability, any Resolution refutation of this set of clauses has $2^{\Omega(n)}$ many lines (i.e., clauses); see Jakob Nordström's lecture notes.

$\endgroup$
  • $\begingroup$ Yet that probability is not 100%? But there exist formulas for which that probability is 100%, is that correct? $\endgroup$ – rus9384 Aug 31 '17 at 9:27
  • $\begingroup$ The probability is over the choice of the formula. For most graphs the resulting formula will require an exponentially long Resolution refutation. You can also construct explicit graphs for which this holds. $\endgroup$ – Yuval Filmus Aug 31 '17 at 9:30
  • $\begingroup$ To stress the point, once we fix the formula, there is nothing probabilistic going on any more. $\endgroup$ – Yuval Filmus Aug 31 '17 at 9:32
  • $\begingroup$ Resolution runtime is independent on order of applying it? $\endgroup$ – rus9384 Aug 31 '17 at 9:49
  • $\begingroup$ The lower bound is on the number of lines in any resolution refutation. I don't care how you generate the refutation. I only charge you for the number of lines in the resulting proof. $\endgroup$ – Yuval Filmus Aug 31 '17 at 9:51

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.