Clause redundancy and preprocessing in maximum satisfiability

DOI10.1007/978-3-031-10769-6_6OpenAlexW4289104008MaRDI QIDQ2104499

Hannes Ihalainen, Matti Järvisalo, Jeremias Berg

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_6

zbMATH Keywords

maximum satisfiabilitypreprocessingclause redundancypropagation redundancy

Mathematics Subject Classification ID

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

Uses Software

• MaxPre
• RC2

Cites Work

• Unnamed Item
• Unnamed Item
• Simulating circuit-level simplifications on CNF
• SAT-based MaxSAT algorithms
• A theory of measurement in diagnosis from first principles
• Dynamic polynomial watchdog encoding for solving weighted MaxSAT
• Efficient, verified checking of propositional proofs
• A flexible proof format for SAT solver-elaborator communication
• Simulating strong practical proof systems with extended resolution
• On preprocessing for weighted MaxSAT
• Unifying reasoning and core-guided search for maximum satisfiability
• Strong extension-free proof systems
• Core-boosted linear search for incomplete MaxSAT
• Iterative and core-guided maxsat solving: a survey and assessment
• Short proofs without new variables
• Efficient certified RAT verification
• Mycielski graphs and PR proofs
• Super-Blocked Clauses
• SAT-Based Preprocessing for MaxSAT
• Inprocessing Rules
• Clause Elimination for SAT and QSAT
• Subsumed Label Elimination for Maximum Satisfiability
• RC2: an Efficient MaxSAT Solver
• Progress in Artificial Intelligence
• Exploiting the Power of mip Solvers in maxsat