{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,23]],"date-time":"2026-01-23T07:45:34Z","timestamp":1769154334066,"version":"3.49.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661667","type":"print"},{"value":"9783319661674","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66167-4_9","type":"book-chapter","created":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T07:15:18Z","timestamp":1503904518000},"page":"153-171","source":"Crossref","is-referenced-by-count":24,"title":["Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a Preliminary Report"],"prefix":"10.1007","author":[{"given":"Zhengbing","family":"Bian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabian","family":"Chudak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William","family":"Macready","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aidan","family":"Roy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Varotti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"9_CR1","unstructured":"Experimental data, source code, and supplementary material. https:\/\/bitbucket.org\/aqcsat\/frocos2017"},{"key":"9_CR2","doi-asserted-by":"crossref","first-page":"7018","DOI":"10.1016\/j.tcs.2011.09.015","volume":"412","author":"I Adler","year":"2011","unstructured":"Adler, I., Dorn, F., Fomin, F.V., Sau, I., Thilikos, D.M.: Faster parameterized algorithms for minor containment. Theor. Comput. Sci. 412, 7018\u20137028 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR3","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Handbook of Satisfiability (2009)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Betz, V., Rose, J.: Vpr: a new packing, placement and routing tool for FPGA research. In: Field Programmable Logic Workshop (1997)","DOI":"10.1007\/3-540-63465-7_226"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bian, Z., Chudak, F., Israel, R., Lackey, B., Macready, W.G., Roy A.: Discrete optimization using quantum annealing on sparse Ising models. Frontiers in Physics (2014)","DOI":"10.3389\/fphy.2014.00056"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Bian, Z., Chudak, F., Israel, R.B., Lackey, B., Macready, W.G., Roy, A.: Mapping constrained optimization problems to quantum annealing with application to fault diagnosis. In: Frontiers in ICT (2016)","DOI":"10.3389\/fict.2016.00014"},{"key":"9_CR7","unstructured":"Bian, Z., Chudak, F., Macready, W., Roy, A., Sebastiani, R., Varotti, S.: Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a Preliminary Report (2017). Extended version. https:\/\/bitbucket.org\/aqcsat\/frocos2017\/raw\/HEAD\/sat2ising_extended.pdf"},{"key":"9_CR8","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/s11128-015-1150-6","volume":"15","author":"T Boothby","year":"2016","unstructured":"Boothby, T., King, A.D., Roy, A.: Fast clique minor generation in chimera qubit connectivity graphs. Quant. Inf. Proc. 15, 495\u2013508 (2016)","journal-title":"Quant. Inf. Proc."},{"key":"9_CR9","unstructured":"Cai, J., Macready, W.G., Roy, A.: A practical heuristic for finding graph minors. arXiv preprint (2014)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Chan, T., Cong, J., Kong, T., Shinnerl, J.: Multilevel optimization for large-scale circuit placement. In: ICCAD (2000)","DOI":"10.1109\/ICCAD.2000.896469"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Chen, H.Y., Hsu, C.H., Chang Y.W.: High-performance global routing with fast overflow reduction. In: ASPDAC, January 2009","DOI":"10.1109\/ASPDAC.2009.4796543"},{"key":"9_CR12","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s11128-008-0082-9","volume":"7","author":"V Choi","year":"2008","unstructured":"Choi, V.: Minor-embedding in adiabatic quantum computation: I. the parameter setting problem. Quant. Inf. Proc. 7, 193\u2013209 (2008)","journal-title":"Quant. Inf. Proc."},{"key":"9_CR13","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/s11128-010-0200-3","volume":"10","author":"V Choi","year":"2011","unstructured":"Choi, V.: Minor-embedding in adiabatic quantum computation: II. minor-universal graph design. Quant. Inf. Proc. 10, 343\u2013353 (2011)","journal-title":"Quant. Inf. Proc."},{"key":"9_CR14","unstructured":"Correia, V.P., Reis A.I.: Classifying n-input boolean functions. In: VII Iberchip (2001)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Dechter, R.: Bucket elimination: a unifying framework for reasoning. In: Proceedings of the UAI (1996)","DOI":"10.1145\/242224.242302"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Denchev, V.S., Boixo, S., Isakov, S.V., Ding, N., Babbush, R., Smelyanskiy, V., Martinis, J., Neven, H.: What is the Computational Value of Finite-Range Tunneling? Ph.Rev.X (2016)","DOI":"10.1103\/PhysRevX.6.031015"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-72788-0_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"N Een","year":"2007","unstructured":"Een, N., Mishchenko, A., S\u00f6rensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272\u2013286. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-72788-0_26"},{"key":"9_CR18","unstructured":"Farhi, E., Goldstone, J., Gutmann, S., Sipser, M.: Quantum computation by adiabatic evolution. arXiv preprint (2000)"},{"key":"9_CR19","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/2442087.2442103","volume":"18","author":"M Gester","year":"2013","unstructured":"Gester, M., M\u00fcller, D., Nieberg, T., Panten, C., Schulte, C., Vygen, J.: Bonnroute: algorithms and data structures for fast and good VLSI routing. TODAES 18, 32 (2013)","journal-title":"TODAES"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Huang, Z., Wang, L., Nasikovskiy, Y., Mishchenko, A.: Fast boolean matching based on NPN classification. In: ICFPT (2013)","DOI":"10.1109\/FPT.2013.6718374"},{"key":"9_CR21","unstructured":"King, J., Yarkoni, S., Raymond, J., Ozfidan, I., King, A.D., Nevisi, M.M., Hilton, J.P., McGeoch, C.C.: Quantum Annealing amid Local Ruggedness and Global Frustration. arXiv preprint (2017)"},{"key":"9_CR22","doi-asserted-by":"crossref","first-page":"060512","DOI":"10.1103\/PhysRevB.82.060512","volume":"82","author":"T Lanting","year":"2010","unstructured":"Lanting, T., Harris, R., Johansson, J., Amin, M.H.S., Berkley, A.J., Gildert, S., Johnson, M.W., Bunyk, P., Tolkacheva, E., Ladizinsky, E., Ladizinsky, N., Oh, T., Perminov, I., Chapple, E.M., Enderud, C., Rich, C., Wilson, B., Thom, M.C., Uchaikin, S., Rose, G.: Cotunneling in pairs of coupled flux qubits. Phys. Rev. B 82, 060512 (2010)","journal-title":"Phys. Rev. B"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: Dag-aware aig rewriting: a fresh look at combinational logic synthesis. In: DAC (2006)","DOI":"10.1109\/DAC.2006.229287"},{"key":"9_CR24","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R., Wang, X., Kam T.: Technology mapping with boolean matching, supergates and choices (2005)"},{"key":"9_CR25","unstructured":"Mishchenko, A., Chatterjee, S., Jiang, R., Brayton, R.K.: Fraigs: a unifying representation for logic synthesis and verification. Technical report (2005)"},{"key":"9_CR26","first-page":"1066","volume":"27","author":"JA Roy","year":"2008","unstructured":"Roy, J.A., Markov, I.L.: High-performance routing at the nanometer scale. TCAD 27, 1066\u20131077 (2008)","journal-title":"TCAD"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Roy, J.A., Papa, D.A., Adya, S.N., Chan, H.H., Ng, A.N., Lu, J.F., Markov, I.L.: Capo: robust and scalable open-source min-cut floorplacer. In: ISPD (2005)","DOI":"10.1145\/1055137.1055184"},{"key":"9_CR28","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/2699915","volume":"16","author":"R Sebastiani","year":"2015","unstructured":"Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. TOCL 16, 12 (2015)","journal-title":"TOCL"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-21690-4_27","volume-title":"Computer Aided Verification","author":"R Sebastiani","year":"2015","unstructured":"Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 447\u2013454. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_27"},{"key":"9_CR30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1671970.1671972","volume":"15","author":"I Spence","year":"2010","unstructured":"Spence, I.: Sgen1: a generator of small but difficult satisfiability benchmarks. JEA 15, 1\u20132 (2010)","journal-title":"JEA"},{"key":"9_CR31","first-page":"349","volume":"14","author":"W-J Sun","year":"1995","unstructured":"Sun, W.-J., Sechen, C.: Efficient and effective placement for very large circuits. TCAD 14, 349\u2013359 (1995)","journal-title":"TCAD"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/11527695_24","volume-title":"Theory and Applications of Satisfiability Testing","author":"DAD Tompkins","year":"2005","unstructured":"Tompkins, D.A.D., Hoos, H.H.: UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306\u2013320. Springer, Heidelberg (2005). doi: 10.1007\/11527695_24"},{"key":"9_CR33","unstructured":"Xu, Y., Zhang, Y., Chu C.: Fastroute 4.0: global router with efficient via minimization. In: ASPDAC (2009)"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Zaribafiyan, A., Marchand, D.J.J., Rezaei, S.S.C.: Systematic and deterministic graph-minor embedding for cartesian products of graphs. CoRR (2016)","DOI":"10.1007\/s11128-017-1569-z"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66167-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T17:14:35Z","timestamp":1570036475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66167-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661667","9783319661674"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66167-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}