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?