Recent years have witnessed 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 HornMaxSAT. Furthermore, the paper also shows how linear time decision procedures for Horn formulas can be used for developing novel algorithms for the HornMaxSAT problem.
CITATION STYLE
Marques-Silva, J., Ignatiev, A., & Morgado, A. (2017). Horn maximum satisfiability: Reductions, algorithms and applications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10423 LNAI, pp. 681–694). Springer Verlag. https://doi.org/10.1007/978-3-319-65340-2_56
Mendeley helps you to discover research relevant for your work.