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 language | English |
---|---|
Title of host publication | Progress in Artificial Intelligence |
Subtitle of host publication | 18th EPIA Conference on Artificial Intelligence, EPIA 2017 Porto, Portugal, September 5–8, 2017 Proceedings |
Editors | Eugenio Oliveira, Joao Gama, Zita Vale, Henrique Lopes Cardoso |
Place of Publication | Cham Switzerland |
Publisher | Springer |
Pages | 681-694 |
Number of pages | 14 |
ISBN (Electronic) | 9783319653402 |
ISBN (Print) | 9783319653396 |
DOIs | |
Publication status | Published - 2017 |
Externally published | Yes |
Event | Portuguese Conference on Artificial Intelligence 2017 - Porto, Portugal Duration: 5 Sept 2017 → 8 Sept 2017 Conference number: 18th https://web.fe.up.pt/~epia2017/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 10423 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | Portuguese Conference on Artificial Intelligence 2017 |
---|---|
Abbreviated title | EPIA 2017 |
Country/Territory | Portugal |
City | Porto |
Period | 5/09/17 → 8/09/17 |
Internet address |