{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:37:58Z","timestamp":1759639078654,"version":"3.37.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030206512"},{"type":"electronic","value":"9783030206529"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-20652-9_23","type":"book-chapter","created":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:03:25Z","timestamp":1558983805000},"page":"341-354","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing CNF SAT Symmetry Breaking in PVS"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3704-1060","authenticated-orcid":false,"given":"David E.","family":"Narv\u00e1ez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,5,28]]},"reference":[{"issue":"9","key":"23_CR1","doi-asserted-by":"publisher","first-page":"1117","DOI":"10.1109\/TCAD.2003.816218","volume":"22","author":"FA Aloul","year":"2003","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult instances of Boolean satisfiability in the presence of symmetry. IEEE Trans. CAD Integr. Circ. Syst. 22(9), 1117\u20131137 (2003). \n                    https:\/\/doi.org\/10.1109\/TCAD.2003.816218","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"issue":"5","key":"23_CR2","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1109\/TC.2006.75","volume":"55","author":"FA Aloul","year":"2006","unstructured":"Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for Boolean satisfiability. IEEE Trans. Comput. 55(5), 549\u2013558 (2006). \n                    https:\/\/doi.org\/10.1109\/TC.2006.75","journal-title":"IEEE Trans. Comput."},{"issue":"1\u20134","key":"23_CR3","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10817-018-9455-7","volume":"61","author":"JC Blanchette","year":"2018","unstructured":"Blanchette, J.C., Fleury, M., Lammich, P., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. J. Autom. Reason. 61(1\u20134), 333\u2013365 (2018). \n                    https:\/\/doi.org\/10.1007\/s10817-018-9455-7","journal-title":"J. Autom. Reason."},{"key":"23_CR4","doi-asserted-by":"publisher","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: 3rd Annual ACM Symposium on Theory of Computing, pp. 151\u2013158. ACM (1971). \n                    https:\/\/doi.org\/10.1145\/800157.805047","DOI":"10.1145\/800157.805047"},{"key":"23_CR5","unstructured":"Crawford, J.: A theoretical analysis of reasoning by symmetry in first-order logic. In: AAAI Workshop on Tractable Reasoning, pp. 17\u201322 (1992)"},{"key":"23_CR6","first-page":"148","volume-title":"Knowledge Representation and Reasoning","author":"JM Crawford","year":"1996","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Aiello, L.C., Doyle, J., Shapiro, S.C. (eds.) Knowledge Representation and Reasoning, pp. 148\u2013159. Morgan Kaufmann, Burlington (1996)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-40970-2_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"J Devriendt","year":"2016","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104\u2013122. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-40970-2_8"},{"issue":"5\u20136","key":"23_CR8","doi-asserted-by":"publisher","first-page":"636","DOI":"10.1017\/S1471068416000508","volume":"16","author":"J Devriendt","year":"2016","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: On local domain symmetry for model expansion. Theory Pract. Logic Program. 16(5\u20136), 636\u2013652 (2016)","journal-title":"Theory Pract. Logic Program."},{"key":"23_CR9","doi-asserted-by":"publisher","unstructured":"Heule, M.: The quest for perfect and compact symmetry breaking for graph problems. In: Davenport, J.H., et al. (eds.) 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 149\u2013156. IEEE Computer Society (2016). \n                    https:\/\/doi.org\/10.1109\/SYNASC.2016.034","DOI":"10.1109\/SYNASC.2016.034"},{"issue":"8","key":"23_CR10","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/3107239","volume":"60","author":"M Heule","year":"2017","unstructured":"Heule, M., Kullmann, O.: The science of brute force. Commun. ACM 60(8), 70\u201379 (2017). \n                    https:\/\/doi.org\/10.1145\/3107239","journal-title":"Commun. ACM"},{"issue":"50","key":"23_CR11","doi-asserted-by":"publisher","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F Mari\u0107","year":"2010","unstructured":"Mari\u0107, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor. Comput. Sci. 411(50), 4333\u20134356 (2010). \n                    https:\/\/doi.org\/10.1016\/j.tcs.2010.09.014","journal-title":"Theor. Comput. Sci."},{"key":"23_CR12","unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS. Contractor Report NASA\/CR-2003-212418, NASA, Langley Research Center, Hampton VA 23681\u20132199, USA, May 2003"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). \n                    https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"23_CR14","unstructured":"Owre, S., Shankar, N.: Abstract datatypes in PVS. Technical report SRI-CSL-93-9R, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993. Extensively revised June 1997; Also available as NASA Contractor Report CR-97-206264"},{"key":"23_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2011.03.002","volume":"269","author":"N Shankar","year":"2011","unstructured":"Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-based satisfiability solver. Electron. Notes Theor. Comput. Sci. 269, 3\u201317 (2011). \n                    https:\/\/doi.org\/10.1016\/j.entcs.2011.03.002","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Yu, Y., Subramanyan, P., Tsiskaridze, N., Malik, S.: All-SAT using minimal blocking clauses. In: 27th International Conference on VLSI Design and 13th International Conference on Embedded Systems, pp. 86\u201391 (2014). \n                    https:\/\/doi.org\/10.1109\/VLSID.2014.22","DOI":"10.1109\/VLSID.2014.22"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-20652-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:17:58Z","timestamp":1558984678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-20652-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030206512","9783030206529"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-20652-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 May 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/robonaut.jsc.nasa.gov\/R2\/pages\/nfm2019.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}