Applications of minimal unsatisfiable formulas to polynomially reduction for formulas

A conjunctive normal form (CNF) formula F is minimal unsatisfiable if F is unsatisfiable and the resulting formula removing any clause from F is satisfiable. (r,s)-CNF is a subclass of CNF in which each clause of formula has exactly r distinct literals and every variable occurs at most s times. The corresponding satisfiable problem (r,s)-SAT means that the instances are restricted in (r,s)-CNF. For positive integer r≥3, there exists a critical function f(r) such that all formulas in (r,f(r))-CNF are satisfiable, but (r,f(r)+1)-SAT is already NP-Complete. It is open whether or not the function f is computable. One can only estimate some bounds of f(r) except for f(3)=3 and f(4)=4. In this paper, the applications of minimal unsatisfiable formulas are described for transformations between CNF formulas. A new algorithm is presented to introduce less new variables in transformation from CNF to 3-CNF, which for clauses with length l(>3) only [1/2] new variables are introduced. The principle and method for transforming CNF to (r,s)-CNF and constructing unsatisfiable formulas in (r,s)-CNF are presented.