On dedicated CDCL strategies for PB solvers

DOI10.1007/978-3-030-80223-3_22MaRDI QIDQ2118312zbMATH OpenOpenAlexFDO

Authors Daniel Le Berre, Romain Wallon

Publication date 22 March 2022

Full work available at URL https://arxiv.org/abs/2109.01013

zbMATH Keywords

branching heuristicslearned constraint deletion strategiespseudo-Boolean optimizationpseudo-Boolean solvingrestart policies

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites work

• Adaptive Restart Strategies for Conflict Driven SAT Solvers
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Evaluating CDCL variable scoring schemes
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 5139165 (Why is no real title available?)
• scientific article; zbMATH DE number 5139167 (Why is no real title available?)
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving
• Learning rate based branching heuristic for SAT solvers
• On the complexity of cutting-plane proofs
• On the power of clause-learning SAT solvers as resolution engines
• On weakening strategies for PB solvers
• Optimal speedup of Las Vegas algorithms
• Outline of an algorithm for integer solutions to linear programs
• The intractability of resolution
• Theory and Applications of Satisfiability Testing
• Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers

Cited in

(1)

• Which algorithm to select in sports timetabling?

Describes a project that uses

Uses Software

• MiniSat
• Pueblo
• SATIRE
• Chaff
• PicoSAT
• Sat4j

This page was built for publication: On dedicated CDCL strategies for PB solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2118312)