Techniques inspired by local search for incomplete MaxSAT and the linear algorithm: varying resolution and solution-guided search

Emir Demirović, Peter J. Stuckey

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

Abstract

We present a MaxSAT algorithm designed to find high-quality solutions when faced with a tight time budget, e.g. five minutes. The motivation stems from the fact that, for many practical applications, time resources are limited and thus a ‘good solution’ suffices. We identify three weaknesses of the linear MaxSAT algorithm that prevent it from effectively computing low-violation solutions early in the search and develop a novel approach inspired by local search to address these issues. Our varying resolution method initially considers a rough view of the soft clauses (low resolution) and with time refines and adds the remaining constraints until the original problem is solved (high resolution). In addition, we combine the technique with solution-guided search. We experimentally evaluate our approach on test bed benchmarks from the MaxSAT Evaluation 2018 and show that improvements can be achieved over the baseline linear MaxSAT algorithm.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication25th International Conference, CP 2019 Stamford, CT, USA, September 30 – October 4, 2019 Proceedings
EditorsThomas Schiex, Simon de Givry
Place of PublicationCham Switzerland
PublisherSpringer
Pages177-194
Number of pages18
ISBN (Electronic)9783030300487
ISBN (Print)9783030300470
DOIs
Publication statusPublished - 2019
EventInternational Conference on Principles and Practice of Constraint Programming 2019 - Stanford, Stamford, United States of America
Duration: 30 Sep 20194 Oct 2019
Conference number: 25th
https://cp2019.a4cp.org/

Publication series

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

Conference

ConferenceInternational Conference on Principles and Practice of Constraint Programming 2019
Abbreviated titleCP 2019
CountryUnited States of America
CityStamford
Period30/09/194/10/19
Internet address

Keywords

  • Incomplete MaxSAT
  • MaxSAT
  • Solution-guided search

Cite this

Demirović, E., & Stuckey, P. J. (2019). Techniques inspired by local search for incomplete MaxSAT and the linear algorithm: varying resolution and solution-guided search. In T. Schiex, & S. de Givry (Eds.), Principles and Practice of Constraint Programming : 25th International Conference, CP 2019 Stamford, CT, USA, September 30 – October 4, 2019 Proceedings (pp. 177-194). (Lecture Notes in Computer Science; Vol. 11802 ). Springer. https://doi.org/10.1007/978-3-030-30048-7_11