Horn maximum satisfiability: reductions, algorithms and applications

Joao Marques-Silva; Alexey Ignatiev; Antonio Morgado

doi:10.1007/978-3-319-65340-2_56

Horn maximum satisfiability: reductions, algorithms and applications

Joao Marques-Silva, Alexey Ignatiev, Antonio Morgado

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research

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 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	https://doi.org/10.1007/978-3-319-65340-2_56
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	https://web.fe.up.pt/~epia2017/

Access to Document

10.1007/978-3-319-65340-2_56

Cite this

Marques-Silva, J., Ignatiev, A., & Morgado, A. (2017). Horn maximum satisfiability: reductions, algorithms and applications. In E. Oliveira, J. Gama, Z. Vale, & H. Lopes Cardoso (Eds.), Progress in Artificial Intelligence: 18th EPIA Conference on Artificial Intelligence, EPIA 2017 Porto, Portugal, September 5–8, 2017 Proceedings (pp. 681-694). (Lecture Notes in Computer Science ; Vol. 10423 ). Springer. https://doi.org/10.1007/978-3-319-65340-2_56

Marques-Silva, Joao ; Ignatiev, Alexey ; Morgado, Antonio. / Horn maximum satisfiability : reductions, algorithms and applications. Progress in Artificial Intelligence: 18th EPIA Conference on Artificial Intelligence, EPIA 2017 Porto, Portugal, September 5–8, 2017 Proceedings. editor / Eugenio Oliveira ; Joao Gama ; Zita Vale ; Henrique Lopes Cardoso. Cham Switzerland : Springer, 2017. pp. 681-694 (Lecture Notes in Computer Science ).

@inproceedings{a5734f805b8741b0b6d330085b9f06c6,

title = "Horn maximum satisfiability: reductions, algorithms and applications",

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.",

author = "Joao Marques-Silva and Alexey Ignatiev and Antonio Morgado",

year = "2017",

doi = "10.1007/978-3-319-65340-2_56",

language = "English",

isbn = "9783319653396",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "681--694",

editor = "{ Oliveira}, Eugenio and Joao Gama and Zita Vale and {Lopes Cardoso}, Henrique",

booktitle = "Progress in Artificial Intelligence",

note = "Portuguese Conference on Artificial Intelligence 2017, EPIA 2017 ; Conference date: 05-09-2017 Through 08-09-2017",

url = "https://web.fe.up.pt/~epia2017/",

}

Marques-Silva, J, Ignatiev, A & Morgado, A 2017, Horn maximum satisfiability: reductions, algorithms and applications. in E Oliveira, J Gama, Z Vale & H Lopes Cardoso (eds), Progress in Artificial Intelligence: 18th EPIA Conference on Artificial Intelligence, EPIA 2017 Porto, Portugal, September 5–8, 2017 Proceedings. Lecture Notes in Computer Science , vol. 10423 , Springer, Cham Switzerland, pp. 681-694, Portuguese Conference on Artificial Intelligence 2017, Porto, Portugal, 5/09/17. https://doi.org/10.1007/978-3-319-65340-2_56

Horn maximum satisfiability: reductions, algorithms and applications. / Marques-Silva, Joao; Ignatiev, Alexey; Morgado, Antonio.
Progress in Artificial Intelligence: 18th EPIA Conference on Artificial Intelligence, EPIA 2017 Porto, Portugal, September 5–8, 2017 Proceedings. ed. / Eugenio Oliveira; Joao Gama; Zita Vale; Henrique Lopes Cardoso. Cham Switzerland: Springer, 2017. p. 681-694 (Lecture Notes in Computer Science ; Vol. 10423 ).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research

TY - GEN

T1 - Horn maximum satisfiability

T2 - Portuguese Conference on Artificial Intelligence 2017

AU - Marques-Silva, Joao

AU - Ignatiev, Alexey

AU - Morgado, Antonio

N1 - Conference code: 18th

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85029000186&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-65340-2_56

DO - 10.1007/978-3-319-65340-2_56

M3 - Conference Paper

SN - 9783319653396

T3 - Lecture Notes in Computer Science

SP - 681

EP - 694

BT - Progress in Artificial Intelligence

A2 - Oliveira, Eugenio

A2 - Gama, Joao

A2 - Vale, Zita

A2 - Lopes Cardoso, Henrique

PB - Springer

CY - Cham Switzerland

Y2 - 5 September 2017 through 8 September 2017

ER -

Marques-Silva J, Ignatiev A, Morgado A. Horn maximum satisfiability: reductions, algorithms and applications. In Oliveira E, Gama J, Vale Z, Lopes Cardoso H, editors, Progress in Artificial Intelligence: 18th EPIA Conference on Artificial Intelligence, EPIA 2017 Porto, Portugal, September 5–8, 2017 Proceedings. Cham Switzerland: Springer. 2017. p. 681-694. (Lecture Notes in Computer Science ). doi: 10.1007/978-3-319-65340-2_56

Horn maximum satisfiability: reductions, algorithms and applications

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this