Trade-offs between time and memory in a tighter model of CDCL SAT solvers

DOI10.1007/978-3-319-40970-2_11MaRDI QIDQ2818010zbMATH OpenOpenAlexWikidataFDO

Authors Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordstrom, Marc Vinyals

Publication date 5 September 2016

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

Full work available at URL http://hdl.handle.net/2117/103872

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On the power of clause-learning SAT solvers as resolution engines
• Off the Trail: Re-examining the CDCL Algorithm
• On CDCL-based proof systems with the ordered decision strategy
• Reusing the assignment trail in CDCL solvers
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution

Cites work

• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• scientific article; zbMATH DE number 3029852 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Hard examples for resolution
• Improved separations of regular resolution from clause learning proof systems
• Many hard examples for resolution
• On the power of clause-learning SAT solvers as resolution engines
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Resolution Is Not Automatizable Unless W[P] Is Tractable
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Short proofs are narrow—resolution made simple
• Small Stone in pool
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Some trade-off results for polynomial calculus (extended abstract)
• Space Complexity in Propositional Calculus
• Space bounds for resolution
• Space complexity of random formulae in resolution
• Space proof complexity for random 3-CNFs
• The intractability of resolution
• The relative efficiency of propositional proof systems
• Time-space tradeoffs in resolution, superpolynomial lower bounds for superlinear space
• Total space in resolution
• Total space in resolution is at least width squared

Cited in

(4)

• On CDCL-Based Proof Systems with the Ordered Decision Strategy
• A note about k-DNF resolution
• Formal Methods in Computer-Aided Design
• On CDCL-based proof systems with the ordered decision strategy

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Trade-offs between time and memory in a tighter model of CDCL SAT solvers

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