Certified MaxSAT preprocessing

DOI10.1007/978-3-031-63498-7_24MaRDI QIDQ7034851zbMATH OpenFDO

Authors Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordstrom

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63498-7_24

zbMATH Keywords

formally verified proof checkingmaximum satisfiabilitypreprocessingproof logging

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Brief Overview of HOL4
• A framework for certified Boolean branch-and-bound optimization
• A proof builder for Max-SAT
• Abstract cores in implicit hitting set MaxSat solving
• Automated testing and debugging of SAT and QBF solvers
• Blocked clause elimination
• Certified CNF translations for pseudo-Boolean solving
• Certified Core-Guided MaxSAT Solving
• Certified dominance and symmetry breaking for combinatorial optimisation
• Certifying algorithms
• Clause redundancy and preprocessing in maximum satisfiability
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• DRMaxSAT with MaxHS: first contact
• Dynamic polynomial watchdog encoding for solving weighted MaxSAT
• Efficient certified RAT verification
• Exploiting the power of MIP solvers in MAXSAT
• Exploiting the real power of unit propagation lookahead
• Handbook of satisfiability. In 2 parts
• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• Improvements to core-guided binary search for MaxSAT
• MaxSAT resolution and subcube sums
• On preprocessing for weighted MaxSAT
• On the complexity of cutting-plane proofs
• Principles and practice of constraint programming -- CP 2002. 8th international conference, CP 2002, Ithaca, NY, USA, September 9--13, 2002. Proceedings.
• Proof-producing translation of higher-order logic into pure and stateful ML
• Proofs and Certificates for Max-SAT
• QMaxSATpb: a certified MaxSAT solver
• RC2: an efficient MaxSAT solver
• Resolution for Max-SAT
• Subsumed label elimination for maximum satisfiability
• The verified CakeML compiler backend
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Toward leaner binary-clause reasoning in a satisfiability solver
• Unifying reasoning and core-guided search for maximum satisfiability
• Verified characteristic formulae for CakeML
• Verifying Refutations with Extended Resolution

Cited in

(1)

• Engineering and evaluating multi-objective pseudo-Boolean optimizers

This page was built for publication: Certified MaxSAT preprocessing

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