Learning Heuristics for Quantified Boolean Formulas through Reinforcement Learning

2020-05-01 · ICLR 2020 1 · Gil Lederman, Markus Rabe, Sanjit Seshia, Edward A. Lee

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 solve formulas of impressive size - up to hundreds of thousands of variables. The main challenge is to find a representation of these formulas that lends itself to making predictions in a scalable way. For a family of challenging problems, we learned a heuristic that solves significantly more formulas compared to the existing handwritten heuristics.

📄 PDF Abstract BibTeX

Code (0)

등록된 구현이 없습니다.

Tasks

Deep Reinforcement Learningreinforcement-learning Reinforcement Learning Reinforcement Learning (RL)

Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning

2018-07-20 · Gil Lederman, Markus N. Rabe, Edward A. Lee, Sanjit A. Seshia

Deep Reinforcement Learning reinforcement-learning Reinforcement Learning Reinforcement Learning (RL)

Learning Heuristics for Automated Reasoning through Reinforcement Learning

2019-05-01 · ICLR 2019 5 · Gil Lederman, Markus N. Rabe, Edward A. Lee, Sanjit A. Seshia

We demonstrate how to learn efficient heuristics for automated reasoning algorithms through deep reinforcement learning. We focus on backtracking search algorithms for quantified Boolean logics, which already can solve f…

Deep Reinforcement Learning reinforcement-learning Reinforcement Learning Reinforcement Learning (RL)

Graph Neural Networks for Reasoning 2-Quantified Boolean Formulas

2019-09-25 · Fei Wang, Zhanfu Yang, Ziliang Chen, Guannan Wei 외

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 Reasoning

Synthesis with Explicit Dependencies

2023-01-25 · Priyanka Golia, Subhajit Roy, Kuldeep S. Meel

Quantified Boolean Formulas (QBF) extend propositional logic with quantification $\forall, \exists$. In QBF, an existentially quantified variable is allowed to depend on all universally quantified variables in its scope.…

On Quantifying Literals in Boolean Logic and Its Applications to Explainable AI

2021-08-23 · Adnan Darwiche, Pierre Marquis

Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have bee…