Propositional proof systems based on maximum satisfiability
From MaRDI portal
Publication:2238728
DOI10.1016/j.artint.2021.103552OpenAlexW3182818576MaRDI QIDQ2238728
Antonio Morgado, Alexey Ignatiev, Samuel R. Buss, Maria Luisa Bonet, João P. Marques-Silva
Publication date: 2 November 2021
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.artint.2021.103552
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- SAT-based MaxSAT algorithms
- Propositional proofs and reductions between NP search problems
- On the power of clause-learning SAT solvers as resolution engines
- Extended clause learning
- Short proofs for tricky formulas
- Symbolic techniques in satisfiability solving
- Resolution for Max-SAT
- On the complexity of the maximum satisfiability problem for Horn formulas
- A theory of diagnosis from first principles
- In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving
- On tackling the limits of resolution in SAT solving
- Mutilated chessboard problem is exponentially hard for resolution
- Cutting planes, connectivity, and threshold logic
- An exponential separation between the parity principle and the pigeonhole principle
- DRMaxSAT with MaxHS: first contact
- Iterative and core-guided maxsat solving: a survey and assessment
- Tools and algorithms for the construction and analysis of systems. 25th international conference, TACAS 2019, held as part of the European joint conferences on theory and practice of software, ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings. Part II
- LMHS: A SAT-IP Hybrid MaxSAT Solver
- Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form
- Propositional SAT Solving
- Open-WBO: A Modular MaxSAT Solver,
- Counterexample-guided abstraction refinement for symbolic model checking
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- Lower bounds for resolution and cutting plane proofs and monotone computations
- GRASP: a search algorithm for propositional satisfiability
- Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
- Theory and Applications of Satisfiability Testing
- Exploiting the Power of mip Solvers in maxsat
- Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
- Correct Hardware Design and Verification Methods
- The complexity of theorem-proving procedures
- Theory and Applications of Satisfiability Testing
- On Solving the Partial MAX-SAT Problem
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
