Certified Core-Guided MaxSAT Solving

DOI10.1007/978-3-031-38499-8_1MaRDI QIDQ6492726zbMATH OpenFDO

Authors Jeremias Berg, Bart Bogaerts, Jakob Nordstrom, Andy Oertel, Dieter Vandesande

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_1

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• A computational status update for exact rational mixed integer programming
• A framework for certified Boolean branch-and-bound optimization
• A hybrid branch-and-bound approach for exact rational mixed-integer programming
• A proof builder for Max-SAT
• Boolean lexicographic optimization: algorithms \& applications
• Boosting branch-and-bound MaxSAT solvers with clause learning
• Certifying algorithms
• Clause redundancy and preprocessing in maximum satisfiability
• Core-guided and core-boosted search for CP
• DRMaxSAT with MaxHS: first contact
• Dynamic polynomial watchdog encoding for solving weighted MaxSAT
• Efficient CNF encoding of Boolean cardinality constraints
• Efficient certified RAT verification
• Encoding cardinality constraints using multiway merge selection networks
• Exploiting the power of MIP solvers in MAXSAT
• GRASP: a search algorithm for propositional satisfiability
• Handbook of constraint programming.
• Handbook of satisfiability. In 2 parts
• MaxSAT resolution and subcube sums
• Mixed integer programming: analyzing 12 years of progress
• On Solving the Partial MAX-SAT Problem
• On the complexity of k-SAT
• On the complexity of cutting-plane proofs
• Progress in computational mixed integer programming -- a look back from the other side of the tipping point
• Proofs and Certificates for Max-SAT
• QMaxSATpb: a certified MaxSAT solver
• RC2: an efficient MaxSAT solver
• Resolution for Max-SAT
• The complexity of satisfiability of small depth circuits
• Unsatisfiability-based optimization in clasp
• Verifying Refutations with Extended Resolution
• WPM3: an (in)complete algorithm for weighted partial MaxSAT

Cited in

(7)

• Certified MaxSAT preprocessing
• Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
• Enhancing MaxSAT local search via a unified soft clause weighting scheme
• MaxSAT resolution with inclusion redundancy
• On the counting version of the maximum 2-satisfiability problem
• Automated mathematical discovery and verification: minimizing pentagons in the plane
• Engineering and evaluating multi-objective pseudo-Boolean optimizers

This page was built for publication: Certified Core-Guided MaxSAT Solving

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