AI帮你理解科学

AI 生成解读视频

AI抽取解析论文重点内容自动生成视频


pub
生成解读视频

AI 溯源

AI解析本论文相关学术脉络


Master Reading Tree
生成 溯源树

AI 精读

AI抽取本论文的概要总结


微博一下
In contrast to existing SAT generators, G2SAT does not rely on hand-crafted algorithms and is able to generate diverse SAT formulas similar to input formulas, as measured by many graph statistics and SAT solver performance

G2SAT: Learning to Generate SAT Formulas

ADVANCES IN NEURAL INFORMATION PROCESSING SYSTEMS 32 (NIPS 2019), (2019): 10552-10563

被引用10|浏览172
EI WOS
下载 PDF 全文
引用
微博一下

摘要

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 for-mulas. However, t...更多

代码

数据

0
简介
  • The Boolean Satisfiability (SAT) problem is central to computer science, and finds many applications across Artificial Intelligence, including planning [24], verification [7], and theorem proving [14].
  • SAT was the first problem to be shown to be NP-complete [9], and there is believed to be no general procedure for solving arbitrary SAT instances efficiently.
  • Incomplete search methods such as WalkSAT [35] and survey propagation [6] are more effective at solving large, randomly generated formulas, while complete solvers leveraging conflict-driven clause learning (CDCL) [30] fare better on large structured SAT formulas that commonly arise in industrial settings.
重点内容
  • The Boolean Satisfiability (SAT) problem is central to computer science, and finds many applications across Artificial Intelligence, including planning [24], verification [7], and theorem proving [14]
  • We present G2SAT, the first deep generative model that learns to generate SAT formulas based on a given set of input formulas
  • We report the relative SAT solver performance, i.e., given k SAT solvers, we rank them based on their performance over the SAT formulas used for training and the generated SAT formulas, and evaluate how well the two rankings align
  • We compute the relative error over the generated graph statistics with respect to the ground-truth statistics, and G2SAT can reduce the relative error by 24% on average compared with baseline methods
  • We introduced G2SAT, the first deep generative model for SAT formulas
  • In contrast to existing SAT generators, G2SAT does not rely on hand-crafted algorithms and is able to generate diverse SAT formulas similar to input formulas, as measured by many graph statistics and SAT solver performance
方法
  • Configurations, G2SAT is the only method that finds one that results in a large performance gain (18% faster run time) on unobserved SAT formulas.
  • This experiment is limited in scale, the promising results indicate that G2SAT could open up opportunities for developing better SAT solvers, even in application domains where benchmarks are scarce.
  • The authors found that G2SAT scales roughly linearly for both tasks with respect to the number of clauses
结果
  • The authors compute the relative error over the generated graph statistics with respect to the ground-truth statistics, and G2SAT can reduce the relative error by 24% on average compared with baseline methods.
  • To further illustrate this performance gain, the authors plot the distribution of the selected properties over the generated formulas in Figure 2, where each dot corresponds to a graph.
  • The authors see that G2SAT nicely interpolates and extrapolates on all the statistics of the input graphs, while the baselines only do well on some of the statistics
结论
  • The authors introduced G2SAT, the first deep generative model for SAT formulas.
  • In contrast to existing SAT generators, G2SAT does not rely on hand-crafted algorithms and is able to generate diverse SAT formulas similar to input formulas, as measured by many graph statistics and SAT solver performance.
  • While future work is called for to generate larger and harder formulas, the authors believe the framework shows great potential for understanding and improving SAT solvers
总结
  • Introduction:

    The Boolean Satisfiability (SAT) problem is central to computer science, and finds many applications across Artificial Intelligence, including planning [24], verification [7], and theorem proving [14].
  • SAT was the first problem to be shown to be NP-complete [9], and there is believed to be no general procedure for solving arbitrary SAT instances efficiently.
  • Incomplete search methods such as WalkSAT [35] and survey propagation [6] are more effective at solving large, randomly generated formulas, while complete solvers leveraging conflict-driven clause learning (CDCL) [30] fare better on large structured SAT formulas that commonly arise in industrial settings.
  • Objectives:

    The authors' goal is to design a SAT generator that, given a suite of SAT formulas, generates new SAT formulas with similar properties.
  • The authors' aim is to capture graph theoretic properties, and realistic SAT solver behavior.
  • NeuroSAT focuses on using the embeddings to solve SAT formulas, while the authors aim to generate SAT formulas
  • Methods:

    Configurations, G2SAT is the only method that finds one that results in a large performance gain (18% faster run time) on unobserved SAT formulas.
  • This experiment is limited in scale, the promising results indicate that G2SAT could open up opportunities for developing better SAT solvers, even in application domains where benchmarks are scarce.
  • The authors found that G2SAT scales roughly linearly for both tasks with respect to the number of clauses
  • Results:

    The authors compute the relative error over the generated graph statistics with respect to the ground-truth statistics, and G2SAT can reduce the relative error by 24% on average compared with baseline methods.
  • To further illustrate this performance gain, the authors plot the distribution of the selected properties over the generated formulas in Figure 2, where each dot corresponds to a graph.
  • The authors see that G2SAT nicely interpolates and extrapolates on all the statistics of the input graphs, while the baselines only do well on some of the statistics
  • Conclusion:

    The authors introduced G2SAT, the first deep generative model for SAT formulas.
  • In contrast to existing SAT generators, G2SAT does not rely on hand-crafted algorithms and is able to generate diverse SAT formulas similar to input formulas, as measured by many graph statistics and SAT solver performance.
  • While future work is called for to generate larger and harder formulas, the authors believe the framework shows great potential for understanding and improving SAT solvers
表格
  • Table1: Graph statistics of generated formulas (mean ± std. (relative error to training formulas))
  • Table2: Relative SAT Solver Performance
  • Table3: Performance gain when using generated on training as well as synthetic SAT formulas. SAT formulas to tune SAT solvers
Download tables as Excel
相关工作
  • SAT Generators. Existing synthetic SAT generators are hand-crafted models that are typically designed to generate formulas that fit a particular graph statistic. The mainstream generators for pseudo-industrial SAT instances include the Community Attachment (CA) model [15], which generates formulas with a given VIG modularity, and the Popularity-Similarity (PS) model [16], which generates formulas with a specific VCG degree distribution. In addition, there are also generators for random k-SAT instances [5] and crafted instances that come from translations of structured combinatorial problems, such as graph coloring, graph isomorphism, and Ramsey numbers [28]. Currently, all SAT generators are hand-crafted and machine learning provides an exciting alternative.

    Deep Graph Generators. Existing deep generative models of graphs fall into two categories. In the first class are models that focus on generating perturbations of a given graph, by direct decoding from computed node embeddings [26] or latent variables [17], or learning the random walk distribution of a graph [4]. The second class comprises models that can learn to generate a graph by sequentially adding nodes and edges [29, 45, 43]. Domain specific generators for molecular graphs [10, 22] and 3D point cloud graphs [40] have also been developed. However, current deep generative models of graphs do not readily apply to SAT instance generation. Thus, we develop a novel bipartite graph generator that respects all the constraints imposed by graphical representations of SAT formulas and generates the formula graph via a sequence of node merging operations.
基金
  • We gratefully acknowledge the support of DARPA under No FA865018C7880 (ASED) and MSC; NIH under No U54EB020405 (Mobilize); ARO under No 38796-Z8424103 (MURI); IARPA under No 2017-17071900005 (HFC); NSF under No OAC-1835598 (CINES) and HDR; Stanford Data Science Initiative, Chan Zuckerberg Biohub, Enlight Foundation, JD.com, Amazon, Boeing, Docomo, Huawei, Hitachi, Observe, Siemens, UST Global
引用论文
  • C. Ansótegui, M. L. Bonet, and J. Levy. On the structure of industrial sat instances. In Principles and Practice of Constraint Programming, pages 127–14Springer Berlin Heidelberg, 2009.
    Google ScholarLocate open access versionFindings
  • G. Audemard and L. Simon. Predicting learnt clauses quality in modern sat solvers. In Proceedings of the 21st International Joint Conference on Artifical Intelligence, pages 399–404, 2009.
    Google ScholarLocate open access versionFindings
  • A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
    Google ScholarFindings
  • A. Bojchevski, O. Shchur, D. Zügner, and S. Günnemann. NetGAN: Generating graphs via random walks. In Proceedings of the 35th International Conference on Machine Learning, 2018.
    Google ScholarLocate open access versionFindings
  • Y. Boufkhad, O. Dubois, Y. Interian, and B. Selman. Regular random k-sat: Properties of balanced formulas. J. Autom. Reason., 35:181–200, 2005.
    Google ScholarLocate open access versionFindings
  • A. Braunstein, M. Mézard, and R. Zecchina. Survey propagation: An algorithm for satisfiability. Random Struct. Algorithms, 27:201–226, 2005.
    Google ScholarLocate open access versionFindings
  • E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Form. Methods Syst. Des., 19:7–34, 2001.
    Google ScholarLocate open access versionFindings
  • A. Clauset, C. R. Shalizi, and M. E. J. Newman. Power-law distributions in empirical data. SIAM Review, 51:661–703, 2009.
    Google ScholarLocate open access versionFindings
  • S. A. Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, pages 151–158. ACM, 1971.
    Google ScholarLocate open access versionFindings
  • N. De Cao and T. Kipf. Molgan: An implicit generative model for small molecular graphs. arXiv preprint arXiv:1805.11973, 2018.
    Findings
  • N. Eén and A. Biere. Effective preprocessing in sat through variable and clause elimination. In International conference on theory and applications of satisfiability testing, pages 61–75.
    Google ScholarLocate open access versionFindings
  • N. Eén and N. Sörensson. An extensible sat-solver. In Theory and Applications of Satisfiability Testing, pages 502–518. Springer Berlin Heidelberg, 2004.
    Google ScholarLocate open access versionFindings
  • G. Escamocher, B. O’Sullivan, and S. D. Prestwich. Generating difficult sat instances by preventing triangles. CoRR, abs/1903.03592, 2019.
    Findings
  • H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Dpll(t): Fast decision procedures. In R. Alur and D. A. Peled, editors, Computer Aided Verification, pages 175–188. Springer Berlin Heidelberg, 2004.
    Google ScholarLocate open access versionFindings
  • J. Giráldez-Cru and J. Levy. A modularity-based random sat instances generator. In Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI’15, pages 1952–1958. AAAI Press, 2015.
    Google ScholarLocate open access versionFindings
  • J. Giráldez-Cru and J. Levy. Locality in random sat instances. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pages 638–644, 2017.
    Google ScholarLocate open access versionFindings
  • A. Grover, A. Zweig, and S. Ermon. Graphite: Iterative generative modeling of graphs. arXiv preprint arXiv:1803.10459, 2018.
    Findings
  • W. Hamilton, Z. Ying, and J. Leskovec. Inductive representation learning on large graphs. In Advances in Neural Information Processing Systems, 2017.
    Google ScholarLocate open access versionFindings
  • W. L. Hamilton, R. Ying, and J. Leskovec. Representation learning on graphs: Methods and applications. IEEE Data Engineering Bulletin, 2017.
    Google ScholarLocate open access versionFindings
  • M. J. Heule, M. J. Järvisalo, M. Suda, et al. Proceedings of sat competition 2018. 2018.
    Google ScholarLocate open access versionFindings
  • H. H. Hoos and T. Stützle. Satlib: An online resource for research on sat. Sat, 2000:283–292, 2000.
    Google ScholarLocate open access versionFindings
  • W. Jin, R. Barzilay, and T. Jaakkola. Junction tree variational autoencoder for molecular graph generation. International Conference on Machine Learning, 2018.
    Google ScholarLocate open access versionFindings
  • G. Katsirelos and L. Simon. Eigenvector centrality in industrial sat instances. In Principles and Practice of Constraint Programming, pages 348–356. Springer Berlin Heidelberg, 2012.
    Google ScholarLocate open access versionFindings
  • H. Kautz and B. Selman. Planning as satisfiability. In Proceedings of the 10th European Conference on Artificial Intelligence, pages 359–363. John Wiley & Sons, Inc., 1992.
    Google ScholarLocate open access versionFindings
  • D. P. Kingma and J. Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014.
    Findings
  • T. N. Kipf and M. Welling. Variational graph auto-encoders. arXiv preprint arXiv:1611.07308, 2016.
    Findings
  • T. N. Kipf and M. Welling. Semi-supervised classification with graph convolutional networks. International Conference on Learning Representations, 2017.
    Google ScholarLocate open access versionFindings
  • M. Lauria, J. Elffers, J. Nordström, and M. Vinyals. Cnfgen: A generator of crafted benchmarks. In S. Gaspers and T. Walsh, editors, Theory and Applications of Satisfiability Testing, pages 464–473. Springer International Publishing, 2017.
    Google ScholarLocate open access versionFindings
  • Y. Li, O. Vinyals, C. Dyer, R. Pascanu, and P. Battaglia. Learning deep generative models of graphs. arXiv preprint arXiv:1803.03324, 2018.
    Findings
  • J. Marques-Silva, I. Lynce, and S. Malik. Conflict-driven clause learning sat solvers. In Handbook of Satisfiability, 2009.
    Google ScholarLocate open access versionFindings
  • N. Mull, D. J. Fremont, and S. A. Seshia. On the hardness of sat with community structure. In N. Creignou and D. Le Berre, editors, Theory and Applications of Satisfiability Testing, pages 141–159. Springer International Publishing, 2016.
    Google ScholarLocate open access versionFindings
  • M. E. Newman. Clustering and preferential attachment in growing networks. Physical review E, 64(2), 2001.
    Google ScholarLocate open access versionFindings
  • M. E. Newman. Modularity and community structure in networks. Proceedings of the national academy of sciences, 103(23):8577–8582, 2006.
    Google ScholarLocate open access versionFindings
  • Z. Newsham, V. Ganesh, S. Fischmeister, G. Audemard, and L. Simon. Impact of community structure on sat solver performance. In Theory and Applications of Satisfiability Testing, pages 252–268. Springer International Publishing, 2014.
    Google ScholarLocate open access versionFindings
  • B. Selman, H. Kautz, and B. Cohen. Local search strategies for satisfiability testing. Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, 26, 09 1999.
    Google ScholarLocate open access versionFindings
  • B. Selman, H. Kautz, and D. McAllester. Ten challenges in propositional reasoning and search. In Proceedings of the 15th International Joint Conference on Artificial Intelligence - Volume 1, IJCAI’97, pages 50–54, San Francisco, CA, USA, 1997. Morgan Kaufmann Publishers Inc.
    Google ScholarLocate open access versionFindings
  • B. Selman, D. G. Mitchell, and H. J. Levesque. Generating hard satisfiability problems. Artif. Intell., 81:17–29, 1996.
    Google ScholarLocate open access versionFindings
  • D. Selsam, M. Lamm, B. Bünz, P. Liang, L. de Moura, and D. L. Dill. Learning a sat solver from single-bit supervision. arXiv preprint arXiv:1802.03685, 2018.
    Findings
  • G. S. TSEITIN. On the complexity of derivation in propositional calculus. Structures in Constructive Mathematics and Mathematical Logic, pages 115–125, 1968.
    Google ScholarLocate open access versionFindings
  • D. Valsesia, G. Fracastoro, and E. Magli. Learning localized generative models for 3d point clouds via graph convolution. International Conference on Learning Representations, 2019.
    Google ScholarLocate open access versionFindings
  • H. Wu and R. Ramanujan. Learning to generate industrial sat instances. In Proceedings of the 12th International Symposium on Combinatorial Search, pages 17–29. AAAI Press, 2019.
    Google ScholarLocate open access versionFindings
  • K. Xu, F. Boussemart, F. Hemery, and C. Lecoutre. A simple model to generate hard satisfiable instances. In Proceedings of the 19th International Joint Conference on Artificial Intelligence, 2005.
    Google ScholarLocate open access versionFindings
  • J. You, B. Liu, R. Ying, V. Pande, and J. Leskovec. Graph convolutional policy network for goal-directed molecular graph generation. Advances in Neural Information Processing Systems, 2018.
    Google ScholarLocate open access versionFindings
  • J. You, R. Ying, and J. Leskovec. Position-aware graph neural networks. International Conference on Machine Learning, 2019.
    Google ScholarLocate open access versionFindings
  • J. You, R. Ying, X. Ren, W. Hamilton, and J. Leskovec. GraphRNN: Generating realistic graphs with deep auto-regressive models. In International Conference on Machine Learning, 2018.
    Google ScholarLocate open access versionFindings
作者
Haoze Wu
Haoze Wu
Raghuram Ramanujan
Raghuram Ramanujan
您的评分 :
0

 

标签
评论
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科