Soundness of inprocessing in clause sharing SAT solvers

DOI10.1007/978-3-642-39071-5_4MaRDI QIDQ5326451zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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
• Super-blocked clauses
• Unsatisfiability proofs for distributed clause-sharing SAT solvers

Describes a project that uses

Uses Software

• pfolioUZK
• ppfolio
• CryptoMiniSat
• PrecoSAT
• Chaff

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)