{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:41:25Z","timestamp":1764783685067,"version":"3.28.0"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/memcod.2014.6961846","type":"proceedings-article","created":{"date-parts":[[2014,11,26]],"date-time":"2014-11-26T15:57:36Z","timestamp":1417017456000},"page":"84-93","source":"Crossref","is-referenced-by-count":5,"title":["Structure-aware CNF obfuscation for privacy-preserving SAT solving"],"prefix":"10.1109","author":[{"given":"Ying","family":"Qin","sequence":"first","affiliation":[]},{"given":"ShengYu","family":"Shen","sequence":"additional","affiliation":[]},{"given":"Yan","family":"Jia","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1007\/11496137_9"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/2554797.2554820"},{"key":"18","first-page":"465","article-title":"Non-interactive verifiable computing: Outsourcing computation to untrusted workers","author":"gennaro","year":"2010","journal-title":"Crypto"},{"key":"15","first-page":"256","article-title":"Generating satisfiable problem instances","author":"achlioptas","year":"2000","journal-title":"AAAI\/IAAI"},{"key":"16","article-title":"Equivalence checking hardware multiplier designs","author":"jarvisalo","year":"0","journal-title":"SAT Competition 2007 Benchmark Description"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2232005"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653687"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2007.81"},{"journal-title":"MiniSat-Sat Algorithms and Applications Invited Talk Given by Niklas Sorensson at the CADE-20 Workshop ESCAR","year":"0","key":"12"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-005-0070-3"},{"key":"20","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/S0065-2458(01)80019-X","article-title":"Secure outsourcing of scientific computations","volume":"54","author":"atallah","year":"2001","journal-title":"Advances in Computers"},{"key":"22","first-page":"425","article-title":"Uncheatable distributed computations","author":"golle","year":"2001","journal-title":"CT-RSA"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2003.1199338"},{"journal-title":"Paralleling OpenSMT Towards Cloud Computing","year":"0","key":"24"},{"journal-title":"Formal in the Cloud OneSpin New Spin on Cloud Computing","year":"0","key":"25"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.5772\/9632"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1997.597203"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11119-3_18"},{"key":"3","first-page":"154","article-title":"Helmut veith: Counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"CAV"},{"key":"2","first-page":"1","volume":"i xxiii","author":"hachtel","year":"2006","journal-title":"Logic Synthesis and Verification Algorithms"},{"key":"10","first-page":"361","article-title":"Restoring circuit structure from sat instances","author":"roy","year":"0","journal-title":"IWLS'04"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2011.5935305"},{"key":"6","article-title":"On the complexity of derivation in propositional calculus","author":"tseitin","year":"1968","journal-title":"Studies in Constr Math and Math Logic"},{"key":"5","first-page":"385","article-title":"Grid-based sat solving with iterative partitioning and clause learning","author":"hyv\ufffdrinen","year":"2011","journal-title":"CP"},{"key":"4","first-page":"244","article-title":"Extending SAT solvers to cryptographic problems","author":"soos","year":"2009","journal-title":"SAT"},{"key":"9","first-page":"185","article-title":"Recovering and exploiting structural knowledge from cnf formulas","author":"ostrowski","year":"2002","journal-title":"CP"},{"key":"8","first-page":"291","article-title":"Integrating equivalency reasoning into davis-putnam procedure","author":"li","year":"2000","journal-title":"AAAI\/IAAI"}],"event":{"name":"2014 Twelfth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2014)","start":{"date-parts":[[2014,10,19]]},"location":"Lausanne, Switzerland","end":{"date-parts":[[2014,10,21]]}},"container-title":["2014 Twelfth ACM\/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6950639\/6961832\/06961846.pdf?arnumber=6961846","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T21:00:51Z","timestamp":1498165251000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6961846\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/memcod.2014.6961846","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}