The Boolean satisfiability problem (SAT) stands as a canonical NP-complete combinatorial optimization (CO) problem, with wide impact on both theoretical and industrial scenarios. In particular, the scarcity of real-world SAT instances and their usefulness for tuning SAT solvers underscore the necessity for effective and efficient ways of hard instance generation, whereas existing methods either struggle to maintain plausible hardness or suffer from limited applicability. Different from the typical construction-based methods, this paper introduces an adaptive and efficient graph interpolation approach that in place modifies the raw structure of graph-represented SAT instance by replacing it with a counterpart from another instance. Specifically, our method involves a two-stage matching and mixing pipeline. The matching aims to find a correspondence map of literal nodes from two instance graphs via learned features from a matching network; while the mixing stage involves iteratively exchanging clause pairs with the highest correspondence scores until a specified replacement ratio is achieved. We further show that under our matching-mixing framework, moderate randomness can avoid hardness degradation of SAT instances by introducing Gumbel noise. Experimental results show the superiority of the proposed method with both resemblance in structure and hardness, as well as general applicability in an efficient way. Source code will be released.
MixSATGEN: Learning Graph Mixing for SAT Instance Generation
Xinyan Chen Yang Li Runzhong Wang Junchi Yan