Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability

TL;DR

This paper investigates the limitations of graph neural networks in certifying Boolean unsatisfiability, suggesting they may fail to learn complex logical reasoning tasks involving UNSAT proofs.

Contribution

It provides evidence and analysis showing that generally-defined GNNs have inherent limitations in certifying Boolean UNSAT, highlighting challenges in logical reasoning with GNNs.

Findings

GNNs may fail to certify Boolean UNSAT in complex formulas

Limitations of GNNs in logical reasoning tasks involving UNSAT

Challenges in applying GNNs to predicate logic formulae

Abstract

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.