{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:22:52Z","timestamp":1742973772844,"version":"3.40.3"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_11","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"152-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["ProCount: Weighted Projected Model Counting with Graded Project-Join Trees"],"prefix":"10.1007","author":[{"given":"Jeffrey M.","family":"Dudek","sequence":"first","affiliation":[]},{"given":"Vu H. N.","family":"Phan","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Abo Khamis, M., Ngo, H.Q., Rudra, A.: FAQ: questions asked frequently. In: PODS, pp. 13\u201328 (2016)","DOI":"10.1145\/2902251.2902280"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Abseher, M., Musliu, N., Woltran, S.: htd-a free, open-source framework for (customized) tree decompositions and beyond. In: CPAIOR, pp. 376\u2013386 (2017). https:\/\/doi.org\/10.1007\/978-3-319-59776-8_30","DOI":"10.1007\/978-3-319-59776-8_30"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Aguirre, A.S.M., Vardi, M.: Random 3-SAT and BDDs: the plot thickens further. In: CP, pp. 121\u2013136 (2001). https:\/\/doi.org\/10.1007\/3-540-45578-7_9","DOI":"10.1007\/3-540-45578-7_9"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Aziz, R.A., Chu, G., Muise, C., Stuckey, P.: Projected model counting. In: SAT, pp. 121\u2013137 (2015)","DOI":"10.1007\/978-3-319-24318-4_10"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1613\/jair.2648","volume":"34","author":"F Bacchus","year":"2009","unstructured":"Bacchus, F., Dalmao, S., Pitassi, T.: Solving #SAT and Bayesian inference with backtracking search. JAIR 34, 391\u2013442 (2009). https:\/\/doi.org\/10.1613\/jair.2648","journal-title":"JAIR"},{"issue":"2\u20133","key":"11_CR6","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"RI Bahar","year":"1997","unstructured":"Bahar, R.I., et al.: Algebraic decision diagrams and their applications. Form. Method Syst. Des. 10(2\u20133), 171\u2013206 (1997). https:\/\/doi.org\/10.1023\/A:1008699807402","journal-title":"Form. Method Syst. Des."},{"issue":"3731","key":"11_CR7","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1126\/science.153.3731.34","volume":"153","author":"R Bellman","year":"1966","unstructured":"Bellman, R.: Dynamic programming. Science 153(3731), 34\u201337 (1966). https:\/\/doi.org\/10.1126\/science.153.3731.34","journal-title":"Science"},{"key":"11_CR8","unstructured":"Bouquet, F.: Gestion de la dynamicit\u00e9 et \u00e9num\u00e9ration d\u2019impliquants premiers: une approche fond\u00e9e sur les Diagrammes de D\u00e9cision Binaire. Ph.D. thesis, Aix-Marseille 1 (1999). https:\/\/www.theses.fr\/1999AIX11011"},{"issue":"8","key":"11_CR9","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"100","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE TC 100(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","journal-title":"IEEE TC"},{"key":"11_CR10","unstructured":"Charwat, G., Woltran, S.: BDD-based dynamic programming on tree decompositions. Technical report, Technische Universit\u00e4t Wien, Institut f\u00fcr Informationssysteme (2016). https:\/\/dbai.tuwien.ac.at\/research\/report\/dbai-tr-2016-95.pdf"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Dalmau, V., Kolaitis, P.G., Vardi, M.Y.: Constraint satisfaction, bounded treewidth, and finite-variable logics. In: CP, pp. 310\u2013326 (2002). https:\/\/doi.org\/10.1007\/3-540-46135-3_21","DOI":"10.1007\/3-540-46135-3_21"},{"key":"11_CR12","unstructured":"Darwiche, A.: New advances in compiling CNF to decomposable negation normal form. In: ECAI, pp. 318\u2013322 (2004). https:\/\/dl.acm.org\/doi\/10.5555\/3000001.3000069"},{"issue":"1\u20132","key":"11_CR13","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0004-3702(99)00059-4","volume":"113","author":"R Dechter","year":"1999","unstructured":"Dechter, R.: Bucket elimination: a unifying framework for reasoning. AIJ 113(1\u20132), 41\u201385 (1999). https:\/\/doi.org\/10.1016\/S0004-3702(99)00059-4","journal-title":"AIJ"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Dechter, R.: Constraint Processing. Morgan Kaufmann (2003). https:\/\/doi.org\/10.1016\/B978-1-55860-890-0.X5000-2","DOI":"10.1016\/B978-1-55860-890-0.X5000-2"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: TACAS, pp. 677\u2013691 (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_60","DOI":"10.1007\/978-3-662-46681-0_60"},{"key":"11_CR16","unstructured":"Dudek, J.M., Due\u00f1as-Osorio, L., Vardi, M.Y.: Efficient contraction of large tensor networks for weighted model counting through graph decompositions (2019). arXiv preprint arXiv:1908.04381"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Dudek, J.M., Phan, V.H.N., Vardi, M.Y.: DPMC: weighted model counting by dynamic programming on project-join trees. In: CP, pp. 211\u2013230 (2020). arxiv.org\/abs\/2008.08748","DOI":"10.1007\/978-3-030-58475-7_13"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"1468","DOI":"10.1609\/aaai.v34i02.5505","volume":"34","author":"JM Dudek","year":"2020","unstructured":"Dudek, J.M., Phan, V.H., Vardi, M.Y.: ADDMC: weighted model counting with algebraic decision diagrams. AAAI 34, 1468\u20131476 (2020). https:\/\/doi.org\/10.1609\/aaai.v34i02.5505","journal-title":"AAAI"},{"key":"11_CR19","unstructured":"Dudek, J.M., Vardi, M.Y.: Parallel weighted model counting with tensor networks. In: MCW (2020). https:\/\/mccompetition.org\/assets\/files\/2020\/MCW_2020_paper_1.pdf"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Duenas-Osorio, L., Meel, K.S., Paredes, R., Vardi, M.Y.: Counting-based reliability estimation for power-transmission grids. In: AAAI. pp. 4488\u20134494 (2017)","DOI":"10.1609\/aaai.v31i1.11178"},{"key":"11_CR21","unstructured":"Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Taming the curse of dimensionality: discrete integration by hashing and optimization. In: ICML, pp. 334\u2013342 (2013)"},{"key":"11_CR22","unstructured":"Fichte, J.K., Hecher, M.: Counting with bounded treewidth: meta algorithm and runtime guarantees. In: NMR, pp. 9\u201318 (2020)"},{"key":"11_CR23","unstructured":"Fichte, J.K., Hecher, M., Hamiti, F.: The Model Counting Competition 2020 (2020). arXiv preprint arXiv:2012.01323"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Fichte, J.K., Hecher, M., Morak, M., Woltran, S.: Exploiting treewidth for projected model counting and its limits. In: SAT, pp. 165\u2013184 (2018)","DOI":"10.1007\/978-3-319-94144-8_11"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Fichte, J.K., Hecher, M., Thier, P., Woltran, S.: Exploiting database management systems and treewidth for counting. In: PADL, pp. 151\u2013167 (2020). https:\/\/doi.org\/10.1007\/978-3-030-39197-3_10","DOI":"10.1007\/978-3-030-39197-3_10"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Rabe, M.N., Seshia, S.A.: Maximum model counting. In: AAAI, pp. 3885\u20133892 (2017)","DOI":"10.1609\/aaai.v31i1.11138"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Gupta, R., Sharma, S., Roy, S., Meel, K.S.: WAPS: weighted and projected sampling. In: TACAS, pp. 59\u201376 (2019)","DOI":"10.1007\/978-3-030-17462-0_4"},{"key":"11_CR28","first-page":"1","volume":"23","author":"M Hamann","year":"2018","unstructured":"Hamann, M., Strasser, B.: Graph bisection with pareto optimization. JEA 23, 1\u201334 (2018)","journal-title":"JEA"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Hecher, M., Thier, P., Woltran, S.: Taming high treewidth with abstraction, nested dynamic programming, and database technology. In: SAT, pp. 343\u2013360 (2020)","DOI":"10.1007\/978-3-030-51825-7_25"},{"issue":"4","key":"11_CR30","first-page":"512","volume":"63","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo, R., Paturi, R., Zane, F.: Which problems have strongly exponential complexity? JCSS 63(4), 512\u2013530 (2001)","journal-title":"JCSS"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"J\u00e9gou, P., Kanso, H., Terrioux, C.: Improving exact solution counting for decomposition methods. In: ICTAI, pp. 327\u2013334 (2016). https:\/\/doi.org\/10.1109\/ICTAI.2016.0057","DOI":"10.1109\/ICTAI.2016.0057"},{"key":"11_CR32","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(86)90174-X","volume":"43","author":"MR Jerrum","year":"1986","unstructured":"Jerrum, M.R., Valiant, L.G., Vazirani, V.V.: Random generation of combinatorial structures from a uniform distribution. Theor. Comput. Sci. 43, 169\u2013188 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR33","unstructured":"Kelly, C., Sarkhel, S., Venugopal, D.: Adaptive Rao-Blackwellisation in Gibbs sampling for probabilistic graphical models. In: AISTATS, pp. 2907\u20132915 (2019)"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: QEST, pp. 177\u2013192 (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_16","DOI":"10.1007\/978-3-642-40196-1_16"},{"key":"11_CR35","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/S1571-0653(05)80078-2","volume":"8","author":"AM Koster","year":"2001","unstructured":"Koster, A.M., Bodlaender, H.L., Van Hoesel, S.P.: Treewidth: computational experiments. Electron. Notes Disc. Math. 8, 54\u201357 (2001). https:\/\/doi.org\/10.1016\/S1571-0653(05)80078-2","journal-title":"Electron. Notes Disc. Math."},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Lagniez, J.M., Marquis, P.: An improved decision-DNNF compiler. In: IJCAI, pp. 667\u2013673 (2017). https:\/\/doi.org\/10.24963\/ijcai.2017\/93","DOI":"10.24963\/ijcai.2017\/93"},{"key":"11_CR37","doi-asserted-by":"publisher","first-page":"1536","DOI":"10.1609\/aaai.v33i01.33011536","volume":"33","author":"JM Lagniez","year":"2019","unstructured":"Lagniez, J.M., Marquis, P.: A recursive algorithm for projected model counting. AAAI 33, 1536\u20131543 (2019)","journal-title":"AAAI"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"Lee, N.Z., Wang, Y.S., Jiang, J.H.R.: Solving stochastic Boolean satisfiability under random-exist quantification. In: IJCAI, pp. 688\u2013694 (2017)","DOI":"10.24963\/ijcai.2017\/96"},{"key":"11_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-96826-6","volume-title":"Foundations of Logic Programming","author":"JW Lloyd","year":"2012","unstructured":"Lloyd, J.W.: Foundations of Logic Programming. Springer, Cham (2012). https:\/\/doi.org\/10.1007\/978-3-642-96826-6"},{"key":"11_CR40","unstructured":"Maua, D.D., de Campos, C.P., Cozman, F.G.: The complexity of MAP inference in Bayesian networks specified through logical languages. In: IJCAI, pp. 889\u2013895 (2015)"},{"key":"11_CR41","doi-asserted-by":"publisher","unstructured":"McMahan, B.J., Pan, G., Porter, P., Vardi, M.Y.: Projection pushing revisited. In: EDBT, pp. 441\u2013458 (2004). https:\/\/doi.org\/10.1007\/978-3-540-24741-8_26","DOI":"10.1007\/978-3-540-24741-8_26"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"M\u00f6hle, S., Biere, A.: Dualizing projected model counting. In: ICTAI, pp. 702\u2013709 (2018)","DOI":"10.1109\/ICTAI.2018.00111"},{"key":"11_CR43","volume-title":"Machine Learning: A Probabilistic Perspective","author":"KP Murphy","year":"2012","unstructured":"Murphy, K.P.: Machine Learning: A Probabilistic Perspective. MIT press, Cambridge (2012)"},{"key":"11_CR44","unstructured":"Oztok, U., Darwiche, A.: A top-down compiler for sentential decision diagrams. In: IJCAI, pp. 3141\u20133148 (2015). https:\/\/dl.acm.org\/doi\/10.5555\/2832581.2832687"},{"issue":"1\u20133","key":"11_CR45","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10817-005-9009-7","volume":"35","author":"G Pan","year":"2005","unstructured":"Pan, G., Vardi, M.Y.: Symbolic techniques in satisfiability solving. J. Autom. Reas. 35(1\u20133), 25\u201350 (2005). https:\/\/doi.org\/10.1007\/s10817-005-9009-7","journal-title":"J. Autom. Reas."},{"key":"11_CR46","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1613\/jair.1236","volume":"21","author":"JD Park","year":"2004","unstructured":"Park, J.D., Darwiche, A.: Complexity results and approximation strategies for MAP explanations. JAIR 21, 101\u2013133 (2004)","journal-title":"JAIR"},{"key":"11_CR47","unstructured":"Pearl, J.: Bayesian networks: a model cf self-activated memory for evidential reasoning. In: Proceedings of the 7th Conference of the Cognitive Science Society, University of California, Irvine, CA, USA, pp. 15\u201317 (1985)"},{"key":"11_CR48","doi-asserted-by":"publisher","unstructured":"Robertson, N., Seymour, P.D.: Graph minors. X. Obstructions to tree-decomposition. J. Comb. Theory B 52(2), 153\u2013190 (1991). https:\/\/doi.org\/10.1016\/0095-8956(91)90061-N","DOI":"10.1016\/0095-8956(91)90061-N"},{"issue":"1","key":"11_CR49","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-75560-9_35","volume":"8","author":"M Samer","year":"2010","unstructured":"Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Disc. Algor. 8(1), 50\u201364 (2010). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_35","journal-title":"J. Disc. Algor."},{"key":"11_CR50","unstructured":"Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. SAT 4, 20\u201328 (2004). http:\/\/www.satisfiability.org\/SAT04\/accepted\/65.html"},{"key":"11_CR51","doi-asserted-by":"crossref","unstructured":"Sharma, S., Roy, S., Soos, M., Meel, K.S.: GANAK: a scalable probabilistic exact model counter. In: IJCAI, pp. 1169\u20131176 (2019)","DOI":"10.24963\/ijcai.2019\/163"},{"key":"11_CR52","doi-asserted-by":"publisher","first-page":"1592","DOI":"10.1609\/aaai.v33i01.33011592","volume":"33","author":"M Soos","year":"2019","unstructured":"Soos, M., Meel, K.S.: BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. AAAI 33, 1592\u20131599 (2019)","journal-title":"AAAI"},{"key":"11_CR53","doi-asserted-by":"crossref","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: SAT, pp. 244\u2013257 (2009)","DOI":"10.1007\/978-3-642-02777-2_24"},{"issue":"2","key":"11_CR54","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/S0196-6774(02)00002-0","volume":"43","author":"RE Stearns","year":"2002","unstructured":"Stearns, R.E., Hunt, H.B., III.: Exploiting structure in quantified formulas. J. Algor. 43(2), 220\u2013263 (2002)","journal-title":"J. Algor."},{"issue":"2","key":"11_CR55","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1145\/16856.16888","volume":"15","author":"M Stonebraker","year":"1986","unstructured":"Stonebraker, M., Rowe, L.A.: The design of Postgres. ACM Sigmod Rec. 15(2), 340\u2013355 (1986)","journal-title":"ACM Sigmod Rec."},{"key":"11_CR56","doi-asserted-by":"crossref","unstructured":"Tabajara, L.M., Vardi, M.Y.: Factored Boolean functional synthesis. In: FMCAD, pp. 124\u2013131 (2017). https:\/\/dl.acm.org\/doi\/10.5555\/3168451.3168480","DOI":"10.23919\/FMCAD.2017.8102250"},{"issue":"4","key":"11_CR57","doi-asserted-by":"publisher","first-page":"1283","DOI":"10.1007\/s10878-018-0353-z","volume":"37","author":"H Tamaki","year":"2019","unstructured":"Tamaki, H.: Positive-instance-driven dynamic programming for treewidth. J. Comb. Optim. 37(4), 1283\u20131311 (2019). https:\/\/doi.org\/10.1007\/s10878-018-0353-z","journal-title":"J. Comb. Optim."},{"issue":"3","key":"11_CR58","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1137\/0213035","volume":"13","author":"RE Tarjan","year":"1984","unstructured":"Tarjan, R.E., Yannakakis, M.: Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SICOMP 13(3), 566\u2013579 (1984). https:\/\/doi.org\/10.1137\/0213035","journal-title":"SICOMP"},{"key":"11_CR59","doi-asserted-by":"publisher","unstructured":"Uribe, T.E., Stickel, M.E.: Ordered binary decision diagrams and the Davis-Putnam procedure. In: CCL, pp. 34\u201349 (1994). https:\/\/doi.org\/10.1007\/BFb0016843","DOI":"10.1007\/BFb0016843"},{"key":"11_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"key":"11_CR61","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. JAIR 32, 565\u2013606 (2008)","journal-title":"JAIR"},{"key":"11_CR62","unstructured":"Xue, Y., Li, Z., Ermon, S., Gomes, C.P., Selman, B.: Solving marginal MAP problems with NP oracles and parity constraints. In: NIPS, pp. 1127\u20131135 (2016)"},{"key":"11_CR63","doi-asserted-by":"crossref","unstructured":"Zawadzki, E.P., Platzer, A., Gordon, G.J.: A generalization of SAT and #SAT for robust policy evaluation. In: IJCAI, pp. 2583\u20132589 (2013)","DOI":"10.21236\/ADA606746"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T09:41:05Z","timestamp":1672652465000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}