(extended comment) the "preprocessing" you mention is covered by several standard algorithms. see unit propagation/pure literal elimination in DPLL algorithm & the Quine-Mccluskey CNF minimization algorithm (somewhat more studied in EE context than CS) where pairs of minterms with Hamming distance 1 are combined to find prime implicants. next, essential prime implicants are found. however finding essential prime implicants in the latter algorithm leads to another NP complete minimum set cover problem. most SAT solvers use heuristics for the CNF preprocessing/minimization although some implement the complete/optimal Quine-Mcclusky minimization on demand, which can succeed only for small formulas—the enumeration of all prime implicants can result in "exponential blowup" in size.

see also Shortest Equivalent CNF Formula tcs.se which has refs & defines its complexity class etc.

(extended comment) the "preprocessing" you mention is covered by several standard algorithms. see unit propagation/pure literal elimination in DPLL algorithm & the Quine-Mccluskey CNF minimization algorithm (somewhat more studied in EE context than CS) where pairs of minterms with Hamming distance 1 are combined to find prime implicants. next, essential prime implicants are found. however finding essential prime implicants in the latter algorithm leads to another NP complete minimum set cover problem. most SAT solvers use heuristics for the CNF preprocessing/minimization although some implement the complete/optimal Quine-Mcclusky minimization on demand, which can succeed only for small formulas—the enumeration of all prime implicants can result in "exponential blowup" in size.

see also Shortest Equivalent CNF Formula tcs.se which has refs & defines its complexity class etc.

(extended comment) the "preprocessing" you mention is covered by several standard algorithms. see unit propagation/pure literal elimination in DPLL algorithm & the Quine-Mccluskey CNF minimization algorithm where pairs of minterms with Hamming distance 1 are combined to find prime implicants. next, essential prime implicants are found. however finding essential prime implicants in the latter algorithm leads to another NP complete minimum set cover problem. most SAT solvers use heuristics for the CNF preprocessing/minimization although some implement the complete Quine-Mcclusky minimization on demand, which can succeed only for small formulas.

see also Shortest Equivalent CNF Formula tcs.se which has refs & defines its complexity class etc.

(extended comment) the "preprocessing" you mention is covered by several standard algorithms. see unit propagation/pure literal elimination in DPLL algorithm & the Quine-Mccluskey CNF minimization algorithm (somewhat more studied in EE context than CS) where pairs of minterms with Hamming distance 1 are combined to find prime implicants. next, essential prime implicants are found. however finding essential prime implicants in the latter algorithm leads to another NP complete minimum set cover problem. most SAT solvers use heuristics for the CNF preprocessing/minimization although some implement the complete/optimal Quine-Mcclusky minimization on demand, which can succeed only for small formulas—the enumeration of all prime implicants can result in "exponential blowup" in size.

see also Shortest Equivalent CNF Formula tcs.se which has refs & defines its complexity class etc.