Soundness of inprocessing in clause sharing SAT solvers

DOI10.1007/978-3-642-39071-5_4zbMATH Open1390.68582OpenAlexW134175813MaRDI QIDQ5326451FDOQ5326451

Authors: Norbert Manthey, Tobias Philipp, Christoph Wernhard 

Publication date: 5 August 2013

Published in: Theory and Applications of Satisfiability Testing – SAT 2013 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-39071-5_4

Recommendations

• Clause simplifications in search-space decomposition-based SAT solvers
• An expressive model for instance decomposition based parallel SAT solvers
• Inprocessing rules
• On the power of clause-learning SAT solvers as resolution engines
• scientific article; zbMATH DE number 2243370

Mathematics Subject Classification ID

Cited In (5)

• Local redundancy in SAT: generalizations of blocked clauses
• Clause simplifications in search-space decomposition-based SAT solvers
• An expressive model for instance decomposition based parallel SAT solvers
• Unsatisfiability proofs for distributed clause-sharing SAT solvers
• Super-blocked clauses

Uses Software

• Chaff
• PrecoSAT
• CryptoMiniSat
• ppfolio
• pfolioUZK

This page was built for publication: Soundness of inprocessing in clause sharing SAT solvers

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