Formula Caching in DPLL

DOI10.1145/1714450.1714452zbMATH Open1322.68175OpenAlexW2007316622MaRDI QIDQ2947546FDOQ2947546

Authors: Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind, Paul Beame 

Publication date: 24 September 2015

Published in: ACM Transactions on Computation Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1714450.1714452

Recommendations

• Domain-independent formulas and databases
• Applicative caching
• Amplification by Read-Once Formulas
• Lazy caching in TLA
• Learning read-once formulas with queries
• scientific article; zbMATH DE number 2079659

zbMATH Keywords

resolutionproof complexitysatisfiability

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Complexity of proofs (03F20)

Cited In (5)

• Implementing efficient All solutions SAT solvers
• The state of SAT
• Using membrane calculus to describe DPLL algorithm with clause learning
• Visualizing SAT instances and runs of the DPLL algorithm
• Title not available (Why is that?)

This page was built for publication: Formula Caching in DPLL

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