{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:17:15Z","timestamp":1725585435201},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642215803"},{"type":"electronic","value":"9783642215810"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21581-0_8","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T09:30:19Z","timestamp":1307698219000},"page":"76-89","source":"Crossref","is-referenced-by-count":2,"title":["DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Ignatiev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Semenov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Aloul, F.A., Mneimneh, M.N., Sakallah, K.A.: ZBDD-Based Backtrack Search SAT Solver. In: Proceedings of International Workshop on Logic and Synthesis (IWLS), pp. 131\u2013136 (2002)","key":"8_CR1"},{"unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Tech. Rep. 10\/1, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2010)","key":"8_CR2"},{"issue":"8","key":"8_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"8_CR4","series-title":"LNCS(LNAI)","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/10721959_35","volume-title":"Automated Deduction - CADE-17","author":"P. Chatalic","year":"2000","unstructured":"Chatalic, P., Simon, L.: Zres: The old Davis-Putnam procedure meets ZBDDs. In: McAllester, D. (ed.) CADE 2000. LNCS(LNAI), vol.\u00a01831, pp. 449\u2013454. Springer, Heidelberg (2000)"},{"doi-asserted-by":"crossref","unstructured":"Damiano, R.F., Kukula, J.H.: Checking satisfiability of a conjunction of BDDs. In: 40th Design Automation Conference, DAC 2003, pp. 818\u2013823 (2003)","key":"8_CR5","DOI":"10.1145\/775832.776039"},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W.F. Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional horn formulae. The Journal of Logic Programming\u00a01(3), 267\u2013284 (1984)","journal-title":"The Journal of Logic Programming"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"8_CR8","series-title":"Series on Integrated Circuits and Systems","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-69167-1","volume-title":"SAT-Based Scalable Formal Verification Solutions","author":"M. Ganai","year":"2007","unstructured":"Ganai, M., Gupta, A.: SAT-Based Scalable Formal Verification Solutions. Series on Integrated Circuits and Systems. Springer-Verlag New York, Inc., Secaucus (2007)"},{"doi-asserted-by":"crossref","unstructured":"Gopalakrishnan, S., Durairaj, V., Kalla, P.: Integrating CNF and BDD based SAT solvers. In: IEEE International High-Level Design, Validation, and Test Workshop, pp. 51\u201356 (2003)","key":"8_CR9","DOI":"10.1109\/HLDVT.2003.1252474"},{"key":"8_CR10","first-page":"245","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a Parallel SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation, Special Issue on Parallel SAT Solving\u00a06, 245\u2013262 (2009)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation, Special Issue on Parallel SAT Solving"},{"key":"8_CR11","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1613\/jair.2097","volume":"29","author":"J. Huang","year":"2007","unstructured":"Huang, J., Darwiche, A.: The Language of Search. Journal of Artificial Intelligence Research\u00a029, 191\u2013219 (2007)","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"3","key":"8_CR12","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10601-008-9062-z","volume":"14","author":"M. J\u00e4rvisalo","year":"2009","unstructured":"J\u00e4rvisalo, M., Junttila, T.: Limitations of restricted branching in clause learning. Constraints\u00a014(3), 325\u2013356 (2009)","journal-title":"Constraints"},{"issue":"12","key":"8_CR13","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A. Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification. IEEE Transactions on Computer-Aided Design\u00a021(12), 1377\u20131394 (2002)","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C.Y. Lee","year":"1959","unstructured":"Lee, C.Y.: Representation of Switching Circuits by Binary-Decision Programs. Bell Systems Technical Journal\u00a038, 985\u2013999 (1959)","journal-title":"Bell Systems Technical Journal"},{"issue":"1","key":"8_CR15","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/s10472-005-0425-5","volume":"43","author":"I. Lynce","year":"2005","unstructured":"Lynce, I., Marques-Silva, J.: Efficient data structures for backtrack search SAT solvers. Annals of Mathematics and Artificial Intelligence\u00a043(1), 137\u2013152 (2005)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"5","key":"8_CR16","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"8_CR17","first-page":"530","volume-title":"Proceedings of the 38th Annual Design Automation Conference, DAC 2001","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, DAC 2001, pp. 530\u2013535. ACM, New York (2001)"},{"key":"8_CR18","first-page":"203","volume":"6","author":"T. Schubert","year":"2009","unstructured":"Schubert, T., Lewis, M., Becker, B.: PaMiraXT: Parallel SAT Solving with Threads and Message Passing. Journal on Satisfiability, Boolean Modeling and Computation, Special Issue on Parallel SAT Solving\u00a06, 203\u2013222 (2009)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation, Special Issue on Parallel SAT Solving"},{"unstructured":"Semenov, A., Zaikin, O., Bespalov, D., Posypkin, M.: Parallel algorithms for SAT in application to inversion problems of some discrete functions, arXiv:1102.3563v1 [cs.DC]","key":"8_CR19"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M. Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT Solvers to Cryptographic Problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 244\u2013257. Springer, Heidelberg (2009)"},{"issue":"1","key":"8_CR21","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1177\/1094342005051521","volume":"19","author":"R. Thakur","year":"2005","unstructured":"Thakur, R., Rabenseifner, R., Gropp, W.: Optimization of Collective Communication Operations in MPICH. Int\u2019l Journal of High Performance Computing Applications\u00a019(1), 49\u201366 (2005)","journal-title":"Int\u2019l Journal of High Performance Computing Applications"},{"key":"8_CR22","first-page":"234","volume":"2","author":"G. Tseitin","year":"1968","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a02, 234\u2013259 (1968)","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21581-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,28]],"date-time":"2019-03-28T11:13:03Z","timestamp":1553771583000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21581-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642215803","9783642215810"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21581-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}