W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs

TL;DR

W2SAT introduces a novel graph-based framework for generating realistic SAT instances by learning from real-world data, improving the quality and scalability of synthetic SAT formulas for solver tuning.

Contribution

The paper proposes WLIG, a new representation for SAT formulas, and a graph generative model with a hill-climbing decoding method, advancing SAT instance generation techniques.

Findings

WLIG outperforms existing representations in graph metrics

The generative approach is efficient and scalable

Generated instances improve SAT solver parameter tuning

Abstract

The Boolean Satisfiability (SAT) problem stands out as an attractive NP-complete problem in theoretic computer science and plays a central role in a broad spectrum of computing-related applications. Exploiting and tuning SAT solvers under numerous scenarios require massive high-quality industry-level SAT instances, which unfortunately are quite limited in the real world. To address the data insufficiency issue, in this paper, we propose W2SAT, a framework to generate SAT formulas by learning intrinsic structures and properties from given real-world/industrial instances in an implicit fashion. To this end, we introduce a novel SAT representation called Weighted Literal Incidence Graph (WLIG), which exhibits strong representation ability and generalizability against existing counterparts, and can be efficiently generated via a specialized learning-based graph generative model. Decoding from WLIGs into SAT problems is then modeled as finding overlapping cliques with a novel hill-climbing optimization method termed Optimal Weight Coverage (OWC). Experiments demonstrate the superiority of our WLIG-induced approach in terms of graph metrics, efficiency, and scalability in comparison to previous methods. Additionally, we discuss the limitations of graph-based SAT generation for real-world applications, especially when utilizing generated instances for SAT solver parameter-tuning, and pose some potential directions.