0
$\begingroup$

Let we have a formula $\varphi(x_1,x_2...x_k)$. Now we apply a refutation method: $\varphi(x_1,x_2...x_k)\Leftrightarrow(\varphi(x_1=1,x_2...x_k)\lor\varphi(x_1=0,x_2...x_k))$. Latter formula seems to be longer, but no, good algorithm reduces number of literal occurences. On each step we can modify the formula without changing it's solution space. This gives much more power than resolution has. For example, Tseytin contradiction can be refuted this way in linear time using deterministic algorithm.

But what is the worst case for this algorithm?

Example:

$$\varphi=(x\lor y\lor z)(x\lor\overline y\lor t)(x\lor\overline z\lor\overline v)(\overline x\lor\overline t\lor\overline v)(\overline x\lor\overline z\lor v)(y\lor\overline z\lor v)(\overline y\lor\overline t\lor\overline v)\land(\overline y\lor z\lor t)$$

Step 1. Getting rid of $t$.

Putting $t$. Affected remaining clauses: $(\overline x\lor\overline v)(\overline y\lor\overline v)$. Reducing them: $\overline v\lor \overline x\overline y$.

Putting $\overline t$. Affected remaining clauses: $(x\lor\overline y)(\overline y\lor z)$. Reducing them: $\overline y\lor xz$.

Combining them using OR: $\overline v\lor\overline y\lor xz$.

Step 2. Getting rid of $y$.

Putting $y$. Affected subformula: $\overline v\lor xz$.

Putting $\overline y$. Affected subformula: $(x\lor z)(\overline z\lor v)$.

Combining them: $\overline v\lor xz\lor(x\lor z)(\overline z\lor v)$. Reduction: $x\lor z\lor\overline v$.

Step 3. Getting rid of $x$.

Putting $x$. Affected subformula: $\overline z\lor v$.

Putting $\overline x$. Affected subformula: $(z\lor \overline v)(\overline z\lor\overline v)$. Reduction: $\overline v$.

Combining them: $1$.

All clauses are covered, formula is satisfiable.

But what would be the hardest case for this and is it possible to break exponential bound using this method? Is this method general enough (we can modify formula by any ways until solution space is unchanged and this is checkable in polynomial time) that saying it requires superpolynomial time (for unsatisfiable formula) will imply $\mathsf{NP\ne coNP}$?

Note that for unsatisfiable formula it's possible to non-deterministically ignore some clauses if refutation can be done without their usage.

$\endgroup$
1
$\begingroup$

The worst case is exponential. Each time you apply your method to a single variable, you are potentially doubling the size of the formula. You might need to apply this to each of the $k$ variables, so the size of the formula might blow up by a factor of $2^k$. In other words, the running time of this algorithm could potentially be exponential.

What you have described is basically a variation on the DPLL algorithm. The DPLL algorithm picks an variable, say $x_1$, sets it first to true, simplifies, and tests satisfiability of that; then sets it to false, simplifies, and tests satisfiability of that. That's very similar to what you are doing. An important choice here is exactly what simplification we do; you didn't describe that explicitly, but you can find a description of the specific simplifications that are done in the DPLL algorithm can be found in any good reference on DPLL. DPLL is probably better than your method because it separately simplifies $\phi(0,x_2,\dots,x_k)$ and simplifies $\phi(1,x_2,\dots,x_k)$, which is potentially easier than simplifying the combined formula $\phi(0,x_2,\dots,x_k) \lor \phi(1,x_2,\dots,x_k)$ (depending on what simplification rules you use).

$\endgroup$
  • $\begingroup$ I would argue that DPLL is not better because mine on the first step reduces 3CNF formula to $(2SAT_1\lor2SAT_2)\land(3SAT)$. Then it tries to assign variables occuring in those 2SAT's. It is trivial, that formula gets shorter on each step as well as number of OR gates potentially increases. Also, DPLL is not non-deterministic. $\endgroup$ – rus9384 Sep 14 '17 at 0:56

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.