# Horn Maximum Satisfiability: Reductions, Algorithms & Applications

## TL;DR

This paper explores Horn MaxSAT, demonstrating its broad applicability to various problems, and introduces new algorithms leveraging linear-time decision procedures for Horn formulas.

## Contribution

It introduces the study of Horn MaxSAT, showing its relevance to many problems and developing algorithms based on Horn formulas' decision procedures.

## Key findings

- Horn MaxSAT can model many optimization and decision problems.
- Linear-time decision procedures for Horn formulas enable new algorithms for Horn MaxSAT.
- The paper bridges Horn formulas and MaxSAT solving techniques.

## Abstract

Recent years have witness remarkable performance improvements in maximum satisfiability (MaxSAT) solvers. In practice, MaxSAT algorithms often target the most generic MaxSAT formulation, whereas dedicated solvers, which address specific subclasses of MaxSAT, have not been investigated. This paper shows that a wide range of optimization and decision problems are either naturally formulated as MaxSAT over Horn formulas, or permit simple encodings using Horn MaxSAT. Furthermore, the paper also shows how linear time decision procedures for Horn formulas can be used for developing novel algorithms for the Horn MaxSAT problem.