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.
|Status||Gepubliceerd - nov 2020|
|Evenement||2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI) - Baltimore, Verenigde Staten van Amerika|
Duur: 9 dec 2020 → 11 dec 2020
|Congres||2020 IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI)|
|Land||Verenigde Staten van Amerika|
|Periode||9/12/20 → 11/12/20|