{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T18:13:49Z","timestamp":1649182429667},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,8,14]],"date-time":"2014-08-14T00:00:00Z","timestamp":1407974400000},"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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1007\/s10703-014-0214-z","type":"journal-article","created":{"date-parts":[[2014,8,13]],"date-time":"2014-08-13T21:48:01Z","timestamp":1407966481000},"page":"111-143","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Quantifier elimination by dependency sequents"],"prefix":"10.1007","volume":"45","author":[{"given":"Eugene","family":"Goldberg","sequence":"first","affiliation":[]},{"given":"Panagiotis","family":"Manolios","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,8,14]]},"reference":[{"key":"214_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla P, Bjesse P, E\u00e9n N (2000) symbolic reachability analysis based on sAT-solvers. In: Proceedings of the 6th international conference on tools and algorithms for construction and analysis of systems, TACAs\u201900, pp 411\u2013425","DOI":"10.1007\/3-540-46419-0_28"},{"key":"214_CR2","doi-asserted-by":"crossref","unstructured":"Ayari A, Basin D (2002) Qubos: deciding quantified boolean logic using propositional satisfiability solvers. In: Proceedings of 4th international conference on formal methods in computer-aided design, vol 2517 of LNCS, FMCAD\u201902, pp 187\u2013201","DOI":"10.1007\/3-540-36126-X_12"},{"key":"214_CR3","unstructured":"Biere A (2004) Resolve and expand. In: Procedings of the seventh international conference on theory and applications of satisfiability testing, SAT\u201904, pp 59\u201370"},{"issue":"2\u20134","key":"214_CR4","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere A (2008) Picosat essentials. J Satisf Boolean Model Comput 4(2\u20134):75\u201397","journal-title":"J Satisf Boolean Model Comput"},{"key":"214_CR5","doi-asserted-by":"crossref","unstructured":"Bradley AR (2011) Sat-based model checking without unrolling. In: Proceedings of the 12th international conference on verification, model checking, and abstract interpretation, VMCAI\u201911, pp 70\u201387","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"214_CR6","doi-asserted-by":"crossref","unstructured":"Brauer J, King A, Kriener J (2011) Existential quantification as incremental sat. In: Proceedings of the 23rd international conference on computer aided verification, CAV\u201911, Springer-Verlag, pp 191\u2013207","DOI":"10.1007\/978-3-642-22110-1_17"},{"issue":"8","key":"214_CR7","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C\u201335","author":"R Bryant","year":"1986","unstructured":"Bryant R (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C\u201335(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"214_CR8","doi-asserted-by":"crossref","unstructured":"Chauhan P, Clarke E, Jha S, Kukula J, Veith H, Wang D (2001) Using combinatorial optimization methods for quantification scheduling. In: Proceedings of the 11th IFIP WG 10.5 advanced research working conference on correct hardware design and verification methods, CHARME \u201901, pp 293\u2013309","DOI":"10.1007\/3-540-44798-9_24"},{"key":"214_CR9","doi-asserted-by":"crossref","unstructured":"Clarke E, Emerson A (1982) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Proceedings of logic of programs, Workshop, pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"214_CR10","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"214_CR11","doi-asserted-by":"crossref","first-page":"608","DOI":"10.1145\/502090.502091","volume":"48","author":"A Darwiche","year":"2001","unstructured":"Darwiche A (2001) Decomposable negation normal form. J ACM 48:608","journal-title":"J ACM"},{"issue":"7","key":"214_CR12","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D (1962) A machine program for theorem proving. Commun ACM 5(7):394\u2013397","journal-title":"Commun ACM"},{"issue":"3","key":"214_CR13","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7(3):201\u2013215","journal-title":"J ACM"},{"key":"214_CR14","doi-asserted-by":"crossref","unstructured":"Ganai M, Gupta A, Ashar P (2004) Efficient sat-based unbounded symbolic model checking using circuit cofactoring. In: Proceedings of the 2004 IEEE\/ACM international conference on computer-aided design, ICCAD\u201904, pp 510\u2013517","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"214_CR15","doi-asserted-by":"crossref","unstructured":"Goldberg E (2009) Boundary points and resolution. In: Proceedings of theory and applications of satisfiability testing, 12th international conference, SAT\u201909, pp 147\u2013160","DOI":"10.1007\/978-3-642-02777-2_16"},{"key":"214_CR16","doi-asserted-by":"crossref","unstructured":"Goldberg E, Manolios P (2011) Sat-solving based on boundary point elimination. In: Proceedings of 6th international Haifa Verification Conference, pp 93\u2013111","DOI":"10.1007\/978-3-642-19583-9_12"},{"key":"214_CR17","unstructured":"Goldberg E, Manolios P (2012) Quantifier elimination by dependency sequents. In: Proceedings of formal methods in computer-aided design, FMCAD\u201912, pp 34\u201344"},{"key":"214_CR18","unstructured":"Goldberg E, Manolios P (2012) Removal of quantifiers by elimination of boundary points. Technical Report. arXiv:1204.1746v2 [cs.LO], Northeastern University"},{"key":"214_CR19","unstructured":"Goldberg E, Manolios P (2013) Quantifier elimination via clause redudnancy. In: Proceedings of formal methods in computer-aided design, FMCAD\u201913, pp 85\u201392"},{"key":"214_CR20","doi-asserted-by":"crossref","unstructured":"Jiang R (2009) Quantifier elimination via functional composition. In: Proceedings of the 21st international conference on computer aided verification, CAV\u201909, pp 383\u2013397","DOI":"10.1007\/978-3-642-02658-4_30"},{"key":"214_CR21","doi-asserted-by":"crossref","unstructured":"Jin H, Somenzi F (2005) Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In: Proceedings of the 42nd annual design automation conference, DAC\u201905, pp 750\u2013753","DOI":"10.1145\/1065579.1065775"},{"issue":"1\u20132","key":"214_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(98)00017-6","volume":"223","author":"O Kullmann","year":"1999","unstructured":"Kullmann O (1999) New methods for 3-sat decision and worst-case analysis. Theor Comput Sci 223(1\u20132):1\u201372","journal-title":"Theor Comput Sci"},{"key":"214_CR23","doi-asserted-by":"crossref","unstructured":"Marques-Silva J, Sakallah K (1996) Grasp: a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE\/ACM international conference on computer-aided design, ICCAD\u201996, pp 220\u2013227","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"214_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K McMillan","year":"1993","unstructured":"McMillan K (1993) Symbolic model checking. Kluwer Academic Publishers, Norwell"},{"key":"214_CR25","doi-asserted-by":"crossref","unstructured":"McMillan K (2002) Applying sat methods in unbounded symbolic model checking. In: Proceedings of the 14th international conference on computer aided verification, CAV\u201902, pp 250\u2013264","DOI":"10.1007\/3-540-45657-0_19"},{"key":"214_CR26","doi-asserted-by":"crossref","unstructured":"McMillan K (2003) Interpolation and sat-based model checking. In: Proceedings of computer aided verification, 15th international conference, CAV\u201903, Springer, pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"214_CR27","doi-asserted-by":"crossref","unstructured":"Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient sat solver. In: Proceedings of the 38th annual design automation conference, DAC\u201901, pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"214_CR28","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/S0166-218X(02)00409-2","volume":"130","author":"D Plaisted","year":"2003","unstructured":"Plaisted D, Biere A, Zhu Y (2003) A satisfiability procedure for quantified Boolean formulae. Discret Appl Math 130(2):291\u2013328","journal-title":"Discret Appl Math"},{"key":"214_CR29","doi-asserted-by":"crossref","unstructured":"Williams P, Biere A, Clarke E, Gupta A (2000) Combining decision diagrams and sat procedures for efficient symbolic model checking. In: Proceedings of the 12th international conference on computer aided verification, CAV\u201900, pp 124\u2013138","DOI":"10.1007\/10722167_13"},{"key":"214_CR30","unstructured":"C2D. http:\/\/reasoning.cs.ucla.edu\/c2d . Accessed 19 May 2013"},{"key":"214_CR31","unstructured":"HWMCC-2010 benchmarks. http:\/\/www.fmv.jku.at\/hwmcc10\/benchmarks.html . Accessed 3 April 2013"},{"key":"214_CR32","unstructured":"http:\/\/www.fmgroup.polito.it\/index.php\/download\/ . Accessed 5 May 2013"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0214-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0214-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0214-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,13]],"date-time":"2019-08-13T22:01:54Z","timestamp":1565733714000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0214-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,14]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["214"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0214-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,14]]}}}