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

DOI10.1007/978-3-319-40970-2_11zbMATH Open1475.68343OpenAlexW2490137294WikidataQ61732578 ScholiaQ61732578MaRDI QIDQ2818010FDOQ2818010

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

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

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)

Cites Work

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

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

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)