Extended resolution clause learning via dual implication points

DOI10.46298/LMCS-22(2:23)2026MaRDI QIDQ7255001zbMATH OpenFDO

Authors Samuel R. Buss, Jonathan Chung, Vijay Ganesh, Albert Oliveras

Publication date 29 May 2026

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-22(2:23)2026

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• Backing backtracking
• Cadiback: Extracting backbones with CaDiCaL
• Chronological backtracking
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Computer Aided Verification
• Effective auxiliary variables via structured reencoding
• Encoding Redundancy for Satisfaction-Driven Clause Learning
• Extended clause learning
• Generating Extended Resolution Proofs with a BDD-Based SAT Solver
• Hard examples for resolution
• Hardware and software: verification and testing. 8th international Haifa verification conference, HVC 2012, Haifa, Israel, November 6--8, 2012. Revised selected papers
• scientific article; zbMATH DE number 3904558 (Why is no real title available?)
• Learning shorter redundant clauses in SDCL using MaxSAT
• On the power of clause-learning SAT solvers as resolution engines
• Preprocessing of propagation redundant clauses
• Short proofs without new variables
• Size-space tradeoffs for resolution
• Strong extension-free proof systems
• The intractability of resolution
• Zur allgemeinen Kurventheorie.

This page was built for publication: Extended resolution clause learning via dual implication points

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