{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T09:03:51Z","timestamp":1774602231957,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466803","type":"print"},{"value":"9783662466810","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_25","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T22:56:36Z","timestamp":1427756196000},"page":"304-319","source":"Crossref","is-referenced-by-count":53,"title":["On Parallel Scalable Uniform SAT Witness Generation"],"prefix":"10.1007","author":[{"given":"Supratik","family":"Chakraborty","sequence":"first","affiliation":[]},{"given":"Daniel J.","family":"Fremont","sequence":"additional","affiliation":[]},{"given":"Kuldeep S.","family":"Meel","sequence":"additional","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"CryptoMiniSAT, http:\/\/www.msoos.org\/cryptominisat2\/"},{"issue":"2","key":"25_CR2","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1006\/inco.2000.2885","volume":"163","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Goldreich, O., Petrank, E.: Uniform generation of NP-witnesses using an NP-oracle. Information and Computation\u00a0163(2), 510\u2013526 (2000)","journal-title":"Information and Computation"},{"key":"25_CR3","unstructured":"Bening, L., Foster, H.: Principles of verifiable RTL design \u2013 A functional coding style supporting verification processes. Springer (2001)"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/978-3-642-39799-8_40","volume-title":"Computer Aided Verification","author":"S. Chakraborty","year":"2013","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable and nearly uniform generator of SAT witnesses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 608\u2013623. Springer, Heidelberg (2013)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-40627-0_18","volume-title":"Principles and Practice of Constraint Programming","author":"S. Chakraborty","year":"2013","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Schulte, C. (ed.) CP 2013. LNCS, vol.\u00a08124, pp. 200\u2013216. Springer, Heidelberg (2013)"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Balancing scalability and uniformity in SAT-witness generator. In: Proc. of DAC, pp. 1\u20136 (2014)","DOI":"10.1145\/2593069.2593097"},{"key":"25_CR7","unstructured":"Dechter, R., Kask, K., Bin, E., Emek, R.: Generating random solutions for constraint satisfaction problems. In: AAAI, pp. 15\u201321 (2002)"},{"issue":"3","key":"25_CR8","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1109\/12.21127","volume":"38","author":"D.L. Eager","year":"1989","unstructured":"Eager, D.L., Zahorjan, J., Lazowska, E.D.: Speedup versus efficiency in parallel systems. IEEE Trans. on Computers\u00a038(3), 408\u2013423 (1989)","journal-title":"IEEE Trans. on Computers"},{"key":"25_CR9","unstructured":"Ermon, S., Gomes, C.P., Sabharwal, A., Selman, B.: Embed and project: Discrete sampling with universal hashing. In: Proc. of NIPS (2013)"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Esmaeilzadeh, H., Blem, E., Amant, R.S., Sankaralingam, K., Burger, D.: Dark silicon and the end of multicore scaling. In: Proc. of ISCA, pp. 365\u2013376 (2011)","DOI":"10.1145\/2024723.2000108"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/11889205_56","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"V. Gogate","year":"2006","unstructured":"Gogate, V., Dechter, R.: A new algorithm for sampling CSP solutions uniformly at random. In: Benhamou, F. (ed.) CP 2006. LNCS, vol.\u00a04204, pp. 711\u2013715. Springer, Heidelberg (2006)"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Near uniform sampling of combinatorial spaces using XOR constraints. In: Proc. of NIPS, pp. 670\u2013676 (2007)","DOI":"10.7551\/mitpress\/7503.003.0065"},{"issue":"4","key":"25_CR13","doi-asserted-by":"publisher","first-page":"41905","DOI":"10.1103\/PhysRevE.65.041905","volume":"65","author":"I. Grosse","year":"2002","unstructured":"Grosse, I., Bernaola-Galv\u00e1n, P., Carpena, P., Rom\u00e1n-Rold\u00e1n, R., Oliver, J., Stanley, E.: Analysis of symbolic sequences using the Jensen-Shannon divergence. Physical Review E\u00a065(4), 41905 (2002)","journal-title":"Physical Review E"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Iyer, M.A.: Race: A word-level ATPG-based constraints solver system for smart random simulation. In: Proc. of ITC, pp. 299\u2013308. Citeseer (2003)","DOI":"10.1109\/TEST.2003.1270852"},{"issue":"2-3","key":"25_CR15","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(86)90174-X","volume":"43","author":"M.R. Jerrum","year":"1986","unstructured":"Jerrum, M.R., Valiant, L.G., Vazirani, V.V.: Random generation of combinatorial structures from a uniform distribution. TCS\u00a043(2-3), 169\u2013188 (1986)","journal-title":"TCS"},{"key":"25_CR16","unstructured":"Kitchen, N.: Markov Chain Monte Carlo Stimulus Generation for Constrained Random Simulation. PhD thesis, University of California, Berkeley (2010)"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Kitchen, N., Kuehlmann, A.: Stimulus generation for constrained random simulation. In: Proc. of ICCAD, pp. 258\u2013265 (2007)","DOI":"10.1109\/ICCAD.2007.4397275"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Madras, N.: Lectures on Monte Carlo Methods. Fields Institute Monographs, vol.\u00a016. AMS (2002)","DOI":"10.1090\/fim\/016"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. of DAC, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-21581-0_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"A. Nadel","year":"2011","unstructured":"Nadel, A.: Generating diverse solutions in SAT. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 287\u2013301. Springer, Heidelberg (2011)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"823","DOI":"10.1007\/978-3-642-40627-0_60","volume-title":"Principles and Practice of Constraint Programming","author":"R. Naveh","year":"2013","unstructured":"Naveh, R., Metodi, A.: Beyond feasibility: CP usage in constrained-random functional hardware verification. In: Schulte, C. (ed.) CP 2013. LNCS, vol.\u00a08124, pp. 823\u2013831. Springer, Heidelberg (2013)"},{"key":"25_CR22","unstructured":"Naveh, Y., Rimon, M., Jaeger, I., Katz, Y., Vinov, M., Marcus, E., Shurek, G.: Constraint-based random stimuli generation for hardware verification. In: Proc. of AAAI, pp. 1720\u20131727 (2006)"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Sipser, M.: A complexity theoretic approach to randomness. In: Proc. of STOC, pp. 330\u2013335 (1983)","DOI":"10.1145\/800061.808762"},{"issue":"3","key":"25_CR24","first-page":"412","volume":"23","author":"J. Yuan","year":"2004","unstructured":"Yuan, J., Aziz, A., Pixley, C., Albin, K.: Simplifying Boolean constraint solving for random simulation vector generation. TCAD\u00a023(3), 412\u2013420 (2004)","journal-title":"TCAD"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:26:03Z","timestamp":1747855563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}