Timezone: »

 
Poster
G2SAT: Learning to Generate SAT Formulas
Jiaxuan You · Haoze Wu · Clark Barrett · Raghuram Ramanujan · Jure Leskovec

Wed Dec 11 10:45 AM -- 12:45 PM (PST) @ East Exhibition Hall B + C #114
in Deep Learning -- Generative Models »

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.

Keywords: Generative Models · Network Analysis · Deep Learning · Algorithms -> Relational Learning; Applications
[ Paper]  [ Poster] 

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