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?
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.