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.

Improve this question
$\endgroup$
14
  • $\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, 2017 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, 2017 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, 2017 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, 2017 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, 2017 at 1:54

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
10
  • $\begingroup$ Yet that probability is not 100%? But there exist formulas for which that probability is 100%, is that correct? $\endgroup$
    – rus9384
    Aug 31, 2017 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, 2017 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, 2017 at 9:32
  • $\begingroup$ Resolution runtime is independent on order of applying it? $\endgroup$
    – rus9384
    Aug 31, 2017 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, 2017 at 9:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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