Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers
In this paper, we investigate the feasibility of learning GNN (Graph Neural Network) based solvers and GNN-based heuristics for specified QBF (Quantified Boolean Formula) problems. We design and evaluate several GNN architectures for 2QBF formulae, and conjecture that GNN has limitations in learning 2QBF solvers. Then we show how to learn a heuristic CEGAR 2QBF solver. We further explore generalizing GNN-based heuristics to larger unseen instances, and uncover some interesting challenges. In summary, this paper provides a comprehensive surveying view of applying GNN-embeddings to specified QBF solvers, and aims to offer guidance in applying ML to more complicated symbolic reasoning problems.
Code (0)
등록된 구현이 없습니다.
Tasks
Graph Neural NetworkSimilar Papers 제목 키워드 기반
Graph Neural Networks for Reasoning 2-Quantified Boolean Formulas
It is valuable yet remains challenging to apply neural networks in logical reasoning tasks. Despite some successes witnessed in learning SAT (Boolean Satisfiability) solvers for propositional logic via Graph Neural Netwo…
Logical ReasoningSolving Quantified Boolean Formulas with Few Existential Variables
The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., pl…
Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability
It is feasible and practically-valuable to bridge the characteristics between graph neural networks (GNNs) and logical reasoning. Despite considerable efforts and successes witnessed to solve Boolean satisfiability (SAT)…
Logical ReasoningAbstract Solvers for Computing Cautious Consequences of ASP programs
Abstract solvers are a method to formally analyze algorithms that have been profitably used for describing, comparing and composing solving techniques in various fields such as Propositional Satisfiability (SAT), Quantif…
Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning
We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on a backtracking search algorithm, which can already solv…
Deep Reinforcement Learningreinforcement-learningReinforcement LearningReinforcement Learning (RL)