Clause redundancy and preprocessing in maximum satisfiability
From MaRDI portal
Publication:2104499
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
Uses Software
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
