Homomorphisms of Conjunctive Normal FormsDiscrete Applied Mathematics vol. 130 no. 2, pp. 351-365, 2003. Download: [paper ps] [paper pdf] Abstract:We study homomorphisms of propositional formulas in CNF generalizing symmetries considered by Krishnamurthy. If f:H->F is a homomorphism, then unsatisfiability of H implies unsatisfiability of F. Homomorphisms from F to a subset F' of F (endomorphisms) are of special interest, since in such case F and F' are satisfiability-equivalent. We show that smallest subsets F' of a formula F for which an endomorphism f:H->F exists are mutually isomorphic. Furthermore, we study connections between homomorphisms and autark assignments.We introduce the concept of proof by homomorphism which is based on the observation that there exist sets Gamma of unsatisfiable formulas such that (i) formulas in Gamma can be recognized in polynomial time, and (ii) for every unsatisfiable formula F there exist some H in Gamma and a homomorphism f:H->F. We identify several sets Gamma of unsatisfiable formulas satisfying (i) and (ii) for which proofs by homomorphism w.r.t. Gamma and tree resolution proofs can be simulated by each other in polynomial time. [back to Stefan Szeider's homepage] |