Progression in maximum satisfiability

A. Ignatiev, A. Morgado, V. Manquinho, I. Lynce, J. Marques-Silva

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

16 Citations (Scopus)

Abstract

Maximum Satisfiability (MaxSAT) is a well-known optimization version of Propositional Satisfiability (SAT), that finds a wide range of relevant practical applications. Despite the significant progress made in MaxSAT solving in recent years, many practically relevant problem instances require prohibitively large run times, and many cannot simply be solved with existing algorithms. One approach for solving MaxSAT is based on iterative SAT solving, which may optionally be guided by unsatisfiable cores. A difficulty with this class of algorithms is the possibly large number of times a SAT solver is called, e.g. for instances with very large clause weights. This paper proposes the use of geometric progressions to tackle this issue, thus allowing, for the vast majority of problem instances, to reduce the number of calls to the SAT solver. The new approach is also shown to be applicable to core-guided MaxSAT algorithms. Experimental results, obtained on a large number of problem instances, show gains when compared to state-of-the-art implementations of MaxSAT algorithms.

Original languageEnglish
Title of host publicationECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic
Subtitle of host publicationIncluding - Prestigious Applications of Intelligent Systems (PAIS 2014) - Proceedings
EditorsTorsten Schaub, Gerhard Friedrich, Barry O'Sullivan
Place of PublicationAmsterdam Netherlands
PublisherIOS Press
Pages453-458
Number of pages6
ISBN (Electronic)9781614994183
DOIs
Publication statusPublished - 2014
Externally publishedYes
EventEuropean Conference on Artificial Intelligence 2014 - Prague, Czech Republic
Duration: 18 Aug 201422 Aug 2014
Conference number: 21st
https://web.archive.org/web/20140322194831/http://www.ecai2014.org/

Publication series

NameFrontiers in Artificial Intelligence and Applications
PublisherIOS Press
Volume263
ISSN (Print)0922-6389
ISSN (Electronic)1879-8314

Conference

ConferenceEuropean Conference on Artificial Intelligence 2014
Abbreviated titleECAI 2014
Country/TerritoryCzech Republic
CityPrague
Period18/08/1422/08/14
Internet address

Cite this