Formula Caching in DPLL

DOI10.1145/1714450.1714452MaRDI QIDQ2947546zbMATH OpenOpenAlexFDO

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

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)

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

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
• scientific article; zbMATH DE number 1950260 (Why is no real title available?)

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)