Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers

DOI10.1007/978-3-319-40970-2_11zbMath1475.68343OpenAlexW2490137294WikidataQ61732578 ScholiaQ61732578MaRDI QIDQ2818010

Massimo Lauria, Marc Vinyals, Jan Elffers, Jan Johannsen, Thomas Magnard, Jakob Nordström

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)

Related Items (2)

A note about \(k\)-DNF resolution ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy

Uses Software

• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• On the power of clause-learning SAT solvers as resolution engines
• The intractability of resolution
• Space bounds for resolution
• Space proof complexity for random 3-CNFs
• Total Space in Resolution
• Space Complexity in Propositional Calculus
• Resolution Is Not Automatizable Unless W[P Is Tractable]
• Solving SAT and SAT Modulo Theories
• Many hard examples for resolution
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Hard examples for resolution
• The relative efficiency of propositional proof systems
• Short proofs are narrow—resolution made simple
• Space complexity of random formulae in resolution
• Total Space in Resolution Is at Least Width Squared
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Time-space tradeoffs in resolution
• Improved Separations of Regular Resolution from Clause Learning Proof Systems
• Small Stone in Pool
• Some trade-off results for polynomial calculus
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution

This page was built for publication: Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers