IB-Net: Initial Branch Network for Variable Decision in Boolean Satisfiability
Boolean Satisfiability problems are vital components in Electronic Design Automation, particularly within the Logic Equivalence Checking process. Currently, SAT solvers are employed for these problems and neural network is tried as assistance to solvers. However, as SAT problems in the LEC context are distinctive due to their predominantly unsatisfiability nature and a substantial proportion of UNSAT-core variables, existing neural network assistance has proven unsuccessful in this specialized domain. To tackle this challenge, we propose IB-Net, an innovative framework utilizing graph neural networks and novel graph encoding techniques to model unsatisfiable problems and interact with state-of-the-art solvers. Extensive evaluations across solvers and datasets demonstrate IB-Net's acceleration, achieving an average runtime speedup of 5.0% on industrial data and 8.3% on SAT competition data empirically. This breakthrough advances efficient solving in LEC workflows.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Boolean Satisfiability via Imitation Learning
We propose ImitSAT, a branching policy for conflict-driven clause learning (CDCL) solvers based on imitation learning for the Boolean satisfiability problem (SAT). Unlike previous methods that predict instance-level sign…
Reinforcement LearningImprove SAT-solving with Machine Learning
In this project, we aimed to improve the runtime of Minisat, a Conflict-Driven Clause Learning (CDCL) solver that solves the Propositional Boolean Satisfiability (SAT) problem. We first used a logistic regression model t…
BIG-bench Machine LearningMulti-Stage Campaigning OptimizationregressionDPLL(MAPF): an Integration of Multi-Agent Path Finding and SAT Solving Technologies
In multi-agent path finding (MAPF), the task is to find non-conflicting paths for multiple agents from their initial positions to given individual goal positions. MAPF represents a classical artificial intelligence probl…
Heuristic SearchMulti-Agent Path FindingMachine Learning for SAT: Restricted Heuristics and New Graph Representations
Boolean satisfiability (SAT) is a fundamental NP-complete problem with many applications, including automated planning and scheduling. To solve large instances, SAT solvers have to rely on heuristics, e.g., choosing a br…
SchedulingCNNSAT: Fast, Accurate Boolean Satisfiability using Convolutional Neural Networks
Boolean satisfiability (SAT) is one of the most well-known NP-complete problems and has been extensively studied. State-of-the-art solvers exist and have found a wide range of applications. However, they still do not sc…