On dedicated CDCL strategies for PB solvers

DOI10.1007/978-3-030-80223-3_22OpenAlexW3186193063MaRDI QIDQ2118312

Romain Wallon, Daniel Le Berre

Publication date: 22 March 2022

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

zbMATH Keywords

pseudo-Boolean optimizationbranching heuristicslearned constraint deletion strategiespseudo-Boolean solvingrestart policies

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the power of clause-learning SAT solvers as resolution engines
• On the complexity of cutting-plane proofs
• Optimal speedup of Las Vegas algorithms
• The intractability of resolution
• Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers
• In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving
• On weakening strategies for PB solvers
• Learning Rate Based Branching Heuristic for SAT Solvers
• Outline of an algorithm for integer solutions to linear programs
• Evaluating CDCL Variable Scoring Schemes
• Adaptive Restart Strategies for Conflict Driven SAT Solvers
• GRASP: a search algorithm for propositional satisfiability
• Theory and Applications of Satisfiability Testing
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution