Treat each clause as a set of literals. Remove repeated literals, tautological clauses, repeated clauses, and any clause containing another clause. The smaller clause already implies the larger one, so deleting the latter preserves exactly the satisfying assignments. Keep all n declared variables even if some disappear from the clauses. The resulting clauses form an antichain: none contains another. An empty clause gives count zero; no clauses gives count 2^n. For sparsification, do not propagate unit clauses by removing variables: the branch accounting keeps a fixed common variable set. This normalization is count-preserving, not merely satisfiability-preserving.