A Unified Framework for Certificate and Compilation for QBF

DOI10.1007/978-3-540-92701-3_15zbMath1209.68517OpenAlexW1513281252MaRDI QIDQ3601811

Benoit da Mota, Igor Stéphan

Publication date: 12 February 2009

Published in: Logic and Its Applications (Search for Journal in Brave)

Full work available at URL: https://hal.univ-angers.fr/hal-03255579/file/icla09.pdf

zbMATH Keywords

quantified Boolean formulas

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (1)

CAQE and QuAbS: Abstraction Based QBF Solvers

Uses Software

• Nenofex
• QUBOS
• Quantor
• sKizzo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A satisfiability procedure for quantified Boolean formulae
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Resolution for quantified Boolean formulas
• Boolean functions as models for quantified Boolean formulas
• Nenofex: Expanding NNF for QBF Solving
• Using SAT in QBF
• A First Step Towards a Unified Proof Checker for QBF
• Graph-Based Algorithms for Boolean Function Manipulation
• Automated Deduction – CADE-20
• A machine program for theorem-proving
• Logic for Programming, Artificial Intelligence, and Reasoning
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2004

This page was built for publication: A Unified Framework for Certificate and Compilation for QBF