{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:54Z","timestamp":1725540534117},"reference-count":22,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009,6]]},"DOI":"10.1109\/hpcsim.2009.5195312","type":"proceedings-article","created":{"date-parts":[[2009,8,11]],"date-time":"2009-08-11T19:09:58Z","timestamp":1250017798000},"page":"161-167","source":"Crossref","is-referenced-by-count":5,"title":["Comparison of knowledge sharing strategies in a parallel QBF solver"],"prefix":"10.1109","author":[{"given":"Paolo","family":"Marin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Narizzano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Giunchiglia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Lewis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Schubert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1016\/0167-8191(96)00024-5"},{"journal-title":"Quantified Boolean Formulas Satisfiability Library (QBFLIB)","year":"2001","author":"giunchiglia","key":"22"},{"key":"17","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190063","article-title":"pmsat: a parallel version of minisat","author":"gil","year":"2008","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_46"},{"key":"15","first-page":"37","article-title":"gridsat: a chaff-based distributed sat solver for the grid","author":"chrabakh","year":"2003","journal-title":"ACM\/IEEE conference on Supercomputing"},{"key":"16","article-title":"a distributed algorithm to evaluate quantified boolean formulae","author":"feldmann","year":"2000","journal-title":"Proc AAAI"},{"key":"13","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-3-540-30494-4_15","article-title":"qube++: an efficient qbf solver","author":"giunchiglia","year":"2004","journal-title":"International Conference on Formal Methods In Computer-Aided Design"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0030"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_36"},{"key":"12","first-page":"200","article-title":"towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation","author":"zhang","year":"2002","journal-title":"International Conference on Principles and Practice of Constraint Programming"},{"key":"21","article-title":"reasoning with quantified boolean formulas","author":"giunchiglia","year":"2009","journal-title":"Frontiers in Artificial Intelligence and Applications"},{"key":"3","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","article-title":"constructing conditional plans by a theorem prover","author":"rintanen","year":"1999","journal-title":"Journal of Artificial Intelligence Research"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/MPIDC.1996.534093"},{"key":"2","first-page":"408","article-title":"bounded model checking with qbf","author":"dershowitz","year":"2005","journal-title":"SAT"},{"key":"1","first-page":"531","article-title":"on combining 01xlogic and qbf","author":"herbstritt","year":"2007","journal-title":"International Conference on Computer Aided Systems Theory"},{"key":"10","article-title":"solution learning and solution directed backjumping revisited","author":"gent","year":"2004","journal-title":"Tech Rep APES-80-2004"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1145\/1120725.1120821"},{"key":"5","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","article-title":"clause\/term resolution and learning in the evaluation of quantified boolean formulas","author":"giunchiglia","year":"2006","journal-title":"Journal of Artificial Intelligence Research (JAIR)"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/HPCSIM.2009.5195312"},{"key":"9","first-page":"369","article-title":"skizzo: a suite to evaluate and certify qbfs","author":"benedetti","year":"2005","journal-title":"Proc CADE"},{"key":"8","first-page":"59","article-title":"resolve and expand","author":"biere","year":"2004","journal-title":"Proc SAT"}],"event":{"name":"Simulation (HPCS)","start":{"date-parts":[[2009,6,21]]},"location":"Leipzig, Germany","end":{"date-parts":[[2009,6,24]]}},"container-title":["2009 International Conference on High Performance Computing & Simulation"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5173446\/5191573\/05195312.pdf?arnumber=5195312","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,21]],"date-time":"2020-05-21T09:58:31Z","timestamp":1590055111000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5195312\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6]]},"references-count":22,"URL":"https:\/\/doi.org\/10.1109\/hpcsim.2009.5195312","relation":{},"subject":[],"published":{"date-parts":[[2009,6]]}}}