1
$\begingroup$

I have a CNF formula like $(x_1∨x_2∨x_3') ∧ (x_1' ∨ x_4 ∨ x_2)$ ...

Perhaps I want to see if the equation is equivalent to a CNF equation containing a single literal ($x_2$ for example).

I already know I can get there eventually by going through every existing predicate resolution. Meaning if I look at the two clauses in the above example, I can add the following clause to the equation without changing the truth values: $(x_2 ∨ x_4 ∨ x_3')$.

Doing this with the right combination of variables will create two literal clauses, and eventually one literal clauses that can be added again while maintaining the same truth values.

Is there any other way in CNF to find new clauses that hold this property?

$\endgroup$
4
  • $\begingroup$ $x_2$ satisfies the formula, but so does $x_1 \land x_4$. As does $x'_1 \land x'_3$. For your formula to be true, only one disjunct in each conjunct need be true. $\endgroup$
    – amWhy
    Jan 30, 2020 at 4:49
  • $\begingroup$ I’m not really interested in proving satisfiability here, I’m just interested in generating CNF clauses that both have fewer literals and don’t effect the truth table of the original equation $\endgroup$
    – ian.p.swift
    Jan 30, 2020 at 15:50
  • $\begingroup$ This is not a full answer, however if $x_2$ appears in at least 2 disjunctive clauses, you can remove it from all other disjunctive clauses. This is because $x_2\lor(x_2\land x_n)=x_2$. $\endgroup$
    – user400188
    Jun 4, 2020 at 9:39
  • $\begingroup$ I recall if you apply resolution with all possible combinations of clauses involving a the same single literal. Then you can get to erase that literal to produce another formula that is eqisatisfiable to the original. Your formula size will explode exponentially to erase that literal unfortunately. Not sure if some clever data structures can help with explosive number of clauses. $\endgroup$
    – clinux
    Jun 23 at 6:42

1 Answer 1

Reset to default
0
$\begingroup$

I seem to recall that if you apply resolution with all possible combination of clauses contain a certain literal at once, you can produce a new formula that is equisatisfiable to the original formula. However the number of clauses explodes exponentially unfortunately. (Number of clauses gets squared.)

Example:

$(D∨C)∧(D'∨A∨B')∧(D'∨A'∨B')∧(D'∨A'∨B)∧(D∨A)$

Now combine clauses containing $D$ / $D'$ in all possible ways to erase the $D$ literal which constructs the following formula that is equisatisfiable to the original formula.

$(A∨B'∨C)∧(A'∨B'∨C)∧(A'∨B∨C)∧(A∨B')$

Now combine $A$ / $A'$:

$(B'∨C)$

That final formula is obviously satisfiable. So the original formula should be satisfiable too. We first erased $D$, then erased $A$ in that example.

$\endgroup$

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.