Mining definitions in Kissat with Kittens

DOI10.1007/s10703-023-00421-2OpenAlexW4366823129MaRDI QIDQ6056639

Mathias Fleury, Armin Biere

Publication date: 30 October 2023

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-023-00421-2

zbMATH Keywords

variable eliminationSAT solvingdefinition extraction

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Certified DQBF solving by definition extraction
• Incremental inprocessing in SAT solving
• Interpolation-based semantic gate extraction and its applications to QBF preprocessing
• Definability for model counting
• Blocked Clause Decomposition
• Inprocessing Rules
• Clause Elimination for SAT and QSAT
• SAT-Based Model Checking without Unrolling
• Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)
• Applying Logic Synthesis for Speeding Up SAT
• Automated Testing and Debugging of SAT and QBF Solvers
• Clause Elimination Procedures for CNF Formulas
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification
• Bounded model checking using satisfiability solving

This page was built for publication: Mining definitions in Kissat with Kittens