# Horn Maximum Satisfiability: Reductions, Algorithms & Applications

arXiv: https://arxiv.org/abs/1705.05335 · HTML: https://mlsanity.com/paper/1705.05335/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 May 2017.

## Built on by (most cited first, 1 of 1)

- [The Horn Non-Clausal Class and its Polynomiality](https://mlsanity.com/paper/2108.13744/) (2021)

## Abstract (arXiv)

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.