Multiple Decision Making in Conflict-Driven Clause Learning

Research output: Contribution to conferencePaperAcademic

Abstract

Most modern and successful SAT solvers are based on the Conflict-Driven Clause-Learning (CDCL) algorithm. The CDCL approach is to try to learn from previous assignments, and based on this, prune the search space to make better decisions in the future. In the current paper, we propose the introduction of a multiple decision maker (MDM) into CDCL. Adhering to a number of rules, MDM constructs sets of decisions to be made at once. Experiments show MDM has a considerably positive impact on CDCL, for many different SAT application problems. Overall, about 50% of the benchmarks we considered were solved faster when MDM was enabled, and the total processing time of all benchmarks was reduced by 6%. Moreover, MDM allowed 31 extra problems to be solved. We introduce MDM, analyse its impact, and try to understand the cause of that impact.

Original languageEnglish
Pages161-169
Number of pages9
DOIs
Publication statusPublished - Nov 2020
Event2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI) - Baltimore, United States
Duration: 9 Dec 202011 Dec 2020
https://ieeexplore.ieee.org/document/9288221

Conference

Conference2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI)
CountryUnited States
CityBaltimore
Period9/12/2011/12/20
Internet address

Keywords

  • CDCL
  • Multiple Decision Making
  • Satisfiability

Fingerprint Dive into the research topics of 'Multiple Decision Making in Conflict-Driven Clause Learning'. Together they form a unique fingerprint.

Cite this