{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:03:27Z","timestamp":1776373407240,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,14]],"date-time":"2024-04-14T00:00:00Z","timestamp":1713052800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Luxembourg National Research Fund (FNR)","award":["C19\/IS\/13566661\/BEEHIVE\/Cordy"],"award-info":[{"award-number":["C19\/IS\/13566661\/BEEHIVE\/Cordy"]}]},{"name":"Luxembourg National Research Fund (FNR)","award":["AFR Grant 17047437"],"award-info":[{"award-number":["AFR Grant 17047437"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,14]]},"DOI":"10.1145\/3644033.3644371","type":"proceedings-article","created":{"date-parts":[[2024,6,6]],"date-time":"2024-06-06T16:56:27Z","timestamp":1717692987000},"page":"23-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Preprocessing is What You Need: Understanding and Predicting the Complexity of SAT-based Uniform Random Sampling"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0378-5643","authenticated-orcid":false,"given":"Olivier","family":"Zeyen","sequence":"first","affiliation":[{"name":"University of Luxembourg, SnT, Luxembourg, Luxembourg"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8312-1358","authenticated-orcid":false,"given":"Maxime","family":"Cordy","sequence":"additional","affiliation":[{"name":"SnT, University of Luxembourg, Luxembourg, Luxembourg"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8431-0377","authenticated-orcid":false,"given":"Gilles","family":"Perrouin","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Namur, Namur, Belgium"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1483-3858","authenticated-orcid":false,"given":"Mathieu","family":"Acher","sequence":"additional","affiliation":[{"name":"Univ Rennes, Inria, CNRS, IRISA, Rennes, France"}]}],"member":"320","published-online":{"date-parts":[[2024,6,6]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3461002.3473070"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"D. Achlioptas Zayd Hammoudeh and P. Theodoropoulos. 2018. Fast Sampling of Perfectly Uniform Satisfying Assignments. In SAT.","DOI":"10.1007\/978-3-319-94144-8_9"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3491210"},{"key":"e_1_3_2_1_4_1","unstructured":"Anonym. 2023. EQV and preprocessing for URS prediction. https:\/\/github.com\/serval-uni-lu\/urs_scal."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00039"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"D. Batory D. Benavides and A. Ruiz-Cort\u00e9s. 2006. Automated Analysis of Feature Models: Challenges Ahead. Commun. ACM (December 2006).","DOI":"10.1145\/1183236.1183264"},{"key":"e_1_3_2_1_7_1","volume-title":"On Parallel Scalable Uniform SAT Witness Generation. In Tools and Algorithms for the Construction and Analysis of Systems TACAS'15 2015, London, UK, April 11--18, 2015. Proceedings. 304--319","author":"Chakraborty Supratik","unstructured":"Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. 2015. On Parallel Scalable Uniform SAT Witness Generation. In Tools and Algorithms for the Construction and Analysis of Systems TACAS'15 2015, London, UK, April 11--18, 2015. Proceedings. 304--319."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593097"},{"key":"e_1_3_2_1_9_1","volume-title":"Backbones for Equality. In Haifa Verification Conference.","author":"Codish Michael","year":"2013","unstructured":"Michael Codish, Yoav Fekete, and Amit Metodi. 2013. Backbones for Equality. In Haifa Verification Conference."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45234-6_15"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2739480.2754760"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180248"},{"key":"e_1_3_2_1_14_1","volume-title":"An Extensible SAT-solver. In SAT'03","author":"E\u00e9n Niklas","year":"2003","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson. 2003. An Extensible SAT-solver. In SAT'03. Springer, 502--518."},{"key":"e_1_3_2_1_15_1","volume-title":"Vardi","author":"Ganesh Vijay","year":"2021","unstructured":"Vijay Ganesh and Moshe Y. Vardi. 2021. On The Unreasonable Effectiveness of SAT Solvers. In Beyond the worst-case analysis of algorithms, Tim Roughgarden (Ed.). Cambridge University Press, 547--563."},{"key":"e_1_3_2_1_16_1","volume-title":"Meel","author":"Golia Priyanka","year":"2021","unstructured":"Priyanka Golia, M. Soos, Sourav Chakraborty, and Kuldeep S. Meel. 2021. Designing Samplers is Easy: The Boon of Testers. 2021 Formal Methods in Computer Aided Design (FMCAD) (2021), 222--230."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-018-9635-4"},{"key":"e_1_3_2_1_18_1","first-page":"1","article-title":"Graph Bisection with Pareto Optimization","volume":"23","author":"Hamann Michael","year":"2015","unstructured":"Michael Hamann and Ben Strasser. 2015. Graph Bisection with Pareto Optimization. Journal of Experimental Algorithmics (JEA) 23 (2015), 1 -- 34. https:\/\/api.semanticscholar.org\/CorpusID:3395784","journal-title":"Journal of Experimental Algorithmics (JEA)"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-015-9204-z"},{"key":"e_1_3_2_1_20_1","volume-title":"Model Driven Engineering Languages and Systems: 14th International Conference, MODELS '11, Jon Whittle, Tony Clark, and Thomas K\u00fchne (Eds.)","author":"Johansen Martin Fagereng","unstructured":"Martin Fagereng Johansen, \u00d8ystein Haugen, and Franck Fleurey. 2011. Properties of Realistic Feature Models Make Combinatorial Testing of Product Lines Feasible. In Model Driven Engineering Languages and Systems: 14th International Conference, MODELS '11, Jon Whittle, Tony Clark, and Thomas K\u00fchne (Eds.). Springer, 638--652."},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, May 25--31","author":"Kaltenecker Christian","year":"2019","unstructured":"Christian Kaltenecker, Alexander Grebhahn, Norbert Siegmund, Jianmei Guo, and Sven Apel. 2019. Distance-based sampling of software configuration spaces. In Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, May 25--31, 2019, Joanne M. Atlee, Tevfik Bultan, and Jon Whittle (Eds.). IEEE \/ ACM, 1084--1094."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"K. Kang S. Cohen J. Hess W. Novak and S. Peterson. 1990. Feature-Oriented Domain Analysis (FODA). Technical Report CMU\/SEI-90-TR-21. SEI.","DOI":"10.21236\/ADA235785"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106252"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180159"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Jean-Marie Lagniez and Pierre Marquis. 2017. An Improved Decision-DNNF Compiler. In IJCAI.","DOI":"10.24963\/ijcai.2017\/93"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2791060.2791070"},{"key":"e_1_3_2_1_27_1","unstructured":"R. Mateescu. 2011. Treewidth in Industrial SAT Benchmarks."},{"key":"e_1_3_2_1_28_1","volume-title":"SPLC'09","author":"Mendonca Marcilio","year":"2009","unstructured":"Marcilio Mendonca, Andrzej Wasowski, and Krzysztof Czarnecki. 2009. SAT-based analysis of feature models is easy. In SPLC'09 (San Francisco, California). IEEE, 231--240."},{"key":"e_1_3_2_1_29_1","volume-title":"Determining computational complexity from characteristic `phase transitions'. Nature 400, 6740","author":"Monasson R\u00e9mi","year":"1999","unstructured":"R\u00e9mi Monasson, Riccardo Zecchina, Scott Kirkpatrick, Bart Selman, and Lidror Troyansky. 1999. Determining computational complexity from characteristic `phase transitions'. Nature 400, 6740 (1999), 133--137."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106273"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the 23rd International Systems and Software Product Line Conference, SPLC 2019","volume":"13","author":"Oh Jeho","year":"2019","unstructured":"Jeho Oh, Paul Gazzillo, and Don S. Batory. 2019. t-wise coverage by uniform sampling. In Proceedings of the 23rd International Systems and Software Product Line Conference, SPLC 2019, Volume A, Paris, France, September 9--13, 2019, Thorsten Berger, Philippe Collet, Laurence Duchien, Thomas Fogdal, Patrick Heymans, Timo Kehrer, Jabier Martinez, Ra\u00fal Mazo, Leticia Montalvillo, Camille Salinesi, Xhevahire T\u00e9rnava, Thomas Th\u00fcm, and Tewfik Ziadi (Eds.). ACM, 15:1--15:4."},{"key":"e_1_3_2_1_32_1","volume-title":"FASE 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. 127--140","author":"Oudinet Johan","year":"2011","unstructured":"Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Richard Lassaigne, and Sylvain Peyronnet. 2011. Uniform Monte-Carlo Model Checking. In Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. 127--140."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Umut Oztok and Adnan Darwiche. 2014. On Compiling CNF into Decision-DNNF. In CP.","DOI":"10.1007\/978-3-319-10428-7_7"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1016\/j.ipl.2018.11.005","article-title":"On the parameterized complexity of (k, s)-SAT","volume":"143","author":"Paulusma Dani\u00e9l","year":"2019","unstructured":"Dani\u00e9l Paulusma and Stefan Szeider. 2019. On the parameterized complexity of (k, s)-SAT. Inf. Process. Lett. 143 (2019), 34--36.","journal-title":"Inf. Process. Lett."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1953048.2078195"},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the 23rd International Systems and Software Product Line Conference -","volume":"85462202","author":"Pett Tobias","year":"2019","unstructured":"Tobias Pett, Thomas Th\u00fcm, Tobias Runge, Sebastian Krieter, Malte Lochau, and Ina Schaefer. 2019. Product Sampling for Product Lines: The Scalability Challenge. Proceedings of the 23rd International Systems and Software Product Line Conference - Volume A (2019). https:\/\/api.semanticscholar.org\/CorpusID:85462202"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2019.00032"},{"key":"e_1_3_2_1_38_1","unstructured":"Matt Raible. 2015. The JHipster mini-book. C4Media."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2006.23"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR).","author":"Sharma Shubham","unstructured":"Shubham Sharma, Rahul Gupta, Subhajit Roy, and Kuldeep S. Meel. 2018. Knowledge Compilation meets Uniform Sampling. In Proceedings of International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)."},{"key":"e_1_3_2_1_41_1","volume-title":"Proceedings of International Conference on Computer-Aided Verification (CAV).","author":"Soos Mate","unstructured":"Mate Soos, Stephan Gocht, and Kuldeep S. Meel. 2020. Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling. In Proceedings of International Conference on Computer-Aided Verification (CAV)."},{"key":"e_1_3_2_1_42_1","volume-title":"Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling. arXiv preprint arXiv:2110.09026","author":"Soos Mate","year":"2021","unstructured":"Mate Soos and Kuldeep S Meel. 2021. Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling. arXiv preprint arXiv:2110.09026 (2021)."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_38"}],"event":{"name":"FormaliSE '24: 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)","location":"Lisbon Portugal","acronym":"FormaliSE '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644033.3644371","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3644033.3644371","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:56:58Z","timestamp":1750291018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3644033.3644371"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,14]]},"references-count":43,"alternative-id":["10.1145\/3644033.3644371","10.1145\/3644033"],"URL":"https:\/\/doi.org\/10.1145\/3644033.3644371","relation":{},"subject":[],"published":{"date-parts":[[2024,4,14]]},"assertion":[{"value":"2024-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}