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

(6)

• Super-blocked clauses
• An expressive model for instance decomposition based parallel SAT solvers
• Local redundancy in SAT: generalizations of blocked clauses
• Clause simplifications in search-space decomposition-based SAT solvers
• Unsatisfiability proofs for distributed clause-sharing SAT solvers
• Trusted scalable SAT solving with on-the-fly LRAT checking

Describes a project that uses

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)