{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T22:53:35Z","timestamp":1687301615916},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T00:00:00Z","timestamp":1265846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["K\u00fcnstl Intell"],"published-print":{"date-parts":[[2010,4]]},"DOI":"10.1007\/s13218-010-0008-4","type":"journal-article","created":{"date-parts":[[2010,2,10]],"date-time":"2010-02-10T09:07:31Z","timestamp":1265792851000},"page":"15-23","source":"Crossref","is-referenced-by-count":1,"title":["A SAT Solver for Circuits Based on the Tableau Method"],"prefix":"10.1007","volume":"24","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leopold","family":"Haller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,2,11]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/B978-044450813-3\/50007-2","volume-title":"Handbook of automated reasoning, vol\u00a01","author":"M Baaz","year":"2001","unstructured":"Baaz M, Egly U, Leitsch A (2001) Normal form Transformations. In: Robinson JA, Voronkov A (eds) Handbook of automated reasoning, vol\u00a01. Elsevier Science, Amsterdam, pp 273\u2013333"},{"key":"8_CR2","first-page":"203","volume-title":"Proceedings AAAI","author":"RJ Bayardo Jr.","year":"1997","unstructured":"Bayardo RJ Jr., Schrag RC (1997) Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings AAAI. AAAI\/MIT, Menlo Park, pp 203\u2013208"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings DAC, pp\u00a0317\u2013320","DOI":"10.1145\/309847.309942"},{"issue":"4","key":"8_CR4","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","volume":"14","author":"T Boy de\u00a0la Tour","year":"1992","unstructured":"Boy de\u00a0la Tour T (1992) An optimality result for clause form translation. J Symb Comput 14(4):283\u2013301","journal-title":"J Symb Comput"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Cook SA (1971) The complexity of theorem-proving procedures. In: Proceedings STOC, pp\u00a0151\u2013158","DOI":"10.1145\/800157.805047"},{"issue":"1","key":"8_CR6","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook SA, Reckhow R (1979) The relative efficiency of propositional proof systems. J Symb Log 44(1):36\u201350","journal-title":"J Symb Log"},{"key":"8_CR7","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/BF00156916","volume":"1","author":"M D\u2019Agostino","year":"1992","unstructured":"D\u2019Agostino M (1992) Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence. J Log Lang Inf 1:235\u2013252","journal-title":"J Log Lang Inf"},{"issue":"3","key":"8_CR8","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M D\u2019Agostino","year":"1994","unstructured":"D\u2019Agostino M, Mondadori M (1994) The taming of the cut. Classical refutations with analytic cut. J Log Comput 4(3):285\u2013319","journal-title":"J Log Comput"},{"issue":"7","key":"8_CR9","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":"8_CR10","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":"8_CR11","volume-title":"Handbook of satisfiability","author":"R Drechsler","year":"2009","unstructured":"Drechsler R, Juntilla TA, Niemel\u00e4 I, (2009) Non-clausal SAT and ATPG. In: Handbook of satisfiability. IOS Press, Amsterdam"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N (2006) MiniSAT v2. 0 (beta). Solver description, SAT race","DOI":"10.3233\/SAT190014"},{"issue":"1","key":"8_CR13","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/s10601-008-9055-y","volume":"14","author":"U Egly","year":"2009","unstructured":"Egly U, Seidl M, Woltran S (2009) A solver for QBFs in negation normal form. Constraints 14(1):38\u201379","journal-title":"Constraints"},{"key":"8_CR14","unstructured":"Ganai MK, Ashar P, Gupta A, Zhang L, Malik S (2002) Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In: Proceedings DAC, pp\u00a0747\u2013750"},{"key":"8_CR15","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen G (1935) Untersuchungen \u00fcber das\u00a0logische Schlie\u00dfen. Math Z 39:176\u2013210, 405\u2013431","journal-title":"Math Z"},{"key":"8_CR16","unstructured":"Haller L (2008) Extending a tableau-based SAT procedure with techniques from CNF-based SAT. Master\u2019s thesis, Vienna University of Technology, Austria, December 2008"},{"key":"8_CR17","series-title":"LNCS","first-page":"75","volume-title":"Proceedings SAT","author":"H Jain","year":"2006","unstructured":"Jain H, Bartzis C, Clarke EM (2006) Satisfiability checking of non-clausal formulas using general matings. In: Proceedings SAT. LNCS, vol 4121. Springer, Berlin, pp 75\u201389"},{"issue":"3","key":"8_CR18","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s10601-008-9062-z","volume":"14","author":"M J\u00e4rvisalo","year":"2009","unstructured":"J\u00e4rvisalo M, Junttila T (2009) Limitations of restricted branching in clause learning. Constraints 14(3):325\u2013356","journal-title":"Constraints"},{"issue":"1\u20133","key":"8_CR19","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1016\/j.jalgor.2008.02.005","volume":"63","author":"M J\u00e4rvisalo","year":"2008","unstructured":"J\u00e4rvisalo M, Niemel\u00e4 I (2008) The effect of structural branching on the efficiency of clause learning SAT solving: an experimental study. J Algorithms 63(1\u20133):90\u2013113","journal-title":"J Algorithms"},{"key":"8_CR20","series-title":"LNCS","first-page":"553","volume-title":"Proceedings CL","author":"TA Junttila","year":"2000","unstructured":"Junttila TA, Niemel\u00e4 I (2000) Towards an efficient tableau method for Boolean circuit satisfiability checking. In: Proceedings CL. LNCS, vol 1861. Springer, Berlin, pp 553\u2013567"},{"key":"8_CR21","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/978-3-540-74105-3_2","volume-title":"Decision procedures","author":"D Kr\u00f6ning","year":"2008","unstructured":"Kr\u00f6ning D, Strichman O (2008) Decision procedures for propositional logic. In: Decision procedures. Springer, Berlin, pp 25\u201357"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Kuehlmann A, Ganai MK, Paruthi V (2001) Circuit-based Boolean reasoning. In: Proceedings DAC, pp 232\u2013237","DOI":"10.1145\/378239.378470"},{"issue":"5","key":"8_CR23","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva JP, Sakallah KA (1999) Grasp: a search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506\u2013521","journal-title":"IEEE Trans Comput"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings DAC, pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"8_CR25","series-title":"LNCS","first-page":"294","volume-title":"Proceedings SAT","author":"K Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat K, Darwiche A (2007) A lightweight component caching scheme for satisfiability solvers. In: Proceedings SAT. LNCS, vol 4501. Springer, Berlin, pp 294\u2013299"},{"issue":"3","key":"8_CR26","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"DA Plaisted","year":"1986","unstructured":"Plaisted DA, Greenbaum S (1986) A structure-preserving clause form translation. J Symb Comput 2(3):293\u2013304","journal-title":"J Symb Comput"},{"key":"8_CR27","series-title":"LNCS","first-page":"663","volume-title":"Proceedings CP","author":"C Thiffault","year":"2004","unstructured":"Thiffault C, Bacchus F, Walsh T (2004) Solving non-clausal formulas with DPLL search. In: Proceedings CP. LNCS, vol 3258. Springer, Berlin, pp 663\u2013678"},{"key":"8_CR28","first-page":"115","volume":"2","author":"GS Tseitin","year":"1968","unstructured":"Tseitin GS (1968) On the complexity of derivation in propositional calculus. Stud Constr Math Math Log 2:115\u2013125","journal-title":"Stud Constr Math Math Log"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Wu CA, Lin TH, Lee CC, Huang CYR (2007) QuteSAT: a robust circuit-based SAT solver for complex circuit structure. In: Proceedings DATE, pp 1313\u20131318","DOI":"10.1109\/DATE.2007.364479"},{"key":"8_CR30","first-page":"279","volume-title":"Proceedings ICCAD","author":"L Zhang","year":"2001","unstructured":"Zhang L, Madigan CF, Moskewicz MH, Malik S (2001) Efficient conflict driven learning in a Boolean satisfiability solver. In: Proceedings ICCAD. IEEE, New York, pp 279\u2013285"}],"container-title":["KI - K\u00fcnstliche Intelligenz"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-010-0008-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s13218-010-0008-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-010-0008-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T04:48:40Z","timestamp":1685422120000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s13218-010-0008-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,11]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["8"],"URL":"https:\/\/doi.org\/10.1007\/s13218-010-0008-4","relation":{},"ISSN":["0933-1875","1610-1987"],"issn-type":[{"value":"0933-1875","type":"print"},{"value":"1610-1987","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2,11]]}}}