"Satisfiability of Mixed Horn Formulas"
Technical report by Stefan Porschen, Ewald Speckenmeyer, available as BibTeX Source.
Zentrum für Angewandte Informatik Köln, Lehrstuhl Speckenmeyer
Preprint Key:	zaik2005-499
Keywords:	(hidden) Horn formula, (weighted) satisfiability, fixed parameter tractability, minimal vertex cover, Hornformula>q-Horn formula, quadratic formula
MSC codes:	03B05, 68Q25
This technical report has 18 pages, was written in January 2005, it has not been published.
Abstract:	In this paper the class of {em mixed Horn formulas} is introduced that contain a Horn part and a 2-CNF (also called quadratic) part. We show that SAT remains NP-complete for such instances and also that any CNF formula can be encoded in terms of a mixed Horn formula in polynomial time. Further, we provide an exact deterministic algorithm showing that SAT for mixed Horn formulas containing n variables is solvable in time O(2^{0.5284n}). A strong argument showing that it is hard to improve a time bound of O(2^{n/2}) for mixed Horn formulas is provided. We also obtain a fixed-parameter tractability classification for SAT restricted to mixed Horn formulas C of at most k variables in its positive 2-CNF part providing the bound O(|C|2^{0.5284k}). We further show that the NP-hard optimization problem minimum weight SAT for mixed Horn formulas can be solved in time O(2^{0.5284n}) if non-negative weights are assigned to the variables. Motivating examples for mixed Horn formulas are level graph formulas cite{speck} and graph colorability formulas.