Multiple Decision Making in Conflict-Driven Clause Learning

Onderzoeksoutput: Bijdrage aan congresPaperAcademic

Samenvatting

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.

Originele taal-2Engels
Pagina's161-169
Aantal pagina's9
DOI's
StatusGepubliceerd - nov 2020
Evenement2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI) - Baltimore, Verenigde Staten van Amerika
Duur: 9 dec 202011 dec 2020
https://ieeexplore.ieee.org/document/9288221

Congres

Congres2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI)
LandVerenigde Staten van Amerika
StadBaltimore
Periode9/12/2011/12/20
Internet adres

Vingerafdruk Duik in de onderzoeksthema's van 'Multiple Decision Making in Conflict-Driven Clause Learning'. Samen vormen ze een unieke vingerafdruk.

Citeer dit