Homomorphisms and Propositional Proofs

We have shown that the homomorphism rule for resolution systems allows exponentially shorter proofs than Krishnamurthy`s symmetry rule. We plan to study the algorithmic implications of this improvement ("proof search") and to determine the relative complexity of resolution systems with a "dynamic" version of the homomorphism rule. Parameterized Complexity provides a means for coping with computationally hard problems and provides feasible solutions for practical applications. In context of our recent results on the parameterized complexity of the satisfiability problem (SAT), the question rises whether Gallo and Scutellà`s SAT-hierarchy and its generalizations are fixed-parameter tractable. A further research objective is to investigate the relevance of concepts developed in the theory of graph homomorphisms (in particular, Nesetril`s generalization of Hajs`s Calculus) in our context of clause-set homomorphisms.