scientific article; zbMATH DE number 7178357

MaRDI QIDQ5219922zbMATH OpenFDO

Authors Marijn J. H. Heule, Armin Biere

Publication date 9 March 2020

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cited in

(8)

• Generating extended resolution proofs with a BDD-based SAT solver
• Non-clausal redundancy properties
• Formal Verification of Integer Multiplier Circuits Using Algebraic Reasoning: A Survey
• Generating Extended Resolution Proofs with a BDD-Based SAT Solver
• Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
• Clausal congruence closure
• Certifying incremental SAT solving
• Certifying phase abstraction

This page was built for publication:

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