Clause redundancy and preprocessing in maximum satisfiability

DOI10.1007/978-3-031-10769-6_6MaRDI QIDQ2104499zbMATH OpenOpenAlexFDO

Authors Hannes Ihalainen, Jeremias Berg, Matti Järvisalo

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

preprocessingmaximum satisfiabilityclause redundancypropagation redundancy

Mathematics Subject Classification ID

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

Cites work

• A flexible proof format for SAT solver-elaborator communication
• A theory of measurement in diagnosis from first principles
• Clause elimination for SAT and QSAT
• Core-boosted linear search for incomplete MaxSAT
• Dynamic polynomial watchdog encoding for solving weighted MaxSAT
• Efficient certified RAT verification
• Efficient, verified checking of propositional proofs
• Exploiting the power of MIP solvers in MAXSAT
• Handbook of satisfiability. In 2 parts
• Inprocessing rules
• Iterative and core-guided maxsat solving: a survey and assessment
• Local redundancy in SAT: generalizations of blocked clauses
• Mycielski graphs and PR proofs
• On preprocessing for weighted MaxSAT
• Progress in Artificial Intelligence
• RC2: an efficient MaxSAT solver
• SAT-based MaxSAT algorithms
• SAT-based preprocessing for MaxSAT
• Short proofs without new variables
• Simulating circuit-level simplifications on CNF
• Simulating strong practical proof systems with extended resolution
• Strong extension-free proof systems
• Subsumed label elimination for maximum satisfiability
• Super-blocked clauses
• Unifying reasoning and core-guided search for maximum satisfiability

Cited in

(2)

• Preprocessing of propagation redundant clauses
• Certified Core-Guided MaxSAT Solving

Describes a project that uses

Uses Software

• RC2
• MaxPre

This page was built for publication: Clause redundancy and preprocessing in maximum satisfiability

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