Certified SAT solving with GPU accelerated inprocessing

DOI10.1007/S10703-023-00432-ZMaRDI QIDQ6564174zbMATH OpenFDO

Authors Muhammad Osama, Anton Wijs, Armin Biere

Publication date 28 June 2024

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10703-023-00432-Z

zbMATH Keywords

clausal proofsfunctional dependency extractionGPUsinprocessingSAT solving

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• A machine program for theorem-proving
• Algorithms for computing minimal unsatisfiable subsets of constraints
• An efficient SMT solver for string constraints
• Automatic verification of concurrent stochastic systems
• Bounded model checking using satisfiability solving
• Clause elimination procedures for CNF formulas
• Complexity of fixed-size bit-vector logics
• CrystalBall: gazing in the black box of SAT solving
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 956839 (Why is no real title available?)
• Inprocessing rules
• Leveraging GPUs for effective clause sharing in parallel SAT solving
• On a generalization of extended resolution
• raSAT: an SMT solver for polynomial constraints
• Reducing higher-order theorem proving to a sequence of SAT problems
• SAT solver management strategies in IC3: an experimental approach
• SAT-Based Model Checking without Unrolling
• Simulating circuit-level simplifications on CNF
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Verifying Refutations with Extended Resolution

This page was built for publication: Certified SAT solving with GPU accelerated inprocessing

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