Adapting CDCL Strategies for PB Solvers [July 3, 2020]

 Summary

by Romain Wallon for the 11th Pragmatics of SAT International workshop (http://www.pragmaticsofsat.org/2020/)

Current implementations of pseudo-Boolean (PB) solvers are based on the CDCL architecture, which is the central component of modern SAT solvers. In addition to clause learning, this architecture comes with many strategies that help the solver find its way through the search space, either to a solution or to an unsatisfiability proof. Particularly important are the decision heuristic, but also other features like learned clause deletion or restarts. Currently, these strategies are mostly used "as is" in PB solvers, without considering the particular form of the PB constraints they deal with. In this paper, we introduce new ways of adapting these strategies to better take into account the specificities of such constraints, especially regarding their weights and propagation properties. In particular, our experiments show that carefully considering these criteria may have a significant impact on the performance of the solver.

 Infos

Added by :
Daniel Le Berre

Updated on :
July 4, 2020, 12:07 p.m.

Duration :
00:29:15

Number of view :
9 (Show details views)

Type :
Other

Main language :
English

 Downloads
 Embed/Share (Draft Mode)
Please note that your video is in draft mode.
The following links contain a key allowing access. Anyone with this links can access it.
Check the box to autoplay the video.
Check the box to loop the video.
Check the box to indicate the beginning of playing desired.
qrcode