Timezone: »
The Boolean Satisfiability (SAT) problem is the canonical NP-complete problem and is fundamental to computer science, with a wide array of applications in planning, verification, and theorem proving. Developing and evaluating practical SAT solvers relies on extensive empirical testing on a set of real-world benchmark formulas. However, the availability of such real-world SAT formulas is limited. While these benchmark formulas can be augmented with synthetically generated ones, existing approaches for doing so are heavily hand-crafted and fail to simultaneously capture a wide range of characteristics exhibited by real-world SAT instances. In this work, we present G2SAT, the first deep generative framework that learns to generate SAT formulas from a given set of input formulas. Our key insight is that SAT formulas can be transformed into latent bipartite graph representations which we model using a specialized deep generative neural network. We show that G2SAT can generate SAT formulas that closely resemble given real-world SAT instances, as measured by both graph metrics and SAT solver behavior. Further, we show that our synthetic SAT formulas could be used to improve SAT solver performance on real-world benchmarks, which opens up new opportunities for the continued development of SAT solvers and a deeper understanding of their performance.
Author Information
Jiaxuan You (Stanford University)
2nd CS PhD student in Stanford
Haoze Wu (Stanford University)
Clark Barrett (Stanford University)
Clark Barrett joined Stanford University as an Associate Professor (Research) of Computer Science in September 2016. Before that, he was an Associate Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University. His expertise is in constraint solving and its applications to system verification and security. His PhD dissertation introduced a novel approach to constraint solving now known as Satisfiability Modulo Theories (SMT). Today, he is recognized as one of the world's experts in the development and application of SMT techniques. He was also an early pioneer in the development of formal hardware verification: at Intel, he collaborated on a novel theorem prover used to verify key microprocessor properties; and at 0-in Design Automation (now part of Mentor Graphics), he helped build one of the first industrially successful assertion-based verification tool-sets for hardware. He is an ACM Distinguished Scientist.
Raghuram Ramanujan (Davidson College)
Jure Leskovec (Stanford University and Pinterest)
More from the Same Authors
-
2021 : Therapeutics Data Commons: Machine Learning Datasets and Tasks for Drug Discovery and Development »
Kexin Huang · Tianfan Fu · Wenhao Gao · Yue Zhao · Yusuf Roohani · Jure Leskovec · Connor Coley · Cao Xiao · Jimeng Sun · Marinka Zitnik -
2021 Spotlight: Combiner: Full Attention Transformer with Sparse Computation Cost »
Hongyu Ren · Hanjun Dai · Zihang Dai · Mengjiao (Sherry) Yang · Jure Leskovec · Dale Schuurmans · Bo Dai -
2021 : OGB-LSC: A Large-Scale Challenge for Machine Learning on Graphs »
Weihua Hu · Matthias Fey · Hongyu Ren · Maho Nakata · Yuxiao Dong · Jure Leskovec -
2021 : Extending the WILDS Benchmark for Unsupervised Adaptation »
Shiori Sagawa · Pang Wei Koh · Tony Lee · Irena Gao · Sang Michael Xie · Kendrick Shen · Ananya Kumar · Weihua Hu · Michihiro Yasunaga · Henrik Marklund · Sara Beery · Ian Stavness · Jure Leskovec · Kate Saenko · Tatsunori Hashimoto · Sergey Levine · Chelsea Finn · Percy Liang -
2021 : Implicit Quantile Neural Networks for Jet Simulation and Correction »
Michelle Kuchera · Raghuram Ramanujan -
2022 : Tabular deep learning when $d \gg n$ by using an auxiliary knowledge graph »
Camilo Ruiz · Hongyu Ren · Kexin Huang · Jure Leskovec -
2022 : Learning Controllable Adaptive Simulation for Multi-scale Physics »
Tailin Wu · Takashi Maruyama · Qingqing Zhao · Gordon Wetzstein · Jure Leskovec -
2022 : Learning Efficient Hybrid Particle-continuum Representations of Non-equilibrium N-body Systems »
Tailin Wu · Michael Sun · Hsuan-Gu Chou · Pranay Reddy Samala · Sithipont Cholsaipant · Sophia Kivelson · Jacqueline Yau · Rex Ying · E. Paulo Alves · Jure Leskovec · Frederico Fiuza -
2022 : AutoTransfer: AutoML with Knowledge Transfer - An Application to Graph Neural Networks »
Kaidi Cao · Jiaxuan You · Jiaju Liu · Jure Leskovec -
2022 : Efficient Automatic Machine Learning via Design Graphs »
Shirley Wu · Jiaxuan You · Jure Leskovec · Rex Ying -
2022 Competition: OGB-LSC 2022: A Large-Scale Challenge for ML on Graphs »
Weihua Hu · Matthias Fey · Hongyu Ren · Maho Nakata · Yuxiao Dong · Jure Leskovec -
2022 : Introduction to OGB-LSC »
Jure Leskovec -
2022 Poster: Deep Bidirectional Language-Knowledge Graph Pretraining »
Michihiro Yasunaga · Antoine Bosselut · Hongyu Ren · Xikun Zhang · Christopher D Manning · Percy Liang · Jure Leskovec -
2022 Poster: ZeroC: A Neuro-Symbolic Model for Zero-shot Concept Recognition and Acquisition at Inference Time »
Tailin Wu · Megan Tjandrasuwita · Zhengxuan Wu · Xuelin Yang · Kevin Liu · Rok Sosic · Jure Leskovec -
2022 Poster: Learning to Accelerate Partial Differential Equations via Latent Global Evolution »
Tailin Wu · Takashi Maruyama · Jure Leskovec -
2022 Poster: Few-shot Relational Reasoning via Connection Subgraph Pretraining »
Qian Huang · Hongyu Ren · Jure Leskovec -
2021 Poster: Combiner: Full Attention Transformer with Sparse Computation Cost »
Hongyu Ren · Hanjun Dai · Zihang Dai · Mengjiao (Sherry) Yang · Jure Leskovec · Dale Schuurmans · Bo Dai -
2021 Poster: Modeling Heterogeneous Hierarchies with Relation-specific Hyperbolic Cones »
Yushi Bai · Zhitao Ying · Hongyu Ren · Jure Leskovec -
2021 Poster: Neural Distance Embeddings for Biological Sequences »
Gabriele Corso · Zhitao Ying · Michal Pándy · Petar Veličković · Jure Leskovec · Pietro Liò -
2020 : Q&A #2 »
Heng Ji · Jure Leskovec · Jiajun Wu -
2020 : Invited Talk #4 »
Jure Leskovec -
2020 Poster: Open Graph Benchmark: Datasets for Machine Learning on Graphs »
Weihua Hu · Matthias Fey · Marinka Zitnik · Yuxiao Dong · Hongyu Ren · Bowen Liu · Michele Catasta · Jure Leskovec -
2020 Poster: Coresets for Robust Training of Deep Neural Networks against Noisy Labels »
Baharan Mirzasoleiman · Kaidi Cao · Jure Leskovec -
2020 Poster: Graph Information Bottleneck »
Tailin Wu · Hongyu Ren · Pan Li · Jure Leskovec -
2020 Spotlight: Open Graph Benchmark: Datasets for Machine Learning on Graphs »
Weihua Hu · Matthias Fey · Marinka Zitnik · Yuxiao Dong · Hongyu Ren · Bowen Liu · Michele Catasta · Jure Leskovec -
2020 Poster: Distance Encoding: Design Provably More Powerful Neural Networks for Graph Representation Learning »
Pan Li · Yanbang Wang · Hongwei Wang · Jure Leskovec -
2020 Poster: Handling Missing Data with Graph Representation Learning »
Jiaxuan You · Xiaobai Ma · Yi Ding · Mykel J Kochenderfer · Jure Leskovec -
2020 Poster: Design Space for Graph Neural Networks »
Jiaxuan You · Zhitao Ying · Jure Leskovec -
2020 Poster: Beta Embeddings for Multi-Hop Logical Reasoning in Knowledge Graphs »
Hongyu Ren · Jure Leskovec -
2020 Spotlight: Design Space for Graph Neural Networks »
Jiaxuan You · Zhitao Ying · Jure Leskovec -
2019 : Presentation and Discussion: Open Graph Benchmark »
Jure Leskovec -
2019 Workshop: Graph Representation Learning »
Will Hamilton · Rianne van den Berg · Michael Bronstein · Stefanie Jegelka · Thomas Kipf · Jure Leskovec · Renjie Liao · Yizhou Sun · Petar Veličković -
2019 Poster: Hyperbolic Graph Convolutional Neural Networks »
Ines Chami · Zhitao Ying · Christopher Ré · Jure Leskovec -
2019 Poster: GNNExplainer: Generating Explanations for Graph Neural Networks »
Zhitao Ying · Dylan Bourgeois · Jiaxuan You · Marinka Zitnik · Jure Leskovec -
2018 Poster: Graph Convolutional Policy Network for Goal-Directed Molecular Graph Generation »
Jiaxuan You · Bowen Liu · Zhitao Ying · Vijay Pande · Jure Leskovec -
2018 Poster: Dynamic Network Model from Partial Observations »
Elahe Ghalebi · Baharan Mirzasoleiman · Radu Grosu · Jure Leskovec -
2018 Spotlight: Graph Convolutional Policy Network for Goal-Directed Molecular Graph Generation »
Jiaxuan You · Bowen Liu · Zhitao Ying · Vijay Pande · Jure Leskovec -
2018 Spotlight: Dynamic Network Model from Partial Observations »
Elahe Ghalebi · Baharan Mirzasoleiman · Radu Grosu · Jure Leskovec -
2018 Poster: Hierarchical Graph Representation Learning with Differentiable Pooling »
Zhitao Ying · Jiaxuan You · Christopher Morris · Xiang Ren · Will Hamilton · Jure Leskovec -
2018 Spotlight: Hierarchical Graph Representation Learning with Differentiable Pooling »
Zhitao Ying · Jiaxuan You · Christopher Morris · Xiang Ren · Will Hamilton · Jure Leskovec -
2018 Poster: Embedding Logical Queries on Knowledge Graphs »
Will Hamilton · Payal Bajaj · Marinka Zitnik · Dan Jurafsky · Jure Leskovec -
2017 : Jure Leskovec, Stanford »
Jure Leskovec -
2017 : Towards Verification of Deep Neural Networks »
Clark Barrett -
2017 Poster: Inductive Representation Learning on Large Graphs »
Will Hamilton · Zhitao Ying · Jure Leskovec -
2016 Poster: Confusions over Time: An Interpretable Bayesian Model to Characterize Trends in Decision Making »
Himabindu Lakkaraju · Jure Leskovec -
2013 Workshop: Frontiers of Network Analysis: Methods, Models, and Applications »
Edo M Airoldi · David S Choi · Aaron Clauset · Khalid El-Arini · Jure Leskovec -
2013 Poster: Nonparametric Multi-group Membership Model for Dynamic Networks »
Myunghwan Kim · Jure Leskovec -
2012 Workshop: Social network and social media analysis: Methods, models and applications »
Edo M Airoldi · David S Choi · Khalid El-Arini · Jure Leskovec -
2012 Poster: Learning to Discover Social Circles in Ego Networks »
Julian J McAuley · Jure Leskovec -
2010 Workshop: Networks Across Disciplines: Theory and Applications »
Edo M Airoldi · Anna Goldenberg · Jure Leskovec · Quaid Morris -
2010 Oral: On the Convexity of Latent Social Network Inference »
Seth A Myers · Jure Leskovec -
2010 Poster: On the Convexity of Latent Social Network Inference »
Seth A Myers · Jure Leskovec -
2009 Workshop: Analyzing Networks and Learning With Graphs »
Edo M Airoldi · Jure Leskovec · Jon Kleinberg · Josh Tenenbaum