Proofs and Certificates for Max-SAT

DOI10.1613/JAIR.1.13811MaRDI QIDQ5870516zbMATH OpenOpenAlexFDO

Authors Matthieu Py, Mohamed Sami Cherif, Djamal Habet

Publication date 9 January 2023

Published in Journal of Artificial Intelligence Research (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1613/jair.1.13811

zbMATH Keywords

constraint programmingsatisfiability

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• Efficient verified (UN)SAT certificate checking
• Producing and verifying extremely large propositional refutations
• Resolution for Max-SAT
• Efficient verified (UN)SAT certificate checking
• Proof Complexity for the Maximum Satisfiability Problem and its Use in SAT Refutations

Cites work

• \textsc{ahmaxsat}: description and evaluation of a branch and bound Max-SAT solver
• A Complete Calculus for Max-SAT
• A logical approach to efficient Max-SAT solving
• A Machine-Oriented Logic Based on the Resolution Principle
• A near-optimal separation of regular and general resolution
• A proof builder for Max-SAT
• Algorithms for Weighted Boolean Optimization
• Boosting branch-and-bound MaxSAT solvers with clause learning
• Circular (yet sound) proofs
• Curriculum-based course timetabling with SAT and MaxSAT
• Equivalence between systems stronger than resolution
• Handbook of satisfiability. In 2 parts
• scientific article; zbMATH DE number 5613975 (Why is no real title available?)
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 3320385 (Why is no real title available?)
• Iterative and core-guided maxsat solving: a survey and assessment
• MaxSAT resolution and subcube sums
• maxSAT-based large neighborhood search for high school timetabling
• MaxSAT-based scheduling of B2B meetings
• Near optimal seperation of tree-like and general resolution
• New inference rules for Max-SAT
• On Solving the Partial MAX-SAT Problem
• Open-WBO: a modular MaxSAT solver
• Optimal partial-order plan relaxation via MaxSAT
• RC2: an efficient MaxSAT solver
• Resolution for Max-SAT
• SAT-based MaxSAT algorithms
• Solving (Weighted) Partial MaxSAT through Satisfiability Testing
• Solving the Team Composition Problem in a Classroom
• The Complexity of Propositional Proofs
• Theory and Applications of Satisfiability Testing
• Towards a better understanding of (partial weighted) MaxSAT proof systems
• Understanding the power of Max-SAT resolution through up-resilience

Cited in

(3)

• Proof Complexity for the Maximum Satisfiability Problem and its Use in SAT Refutations
• Certified Core-Guided MaxSAT Solving
• Certified MaxSAT preprocessing

Describes a project that uses

Uses Software

• MaxHS
• Open-WBO
• MiniSat

This page was built for publication: Proofs and Certificates for Max-SAT

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