Clause simplifications in search-space decomposition-based SAT solvers

MaRDI QIDQ4583960zbMATH OpenFDO

Authors Tobias Philipp

Publication date 29 August 2018

Full work available at URL http://ebooks.iospress.nl/volumearticle/37210

zbMATH Keywords

SATinprocessingblocked clause eliminationguiding paths

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05)

Recommendations

• Soundness of inprocessing in clause sharing SAT solvers
• An expressive model for instance decomposition based parallel SAT solvers
• Inprocessing rules
• Clause elimination for SAT and QSAT
• Concurrent clause strengthening

Cited in

(3)

• An expressive model for instance decomposition based parallel SAT solvers
• The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study
• Soundness of inprocessing in clause sharing SAT solvers

This page was built for publication: Clause simplifications in search-space decomposition-based SAT solvers

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