{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T14:44:58Z","timestamp":1751035498064,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,8,4]],"date-time":"2023-08-04T00:00:00Z","timestamp":1691107200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSFC","award":["62222607"],"award-info":[{"award-number":["62222607"]}]},{"name":"Science and Technology Commission of Shanghai Municipality","award":["22511105100"],"award-info":[{"award-number":["22511105100"]}]},{"name":"China Key Research and Development Program","award":["2020AAA0107600"],"award-info":[{"award-number":["2020AAA0107600"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,8,6]]},"DOI":"10.1145\/3580305.3599837","type":"proceedings-article","created":{"date-parts":[[2023,8,4]],"date-time":"2023-08-04T18:13:58Z","timestamp":1691172838000},"page":"4414-4425","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5249-3471","authenticated-orcid":false,"given":"Yang","family":"Li","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6336-3819","authenticated-orcid":false,"given":"Xinyan","family":"Chen","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6336-3819","authenticated-orcid":false,"given":"Wenxuan","family":"Guo","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9013-1180","authenticated-orcid":false,"given":"Xijun","family":"Li","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2638-1382","authenticated-orcid":false,"given":"Wanqian","family":"Luo","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8995-5879","authenticated-orcid":false,"given":"Junhua","family":"Huang","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0310-3825","authenticated-orcid":false,"given":"Hui-Ling","family":"Zhen","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Hong Kong, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2236-8784","authenticated-orcid":false,"given":"Mingxuan","family":"Yuan","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Hong Kong, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9639-7679","authenticated-orcid":false,"given":"Junchi","family":"Yan","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}]}],"member":"320","published-online":{"date-parts":[[2023,8,4]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"International Conference on Learning Representations.","author":"Amizadeh Saeed","year":"2018","unstructured":"Saeed Amizadeh , Sergiy Matusevych , and Markus Weimer . 2018 . Learning to Solve Circuit-SAT: An Unsupervised Differentiable Approach . In International Conference on Learning Representations. Saeed Amizadeh, Sergiy Matusevych, and Markus Weimer. 2018. Learning to Solve Circuit-SAT: An Unsupervised Differentiable Approach. In International Conference on Learning Representations."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04244-7_13"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661507"},{"key":"e_1_3_2_2_4_1","volume-title":"Glucose: a solver that predicts learnt clauses quality. SAT Competition","author":"Audemard Gilles","year":"2009","unstructured":"Gilles Audemard and Laurent Simon . 2009. Glucose: a solver that predicts learnt clauses quality. SAT Competition ( 2009 ), 7--8. Gilles Audemard and Laurent Simon. 2009. Glucose: a solver that predicts learnt clauses quality. SAT Competition (2009), 7--8."},{"key":"e_1_3_2_2_5_1","unstructured":"Thomas Aynaud. 2018. Community detection for NetworkX's documentation.  Thomas Aynaud. 2018. Community detection for NetworkX's documentation."},{"key":"e_1_3_2_2_6_1","volume-title":"Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. Department of Computer Science","author":"Balyo Tom\u00e1\u0161","year":"2021","unstructured":"Tom\u00e1\u0161 Balyo , Nils Froleyks , Marijn Heule , Markus Iser , Matti J\u011arvisalo , and Martin Suda ( Eds .). 2021 . Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. Department of Computer Science , University of Helsinki, Finland. Tom\u00e1\u0161 Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J\u011arvisalo, and Martin Suda (Eds.). 2021. Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. Department of Computer Science, University of Helsinki, Finland."},{"key":"e_1_3_2_2_7_1","volume-title":"Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions. Department of Computer Science","author":"Balyo Tomas","year":"2022","unstructured":"Tomas Balyo , Marijn J.H. Heule , Markus Iser , Matti J\u00e4rvisalo , and Martin Suda ( Eds .). 2022 . Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions. Department of Computer Science , University of Helsinki, Finland. Tomas Balyo, Marijn J.H. Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.). 2022. Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions. Department of Computer Science, University of Helsinki, Finland."},{"key":"e_1_3_2_2_8_1","first-page":"111","article-title":"The effect of scrambling CNFs","volume":"59","author":"Biere Armin","year":"2019","unstructured":"Armin Biere and Marijn Heule . 2019 . The effect of scrambling CNFs . In Proceedings of Pragmatics of SAT , Vol. 59. 111 -- 126 . Armin Biere and Marijn Heule. 2019. The effect of scrambling CNFs. In Proceedings of Pragmatics of SAT, Vol. 59. 111--126.","journal-title":"Proceedings of Pragmatics of SAT"},{"volume-title":"Handbook of satisfiability","author":"Biere Armin","key":"e_1_3_2_2_9_1","unstructured":"Armin Biere , Marijn Heule , and Hans van Maaren . 2009. Handbook of satisfiability . Vol. 185 . IOS press . Armin Biere, Marijn Heule, and Hans van Maaren. 2009. Handbook of satisfiability. Vol. 185. IOS press."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1088\/1742-5468\/2008\/10\/P10008"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3459637.3482321"},{"key":"e_1_3_2_2_12_1","volume-title":"Mark EJ Newman, and Cristopher Moore","author":"Clauset Aaron","year":"2004","unstructured":"Aaron Clauset , Mark EJ Newman, and Cristopher Moore . 2004 . Finding community structure in very large networks. Physical review E, Vol. 70 , 6 (2004), 066111. Aaron Clauset, Mark EJ Newman, and Cristopher Moore. 2004. Finding community structure in very large networks. Physical review E, Vol. 70, 6 (2004), 066111."},{"key":"e_1_3_2_2_13_1","series-title":"SIAM review","volume-title":"Power-law distributions in empirical data","author":"Clauset Aaron","year":"2009","unstructured":"Aaron Clauset and Cosma Rohilla Shalizi . 2009. Power-law distributions in empirical data . SIAM review , Vol. 51 , 4 ( 2009 ), 661--703. Aaron Clauset and Cosma Rohilla Shalizi. 2009. Power-law distributions in empirical data. SIAM review, Vol. 51, 4 (2009), 661--703."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_2_15_1","article-title":"HEBO: Pushing The Limits of Sample-Efficient Hyperparameter Optimisation","volume":"74","author":"Cowen-Rivers Alexander","year":"2022","unstructured":"Alexander Cowen-Rivers , Wenlong Lyu , Rasul Tutunov , Zhi Wang , Antoine Grosnit , Ryan-Rhys Griffiths , Alexandre Maravel , Jianye Hao , Jun Wang , Jan Peters , and Haitham Bou Ammar . 2022 . HEBO: Pushing The Limits of Sample-Efficient Hyperparameter Optimisation . Journal of Artificial Intelligence Research , Vol. 74 (07 2022). Alexander Cowen-Rivers, Wenlong Lyu, Rasul Tutunov, Zhi Wang, Antoine Grosnit, Ryan-Rhys Griffiths, Alexandre Maravel, Jianye Hao, Jun Wang, Jan Peters, and Haitham Bou Ammar. 2022. HEBO: Pushing The Limits of Sample-Efficient Hyperparameter Optimisation. Journal of Artificial Intelligence Research, Vol. 74 (07 2022).","journal-title":"Journal of Artificial Intelligence Research"},{"key":"e_1_3_2_2_16_1","first-page":"2020","article-title":"CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020","volume":"50","author":"Katalin Fazekas Mathias Fleury Armin Biere","year":"2020","unstructured":"Armin Biere Katalin Fazekas Mathias Fleury and Maximilian Heisinger . 2020 . CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020 . SAT COMPETITION , Vol. 50 (2020), 2020 . Armin Biere Katalin Fazekas Mathias Fleury and Maximilian Heisinger. 2020. CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020. SAT COMPETITION, Vol. 50 (2020), 2020.","journal-title":"SAT COMPETITION"},{"key":"e_1_3_2_2_17_1","volume-title":"Graph drawing by force-directed placement. Software: Practice and experience","author":"Fruchterman Thomas MJ","year":"1991","unstructured":"Thomas MJ Fruchterman and Edward M Reingold . 1991. Graph drawing by force-directed placement. Software: Practice and experience , Vol. 21 , 11 ( 1991 ), 1129--1164. Thomas MJ Fruchterman and Edward M Reingold. 1991. Graph drawing by force-directed placement. Software: Practice and experience, Vol. 21, 11 (1991), 1129--1164."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"e_1_3_2_2_19_1","volume-title":"On the Performance of Deep Generative Models of Realistic SAT Instances. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT","author":"Garz\u00f3n Iv\u00e1n","year":"2022","unstructured":"Iv\u00e1n Garz\u00f3n , Pablo Mesejo , and Jes\u00fas Gir\u00e1ldez-Cru . 2022 . On the Performance of Deep Generative Models of Realistic SAT Instances. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Iv\u00e1n Garz\u00f3n, Pablo Mesejo, and Jes\u00fas Gir\u00e1ldez-Cru. 2022. On the Performance of Deep Generative Models of Realistic SAT Instances. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)."},{"key":"e_1_3_2_2_20_1","volume-title":"Proceedings of the ACM SIGKDD International Conference on Knowledge Discovery and Data Mining.","author":"Geng Haoyu","year":"2023","unstructured":"Haoyu Geng , Runzhong Wang , Fei Wu , and Junchi Yan . 2023 . GAL-VNE: Solving the VNE Problem with Global Reinforcement Learning and Local One-Shot Neural Prediction . In Proceedings of the ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. Haoyu Geng, Runzhong Wang, Fei Wu, and Junchi Yan. 2023. GAL-VNE: Solving the VNE Problem with Global Reinforcement Learning and Local One-Shot Neural Prediction. In Proceedings of the ACM SIGKDD International Conference on Knowledge Discovery and Data Mining."},{"key":"e_1_3_2_2_21_1","volume-title":"Twenty-Fourth International Joint Conference on Artificial Intelligence.","author":"Gir\u00e1ldez-Cru Jes\u00fas","year":"2015","unstructured":"Jes\u00fas Gir\u00e1ldez-Cru and Jordi Levy . 2015 . A modularity-based random SAT instances generator . In Twenty-Fourth International Joint Conference on Artificial Intelligence. Jes\u00fas Gir\u00e1ldez-Cru and Jordi Levy. 2015. A modularity-based random SAT instances generator. In Twenty-Fourth International Joint Conference on Artificial Intelligence."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/89"},{"key":"e_1_3_2_2_23_1","volume-title":"Machine Learning Methods in Solving the Boolean Satisfiability Problem. Machine Intelligence Research","author":"Guo Wenxuan","year":"2023","unstructured":"Wenxuan Guo , Hui-Ling Zhen , Xijun Li , Wanqian Luo , Mingxuan Yuan , Yaohui Jin , and Junchi Yan . 2023. Machine Learning Methods in Solving the Boolean Satisfiability Problem. Machine Intelligence Research ( 2023 ). https:\/\/doi.org\/10.1007\/s11633-022-1396-2 10.1007\/s11633-022-1396-2 Wenxuan Guo, Hui-Ling Zhen, Xijun Li, Wanqian Luo, Mingxuan Yuan, Yaohui Jin, and Junchi Yan. 2023. Machine Learning Methods in Solving the Boolean Satisfiability Problem. Machine Intelligence Research (2023). https:\/\/doi.org\/10.1007\/s11633-022-1396-2"},{"key":"e_1_3_2_2_24_1","volume-title":"Inductive representation learning on large graphs. Advances in neural information processing systems","author":"Hamilton Will","year":"2017","unstructured":"Will Hamilton , Zhitao Ying , and Jure Leskovec . 2017. Inductive representation learning on large graphs. Advances in neural information processing systems , Vol. 30 ( 2017 ). Will Hamilton, Zhitao Ying, and Jure Leskovec. 2017. Inductive representation learning on large graphs. Advances in neural information processing systems, Vol. 30 (2017)."},{"key":"e_1_3_2_2_25_1","volume-title":"Enhancing SAT solvers with glue variable predictions. arXiv preprint arXiv:2007.02559","author":"Han Jesse Michael","year":"2020","unstructured":"Jesse Michael Han . 2020. Enhancing SAT solvers with glue variable predictions. arXiv preprint arXiv:2007.02559 ( 2020 ). Jesse Michael Han. 2020. Enhancing SAT solvers with glue variable predictions. arXiv preprint arXiv:2007.02559 (2020)."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEST.2010.5699215"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505515.2505577"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Dirk Jansen et al. 2003. The electronic design automation handbook. Springer.  Dirk Jansen et al. 2003. The electronic design automation handbook. Springer.","DOI":"10.1007\/978-0-387-73543-6"},{"key":"e_1_3_2_2_29_1","volume-title":"Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence.","author":"Kautz H","year":"1997","unstructured":"H Kautz , D McAllester , and B Selman . 1997 . Ten challenges in propositional reasoning and search . In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence. H Kautz, D McAllester, and B Selman. 1997. Ten challenges in propositional reasoning and search. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45193-8_1"},{"key":"e_1_3_2_2_31_1","volume-title":"Semi-supervised classification with graph convolutional networks. arXiv preprint arXiv:1609.02907","author":"Kipf Thomas N","year":"2016","unstructured":"Thomas N Kipf and Max Welling . 2016. Semi-supervised classification with graph convolutional networks. arXiv preprint arXiv:1609.02907 ( 2016 ). Thomas N Kipf and Max Welling. 2016. Semi-supervised classification with graph convolutional networks. arXiv preprint arXiv:1609.02907 (2016)."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_34"},{"volume-title":"Kissat Cfexp: Adaptive Restart Policy and Variable Scoring Improvement. SAT COMPETITION 2022 ([n.,d.]), 39","author":"Li Yang","key":"e_1_3_2_2_33_1","unstructured":"Yang Li , Yuqi Jia , Wanqian Luo , Hui-Ling Zhen , Xijun Li , Mingxuan Yuan , and Junchi Yan . [n.,d.]. Kissat Adaptive Restart , Kissat Cfexp: Adaptive Restart Policy and Variable Scoring Improvement. SAT COMPETITION 2022 ([n.,d.]), 39 . Yang Li, Yuqi Jia, Wanqian Luo, Hui-Ling Zhen, Xijun Li, Mingxuan Yuan, and Junchi Yan. [n.,d.]. Kissat Adaptive Restart, Kissat Cfexp: Adaptive Restart Policy and Variable Scoring Improvement. SAT COMPETITION 2022 ([n.,d.]), 39."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485447.3512196"},{"key":"e_1_3_2_2_35_1","unstructured":"In\u00eas Lynce and Joao P Marques-Silva. 2004. On computing minimum unsatisfiable cores. (2004).  In\u00eas Lynce and Joao P Marques-Silva. 2004. On computing minimum unsatisfiable cores. (2004)."},{"volume-title":"Handbook of satisfiability","author":"Marques-Silva Joao","key":"e_1_3_2_2_36_1","unstructured":"Joao Marques-Silva , In\u00eas Lynce , and Sharad Malik . 2021. Conflict-driven clause learning SAT solvers . In Handbook of satisfiability . IOS press , 133--182. Joao Marques-Silva, In\u00eas Lynce, and Sharad Malik. 2021. Conflict-driven clause learning SAT solvers. In Handbook of satisfiability. IOS press, 133--182."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_13"},{"key":"e_1_3_2_2_38_1","volume-title":"Clustering and preferential attachment in growing networks. Physical review E","author":"Newman Mark EJ","year":"2001","unstructured":"Mark EJ Newman . 2001. Clustering and preferential attachment in growing networks. Physical review E , Vol. 64 , 2 ( 2001 ), 025102. Mark EJ Newman. 2001. Clustering and preferential attachment in growing networks. Physical review E, Vol. 64, 2 (2001), 025102."},{"key":"e_1_3_2_2_39_1","volume-title":"Finding and evaluating community structure in networks. Physical review E","author":"Newman Mark EJ","year":"2004","unstructured":"Mark EJ Newman and Michelle Girvan . 2004. Finding and evaluating community structure in networks. Physical review E , Vol. 69 , 2 ( 2004 ), 026113. Mark EJ Newman and Michelle Girvan. 2004. Finding and evaluating community structure in networks. Physical review E, Vol. 69, 2 (2004), 026113."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_20"},{"key":"e_1_3_2_2_41_1","volume-title":"Goal-Aware Neural SAT Solver. In International Joint Conference on Neural Networks.","author":"Ozolins Emils","year":"2022","unstructured":"Emils Ozolins , Karlis Freivalds , Andis Draguns , Eliza Gaile , Ronalds Zakovskis , and Sergejs Kozlovics . 2022 . Goal-Aware Neural SAT Solver. In International Joint Conference on Neural Networks. Emils Ozolins, Karlis Freivalds, Andis Draguns, Eliza Gaile, Ronalds Zakovskis, and Sergejs Kozlovics. 2022. Goal-Aware Neural SAT Solver. In International Joint Conference on Neural Networks."},{"key":"e_1_3_2_2_42_1","volume-title":"On lines and planes of closest fit to systems of points in space. The London, Edinburgh, and Dublin philosophical magazine and journal of science","author":"Pearson Karl","year":"1901","unstructured":"Karl Pearson . 1901. LIII. On lines and planes of closest fit to systems of points in space. The London, Edinburgh, and Dublin philosophical magazine and journal of science , Vol. 2 , 11 ( 1901 ), 559--572. Karl Pearson. 1901. LIII. On lines and planes of closest fit to systems of points in space. The London, Edinburgh, and Dublin philosophical magazine and journal of science, Vol. 2, 11 (1901), 559--572."},{"key":"e_1_3_2_2_43_1","volume-title":"NeuroCore: Guiding high-performance SAT solvers with unsat-core predictions. CoRR","author":"Selsam Daniel","year":"2019","unstructured":"Daniel Selsam and Nikolaj Bj\u00f8rner . 2019. NeuroCore: Guiding high-performance SAT solvers with unsat-core predictions. CoRR ( 2019 ). Daniel Selsam and Nikolaj Bj\u00f8rner. 2019. NeuroCore: Guiding high-performance SAT solvers with unsat-core predictions. CoRR (2019)."},{"volume-title":"International Conference on Learning Representations.","author":"Selsam Daniel","key":"e_1_3_2_2_44_1","unstructured":"Daniel Selsam , Matthew Lamm , Benedikt B\u00fcnz , Percy Liang , Leonardo de Moura , and David L. Dill . 2019. Learning a SAT Solver from Single-Bit Supervision . In International Conference on Learning Representations. Daniel Selsam, Matthew Lamm, Benedikt B\u00fcnz, Percy Liang, Leonardo de Moura, and David L. Dill. 2019. Learning a SAT Solver from Single-Bit Supervision. In International Conference on Learning Representations."},{"key":"e_1_3_2_2_45_1","volume-title":"LinSATNet: The Positive Linear Satisfiability Neural Networks. In International Conference on Machine Learning.","author":"Wang Runzhong","year":"2023","unstructured":"Runzhong Wang , Yunhao Zhang , Ziao Guo , Tianyi Chen , Xiaokang Yang , and Junchi Yan . 2023 . LinSATNet: The Positive Linear Satisfiability Neural Networks. In International Conference on Machine Learning. Runzhong Wang, Yunhao Zhang, Ziao Guo, Tianyi Chen, Xiaokang Yang, and Junchi Yan. 2023. LinSATNet: The Positive Linear Satisfiability Neural Networks. In International Conference on Machine Learning."},{"key":"e_1_3_2_2_46_1","volume-title":"Marijn JH Heule, and Warren A Hunt","author":"Wetzler Nathan","year":"2014","unstructured":"Nathan Wetzler , Marijn JH Heule, and Warren A Hunt . 2014 . DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing. Springer , 422--429. Nathan Wetzler, Marijn JH Heule, and Warren A Hunt. 2014. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing. Springer, 422--429."},{"key":"e_1_3_2_2_47_1","volume-title":"Twelfth Annual Symposium on Combinatorial Search.","author":"Wu Haoze","year":"2019","unstructured":"Haoze Wu and Raghuram Ramanujan . 2019 . Learning to generate industrial sat instances . In Twelfth Annual Symposium on Combinatorial Search. Haoze Wu and Raghuram Ramanujan. 2019. Learning to generate industrial sat instances. In Twelfth Annual Symposium on Combinatorial Search."},{"key":"e_1_3_2_2_48_1","volume-title":"International conference on machine learning. PMLR, 10831--10841","author":"Yehuda Gal","year":"2020","unstructured":"Gal Yehuda , Moshe Gabel , and Assaf Schuster . 2020 . It's not what machines can learn, it's what we cannot teach . In International conference on machine learning. PMLR, 10831--10841 . Gal Yehuda, Moshe Gabel, and Assaf Schuster. 2020. It's not what machines can learn, it's what we cannot teach. In International conference on machine learning. PMLR, 10831--10841."},{"key":"e_1_3_2_2_49_1","volume-title":"G2SAT: Learning to generate sat formulas. Advances in neural information processing systems","author":"You Jiaxuan","year":"2019","unstructured":"Jiaxuan You , Haoze Wu , Clark Barrett , Raghuram Ramanujan , and Jure Leskovec . 2019. G2SAT: Learning to generate sat formulas. Advances in neural information processing systems , Vol. 32 ( 2019 ). Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovec. 2019. G2SAT: Learning to generate sat formulas. Advances in neural information processing systems, Vol. 32 (2019)."},{"key":"e_1_3_2_2_50_1","volume-title":"NLocalSAT: Boosting Local Search with Solution Prediction. In International Joint Conference on Artificial Intelligence. 1177--1183","author":"Zhang Wenjie","year":"2020","unstructured":"Wenjie Zhang , Zeyu Sun , Qihao Zhu , Ge Li , Shaowei Cai , Yingfei Xiong , and Lu Zhang . 2020 . NLocalSAT: Boosting Local Search with Solution Prediction. In International Joint Conference on Artificial Intelligence. 1177--1183 . Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, and Lu Zhang. 2020. NLocalSAT: Boosting Local Search with Solution Prediction. In International Joint Conference on Artificial Intelligence. 1177--1183."}],"event":{"name":"KDD '23: The 29th ACM SIGKDD Conference on Knowledge Discovery and Data Mining","sponsor":["SIGMOD ACM Special Interest Group on Management of Data","SIGKDD ACM Special Interest Group on Knowledge Discovery in Data"],"location":"Long Beach CA USA","acronym":"KDD '23"},"container-title":["Proceedings of the 29th ACM SIGKDD Conference on Knowledge Discovery and Data Mining"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3580305.3599837","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3580305.3599837","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:23Z","timestamp":1750182563000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3580305.3599837"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,4]]},"references-count":50,"alternative-id":["10.1145\/3580305.3599837","10.1145\/3580305"],"URL":"https:\/\/doi.org\/10.1145\/3580305.3599837","relation":{},"subject":[],"published":{"date-parts":[[2023,8,4]]},"assertion":[{"value":"2023-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}