# Satisfiability of Mixed Horn Formulas

Porschen, Stefan and Speckenmeyer, Ewald
(2007)
*Satisfiability of Mixed Horn Formulas.*
**Published in: **
Discrete applied mathematics Vol. 155 (11).
1408 -1419.

## 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 [B. Randerath, E. Speckenmeyer, E. Boros, P. Hammer, A. Kogan, K. Makino, B. Simeone, O. Cepek, A satisfiability formulation of problems on level graphs, ENDM 9 (2001)] and graph colorability formulas.

Editorial actions: |
View Item (Login required) |
---|

ZAIK Number: | zaik2005-499 |
---|---|

Depositing User: | Stefan Porschen |

Date Deposited: | 12 Apr 2007 00:00 |

Last Modified: | 27 Oct 2011 11:54 |

URI: | http://e-archive.informatik.uni-koeln.de/id/eprint/499 |