Encoding Redundancy for Satisfaction-Driven Clause Learning

DOI10.1007/978-3-030-17462-0_3zbMath1527.68212OpenAlexW2926909513MaRDI QIDQ6091331

Benjamin Kiesl, Marijn J. H. Heule, Armin Biere

Publication date: 24 November 2023

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-17462-0_3

Mathematics Subject Classification ID

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 (3)

Never trust your solver: certification for SAT and QBF ⋮ Truth Assignments as Conditional Autarkies ⋮ Covered clauses are not propagation redundant

This page was built for publication: Encoding Redundancy for Satisfaction-Driven Clause Learning