{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:33Z","timestamp":1749318093795,"version":"3.28.0"},"reference-count":18,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,9]]},"DOI":"10.1109\/fmcad.2015.7542255","type":"proceedings-article","created":{"date-parts":[[2016,8,15]],"date-time":"2016-08-15T20:28:56Z","timestamp":1471292936000},"page":"73-80","source":"Crossref","is-referenced-by-count":20,"title":["Skolem functions for factored formulas"],"prefix":"10.1109","author":[{"given":"Ajith K.","family":"John","sequence":"first","affiliation":[]},{"given":"Shetal","family":"Shah","sequence":"additional","affiliation":[]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[]},{"given":"Ashutosh","family":"Trivedi","sequence":"additional","affiliation":[]},{"given":"S.","family":"Akshay","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","first-page":"201","article-title":"A First Step Towards a Unified Proof Checker for QB F","volume":"4501","author":"jussila","year":"2007","journal-title":"Proc of SAT"},{"journal-title":"Berkeley Logic Synthesis and Verification Group ABC A system for sequential synthesis and verification","year":"0","key":"ref11"},{"key":"ref12","article-title":"Efficient Extraction of Skolem Functions from QRAT Proofs","author":"martina seidl","year":"2014","journal-title":"Proc of FMCAD"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"ref14","first-page":"303","article-title":"Binary decision diagrams","volume":"173","author":"fabio","year":"1999","journal-title":"Calculational System Design"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0223-4"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0057-7"},{"article-title":"Techniques in symbolic model checking","year":"2003","author":"trivedi","key":"ref17"},{"key":"ref18","first-page":"115","article-title":"On the complexity of derivation in propositional calculus","author":"tseitin","year":"1968","journal-title":"Structures in Constructive Mathematics and Mathematical Logic Part II Seminars in Mathematics"},{"key":"ref4","first-page":"369","article-title":"sKizzo: A Suite to Evaluate and Certify QBFs","author":"marco","year":"0","journal-title":"Proc of CADE"},{"key":"ref3","first-page":"275","article-title":"The Achilles' heel of QBF","volume":"2","author":"carlos","year":"2005","journal-title":"Proc Of AAAI"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref5","first-page":"17","article-title":"Strategic constraint satisfaction problems","author":"christian","year":"2006","journal-title":"Proc of CP"},{"key":"ref8","first-page":"149","author":"jiang","year":"2011","journal-title":"Resolution proofs and Skolem functions in QBF evaluation and applications In Proc of CAV"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_30"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/s10009-004-0179-0","article-title":"and Wonhong Nam. Symbolic computational techniques for solving games","volume":"7","author":"rajeev","year":"2005","journal-title":"STTT"},{"article-title":"Disjunctive Decomposition Benchmarks","year":"0","author":"john","key":"ref1"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542255"}],"event":{"name":"2015 Formal Methods in Computer-Aided Design (FMCAD)","start":{"date-parts":[[2015,9,27]]},"location":"Austin, TX, USA","end":{"date-parts":[[2015,9,30]]}},"container-title":["2015 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7539356\/7542233\/07542255.pdf?arnumber=7542255","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:45:25Z","timestamp":1498337125000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7542255\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9]]},"references-count":18,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2015.7542255","relation":{},"subject":[],"published":{"date-parts":[[2015,9]]}}}