Learning a SAT Solver from Single-Bit Supervision

Abstract

We present NeuroSAT, a message passing neural network that learns to solve SAT problems after only being trained as a classifier to predict satisfiability. Although it is not competitive with state-of-the-art SAT solvers, NeuroSAT can solve problems that are substantially larger and more difficult than it ever saw during training by simply running for more iterations. Moreover, NeuroSAT generalizes to novel distributions; after training only on random SAT problems, at test time it can solve SAT problems encoding graph coloring, clique detection, dominating set, and vertex cover problems, all on a range of distributions over small random graphs.

References in corpus (8)

• Adam: A Method for Stochastic Optimization
• Neural Message Passing for Quantum Chemistry
• Learning Combinatorial Optimization Algorithms over Graphs
• SATzilla: Portfolio-based Algorithm Selection for SAT
• Gated Graph Sequence Neural Networks
• Recurrent Relational Networks
• Can Neural Networks Understand Logical Entailment?
• Restart Strategy Selection using Machine Learning Techniques

Cited by in corpus (66)

• Combinatorial Optimization with Graph Convolutional Networks and Guided Tree Search
• Deep Reinforcement Learning for Electric Vehicle Routing Problem with Time Windows
• Learning Combinatorial Optimization on Graphs: A Survey with Applications to Networking
• Learning to Perform Local Rewriting for Combinatorial Optimization
• Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective
• Machine Learning on Graphs: A Model and Comprehensive Taxonomy
• Analysing Mathematical Reasoning Abilities of Neural Models
• GamePad: A Learning Environment for Theorem Proving
• Link Scheduling using Graph Neural Networks
• Generative Language Modeling for Automated Theorem Proving
• SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver
• Learning the Travelling Salesperson Problem Requires Rethinking Generalization
• Learning Variable Ordering Heuristics for Solving Constraint Satisfaction Problems
• A Review of Machine Learning Applications in Fuzzing
• Generalize a Small Pre-trained Model to Arbitrarily Large TSP Instances
• Property Invariant Embedding for Automated Reasoning
• LTL2Action: Generalizing LTL Instructions for Multi-Task RL
• Goal-Aware Neural SAT Solver
• Neural Guided Constraint Logic Programming for Program Synthesis
• Erdos Goes Neural: an Unsupervised Learning Framework for Combinatorial Optimization on Graphs
• MEUZZ: Smart Seed Scheduling for Hybrid Fuzzing
• Accelerating Primal Solution Findings for Mixed Integer Programs Based on Solution Prediction
• NNgSAT: Neural Network guided SAT Attack on Logic Locked Complex Structures
• Multitask Learning on Graph Neural Networks: Learning Multiple Graph Centrality Measures with a Unified Network
• Deep Reasoning Networks: Thinking Fast and Slow
• Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
• A Neural Network-based SAT-Resilient Obfuscation Towards Enhanced Logic Locking
• Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers
• Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning
• Siamese Graph Neural Networks for Data Integration
• It's Not What Machines Can Learn, It's What We Cannot Teach
• Learning advanced mathematical computations from examples
• SATformer: Transformer-Based UNSAT Core Learning
• Network Calculus with Flow Prolongation -- A Feedforward FIFO Analysis enabled by ML
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
• Automated proof synthesis for propositional logic with deep neural networks
• Estimating the Circuit Deobfuscating Runtime based on Graph Deep Learning
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis
• Learning dynamic polynomial proofs
• On Learning to Prove
• Neural Execution of Graph Algorithms
• Neural heuristics for SAT solving
• Towards Scale-Invariant Graph-related Problem Solving by Iterative Homogeneous Graph Neural Networks
• Can You Learn an Algorithm? Generalizing from Easy to Hard Problems with Recurrent Networks
• ML + FV = $♡$? A Survey on the Application of Machine Learning to Formal Verification
• Dropout as a Regularizer of Interaction Effects
• Typed Graph Networks
• Making Logic Learnable With Neural Networks
• Neural Logic Networks
• Program synthesis performance constrained by non-linear spatial relations in Synthetic Visual Reasoning Test
• NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks
• Universal Policies for Software-Defined MDPs
• Neural Consciousness Flow
• Fast OBDD Reordering using Neural Message Passing on Hypergraph
• Learning Markov Random Fields for Combinatorial Structures via Sampling through Lovász Local Lemma
• Neural Circuit Synthesis from Specification Patterns
• Solving QSAT problems with neural MCTS
• Constrained Machine Learning: The Bagel Framework
• Towards Utilitarian Combinatorial Assignment with Deep Neural Networks and Heuristic Algorithms
• On the Robustness of Deep Learning-predicted Contention Models for Network Calculus
• Simplex Initialization: A Survey of Techniques and Trends
• A GNN Based Approach to LTL Model Checking
• Zero Training Overhead Portfolios for Learning to Solve Combinatorial Problems
• Extending Answer Set Programs with Neural Networks
• Elementary Logic in Linear Space
• Neural-Network Guided Expression Transformation