Multiple Decision Making in Conflict-Driven Clause Learning

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

2 Citations (Scopus)

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
Title of host publicationProceedings - IEEE 32nd International Conference on Tools with Artificial Intelligence, ICTAI 2020
EditorsMiltos Alamaniotis, Shimei Pan
Pages161-169
Number of pages9
ISBN (Electronic)9781728192284
DOIs
Publication statusPublished - Nov 2020
Event32nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2020 - Baltimore, United States
Duration: 9 Dec 202011 Dec 2020
Conference number: 32
https://ieeexplore.ieee.org/document/9288221

Conference

Conference32nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2020
Abbreviated titleICTAI 2020
Country/TerritoryUnited 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