Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms

DOI10.1007/978-3-031-37709-9_21zbMATH Open1547.68221MaRDI QIDQ6535701

Javier Esparza, Rupak Majumdar, Eszter Couillard, Philipp Czerner

Publication date: 1 February 2024

Mathematics Subject Classification ID

Could not fetch data.

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Generating extended resolution proofs with a BDD-based SAT solver
• Dual proof generation for quantified Boolean formulas with a BDD-based solver
• Flexible proof production in an industrial-strength SMT solver
• Clausal abstraction for DQBF
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• QBF Resolution Systems and Their Proof Complexities
• Extended Resolution Proofs for Conjoining BDDs
• Graph-Based Algorithms for Boolean Function Manipulation
• Algebraic methods for interactive proof systems
• IP = PSPACE
• The knowledge complexity of interactive proof-systems
• Computational Complexity
• Extended Resolution Proofs for Symbolic SAT Solving with Quantification
• Clausal proofs for pseudo-Boolean reasoning

Related Items (1)

A resolution-based interactive proof system for UNSAT

This page was built for publication: Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms

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