Horn maximum satisfiability: reductions, algorithms and applications

Joao Marques-Silva, Alexey Ignatiev, Antonio Morgado

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearch

10 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProgress in Artificial Intelligence
Subtitle of host publication18th EPIA Conference on Artificial Intelligence, EPIA 2017 Porto, Portugal, September 5–8, 2017 Proceedings
EditorsEugenio Oliveira, Joao Gama, Zita Vale, Henrique Lopes Cardoso
Place of PublicationCham Switzerland
PublisherSpringer
Pages681-694
Number of pages14
ISBN (Electronic)9783319653402
ISBN (Print)9783319653396
DOIs
Publication statusPublished - 2017
Externally publishedYes
EventPortuguese Conference on Artificial Intelligence 2017 - Porto, Portugal
Duration: 5 Sept 20178 Sept 2017
Conference number: 18th
https://web.fe.up.pt/~epia2017/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10423
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferencePortuguese Conference on Artificial Intelligence 2017
Abbreviated titleEPIA 2017
Country/TerritoryPortugal
CityPorto
Period5/09/178/09/17
Internet address

Cite this