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 language | English |
---|---|
Title of host publication | Principles and Practice of Constraint Programming |
Subtitle of host publication | 25th International Conference, CP 2019 Stamford, CT, USA, September 30 – October 4, 2019 Proceedings |
Editors | Thomas Schiex, Simon de Givry |
Place of Publication | Cham Switzerland |
Publisher | Springer |
Pages | 177-194 |
Number of pages | 18 |
ISBN (Electronic) | 9783030300487 |
ISBN (Print) | 9783030300470 |
DOIs | |
Publication status | Published - 2019 |
Event | International Conference on Principles and Practice of Constraint Programming 2019 - Stamford, United States of America Duration: 30 Sept 2019 → 4 Oct 2019 Conference number: 25th https://cp2019.a4cp.org/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 11802 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | International Conference on Principles and Practice of Constraint Programming 2019 |
---|---|
Abbreviated title | CP 2019 |
Country/Territory | United States of America |
City | Stamford |
Period | 30/09/19 → 4/10/19 |
Internet address |
Keywords
- Incomplete MaxSAT
- MaxSAT
- Solution-guided search