# Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability

arXiv: https://arxiv.org/abs/1909.11588 · HTML: https://mlsanity.com/paper/1909.11588/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Sep 2019.

## Built on by (most cited first, 2 of 2)

- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)

## Abstract (arXiv)

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), it remains a mystery of GNN-based solvers for more complex predicate logic formulae. In this work, we conjectures with some evidences, that generally-defined GNNs present several limitations to certify the unsatisfiability (UNSAT) in Boolean formulae. It implies that GNNs may probably fail in learning the logical reasoning tasks if they contain proving UNSAT as the sub-problem included by most predicate logic formulae.