Core-boosted linear search for incomplete MaxSAT

Jeremias Berg, Emir Demirović, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

Abstract

Maximum Satisfiability (MaxSAT), the optimisation extension of the well-known Boolean Satisfiability (SAT) problem, is a competitive approach for solving NP-hard problems encountered in various artificial intelligence and industrial domains. Due to its computational complexity, there is an inherent tradeoff between scalability and guarantee on solution quality in MaxSAT solving. Limitations on available computational resources in many practical applications motivate the development of complete any-time MaxSAT solvers, i.e. algorithms that compute optimal solutions while providing intermediate results. In this work, we propose core-boosted linear search, a generic search-strategy that combines two central approaches in modern MaxSAT solving, namely linear and core-guided algorithms. Our experimental evaluation on a prototype combining reimplementations of two state-of-the-art MaxSAT solvers, PMRES as the core-guided approach and LinSBPS as the linear algorithm, demonstrates that our core-boosted linear algorithm often outperforms its individual components and shows competitive and, on many domains, superior results when compared to other state-of-the-art solvers for incomplete MaxSAT solving.

Original languageEnglish
Title of host publicationIntegration of Constraint Programming, Artificial Intelligence, and Operations Research
Subtitle of host publicationand Operations Research 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings
EditorsLouis-Martin Rousseau, Kostas Stergiou
Place of PublicationCham Switzerland
PublisherSpringer
Pages39-56
Number of pages18
ISBN (Electronic)9783030192129
ISBN (Print)9783030192112
DOIs
Publication statusPublished - 2019
EventInternational Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019
- Thessaloniki, Greece
Duration: 4 Jun 20197 Jun 2019
Conference number: 16th
https://cpaior2019.uowm.gr/

Publication series

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

Conference

ConferenceInternational Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019
Abbreviated titleCPAIOR 2019
CountryGreece
CityThessaloniki
Period4/06/197/06/19
Internet address

Keywords

  • Core-guided MaxSat
  • Incomplete solving
  • Linear algorithm
  • Maximum Satisfiability
  • MaxSAT
  • SAT-based MaxSAT

Cite this

Berg, J., Demirović, E., & Stuckey, P. J. (2019). Core-boosted linear search for incomplete MaxSAT. In L-M. Rousseau, & K. Stergiou (Eds.), Integration of Constraint Programming, Artificial Intelligence, and Operations Research: and Operations Research 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings (pp. 39-56). (Lecture Notes in Computer Science ; Vol. 11494 ). Cham Switzerland: Springer. https://doi.org/10.1007/978-3-030-19212-9_3
Berg, Jeremias ; Demirović, Emir ; Stuckey, Peter J. / Core-boosted linear search for incomplete MaxSAT. Integration of Constraint Programming, Artificial Intelligence, and Operations Research: and Operations Research 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings. editor / Louis-Martin Rousseau ; Kostas Stergiou. Cham Switzerland : Springer, 2019. pp. 39-56 (Lecture Notes in Computer Science ).
@inproceedings{573590cbbcc5474e8d5cfd0dba4fda3d,
title = "Core-boosted linear search for incomplete MaxSAT",
abstract = "Maximum Satisfiability (MaxSAT), the optimisation extension of the well-known Boolean Satisfiability (SAT) problem, is a competitive approach for solving NP-hard problems encountered in various artificial intelligence and industrial domains. Due to its computational complexity, there is an inherent tradeoff between scalability and guarantee on solution quality in MaxSAT solving. Limitations on available computational resources in many practical applications motivate the development of complete any-time MaxSAT solvers, i.e. algorithms that compute optimal solutions while providing intermediate results. In this work, we propose core-boosted linear search, a generic search-strategy that combines two central approaches in modern MaxSAT solving, namely linear and core-guided algorithms. Our experimental evaluation on a prototype combining reimplementations of two state-of-the-art MaxSAT solvers, PMRES as the core-guided approach and LinSBPS as the linear algorithm, demonstrates that our core-boosted linear algorithm often outperforms its individual components and shows competitive and, on many domains, superior results when compared to other state-of-the-art solvers for incomplete MaxSAT solving.",
keywords = "Core-guided MaxSat, Incomplete solving, Linear algorithm, Maximum Satisfiability, MaxSAT, SAT-based MaxSAT",
author = "Jeremias Berg and Emir Demirović and Stuckey, {Peter J.}",
year = "2019",
doi = "10.1007/978-3-030-19212-9_3",
language = "English",
isbn = "9783030192112",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "39--56",
editor = "Louis-Martin Rousseau and Kostas Stergiou",
booktitle = "Integration of Constraint Programming, Artificial Intelligence, and Operations Research",

}

Berg, J, Demirović, E & Stuckey, PJ 2019, Core-boosted linear search for incomplete MaxSAT. in L-M Rousseau & K Stergiou (eds), Integration of Constraint Programming, Artificial Intelligence, and Operations Research: and Operations Research 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings. Lecture Notes in Computer Science , vol. 11494 , Springer, Cham Switzerland, pp. 39-56, International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming for Combinatorial Optimization Problems 2019
, Thessaloniki, Greece, 4/06/19. https://doi.org/10.1007/978-3-030-19212-9_3

Core-boosted linear search for incomplete MaxSAT. / Berg, Jeremias; Demirović, Emir; Stuckey, Peter J.

Integration of Constraint Programming, Artificial Intelligence, and Operations Research: and Operations Research 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings. ed. / Louis-Martin Rousseau; Kostas Stergiou. Cham Switzerland : Springer, 2019. p. 39-56 (Lecture Notes in Computer Science ; Vol. 11494 ).

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

TY - GEN

T1 - Core-boosted linear search for incomplete MaxSAT

AU - Berg, Jeremias

AU - Demirović, Emir

AU - Stuckey, Peter J.

PY - 2019

Y1 - 2019

N2 - Maximum Satisfiability (MaxSAT), the optimisation extension of the well-known Boolean Satisfiability (SAT) problem, is a competitive approach for solving NP-hard problems encountered in various artificial intelligence and industrial domains. Due to its computational complexity, there is an inherent tradeoff between scalability and guarantee on solution quality in MaxSAT solving. Limitations on available computational resources in many practical applications motivate the development of complete any-time MaxSAT solvers, i.e. algorithms that compute optimal solutions while providing intermediate results. In this work, we propose core-boosted linear search, a generic search-strategy that combines two central approaches in modern MaxSAT solving, namely linear and core-guided algorithms. Our experimental evaluation on a prototype combining reimplementations of two state-of-the-art MaxSAT solvers, PMRES as the core-guided approach and LinSBPS as the linear algorithm, demonstrates that our core-boosted linear algorithm often outperforms its individual components and shows competitive and, on many domains, superior results when compared to other state-of-the-art solvers for incomplete MaxSAT solving.

AB - Maximum Satisfiability (MaxSAT), the optimisation extension of the well-known Boolean Satisfiability (SAT) problem, is a competitive approach for solving NP-hard problems encountered in various artificial intelligence and industrial domains. Due to its computational complexity, there is an inherent tradeoff between scalability and guarantee on solution quality in MaxSAT solving. Limitations on available computational resources in many practical applications motivate the development of complete any-time MaxSAT solvers, i.e. algorithms that compute optimal solutions while providing intermediate results. In this work, we propose core-boosted linear search, a generic search-strategy that combines two central approaches in modern MaxSAT solving, namely linear and core-guided algorithms. Our experimental evaluation on a prototype combining reimplementations of two state-of-the-art MaxSAT solvers, PMRES as the core-guided approach and LinSBPS as the linear algorithm, demonstrates that our core-boosted linear algorithm often outperforms its individual components and shows competitive and, on many domains, superior results when compared to other state-of-the-art solvers for incomplete MaxSAT solving.

KW - Core-guided MaxSat

KW - Incomplete solving

KW - Linear algorithm

KW - Maximum Satisfiability

KW - MaxSAT

KW - SAT-based MaxSAT

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

U2 - 10.1007/978-3-030-19212-9_3

DO - 10.1007/978-3-030-19212-9_3

M3 - Conference Paper

SN - 9783030192112

T3 - Lecture Notes in Computer Science

SP - 39

EP - 56

BT - Integration of Constraint Programming, Artificial Intelligence, and Operations Research

A2 - Rousseau, Louis-Martin

A2 - Stergiou, Kostas

PB - Springer

CY - Cham Switzerland

ER -

Berg J, Demirović E, Stuckey PJ. Core-boosted linear search for incomplete MaxSAT. In Rousseau L-M, Stergiou K, editors, Integration of Constraint Programming, Artificial Intelligence, and Operations Research: and Operations Research 16th International Conference, CPAIOR 2019 Thessaloniki, Greece, June 4–7, 2019 Proceedings. Cham Switzerland: Springer. 2019. p. 39-56. (Lecture Notes in Computer Science ). https://doi.org/10.1007/978-3-030-19212-9_3