Machine 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 branching variable in DPLL and CDCL solvers. Such heuristics can be improved with machine learning (ML) models; they can reduce the number of steps but usually hinder the running time because useful models are relatively large and slow. We suggest the strategy of making a few initial steps with a trained ML model and then releasing control to classical heuristics; this simplifies cold start for SAT solving and can decrease both the number of steps and overall runtime, but requires a separate decision of when to release control to the solver. Moreover, we introduce a modification of Graph-Q-SAT tailored to SAT problems converted from other domains, e.g., open shop scheduling problems. We validate the feasibility of our approach with random and industrial SAT problems.
Code (0)
등록된 구현이 없습니다.
Tasks
SchedulingSimilar Papers 제목 키워드 기반
Graph Signal Recovery Using Restricted Boltzmann Machines
We propose a model-agnostic pipeline to recover graph signals from an expert system by exploiting the content addressable memory property of restricted Boltzmann machine and the representational ability of a neural netwo…
BIG-bench Machine LearningDenoisingMORBDD: Multiobjective Restricted Binary Decision Diagrams by Learning to Sparsify
In multicriteria decision-making, a user seeks a set of non-dominated solutions to a (constrained) multiobjective optimization problem, the so-called Pareto frontier. In this work, we seek to bring a state-of-the-art met…
Decision MakingMultiobjective OptimizationDiscrete Restricted Boltzmann Machines
We describe discrete restricted Boltzmann machines: probabilistic graphical models with bipartite interactions between visible and hidden discrete variables. Examples are binary restricted Boltzmann machines and discrete…
Constructing Phylogenetic Networks via Cherry Picking and Machine Learning
Combining a set of phylogenetic trees into a single phylogenetic network that explains all of them is a fundamental challenge in evolutionary studies. Existing methods are computationally expensive and can either handle …
Learning fine-grained search space pruning and heuristics for combinatorial optimization
Combinatorial optimization problems arise in a wide range of applications from diverse domains. Many of these problems are NP-hard and designing efficient heuristics for them requires considerable time and experimentatio…
Combinatorial OptimizationReinforcement Learning