{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T10:23:53Z","timestamp":1782987833071,"version":"3.54.5"},"reference-count":29,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1109\/iri.2014.7051971","type":"proceedings-article","created":{"date-parts":[[2015,3,3]],"date-time":"2015-03-03T15:16:47Z","timestamp":1425395807000},"page":"803-810","source":"Crossref","is-referenced-by-count":11,"title":["Extending modern SAT solvers for models enumeration"],"prefix":"10.1109","author":[{"given":"Said","family":"Jabbour","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jerry","family":"Lonlac","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lakhdar","family":"Sais","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yakoub","family":"Salhi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72200-7_13"},{"key":"ref11","first-page":"275","article-title":"Memory efficient all-solutions sat solver and its application for reachability analysis","author":"grumberg","year":"2004","journal-title":"In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD)"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2011.05.002"},{"key":"ref13","article-title":"On when and how to use sat to mine frequent itemsets","author":"henriques","year":"2012","journal-title":"CoRR abs\/1207 6253"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_19"},{"key":"ref15","first-page":"552","article-title":"Constraint programming for mining nary patterns","author":"khiari","year":"2010","journal-title":"Proceedings of the 16th International Conference on Principles and Practice of Constraint Programming (CP‘ 10)"},{"key":"ref16","first-page":"73","article-title":"On a generalization of extended resolution","volume":"34","author":"kullmann","year":"1997","journal-title":"Discrete Applied Mathematics"},{"key":"ref17","first-page":"58","article-title":"Filtering techniques for rapid user classification","author":"lane","year":"1998","journal-title":"AAAI-98\/ICML-98 Joint Workshop on AI Approaches to Time-series Analysis"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.04.004"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"ref28","first-page":"279","article-title":"Efficient conflict driven learning in Boolean satisfiability solver","author":"zhang","year":"2001","journal-title":"IEEE\/ACM CAD'2001"},{"key":"ref4","article-title":"Using sat based image computation for reachability analysis","author":"pankaj","year":"2003","journal-title":"Technical report Technical Report CMU-C S-03-151"},{"key":"ref27","article-title":"A linear-time transformation of linear inequalities into conjunctive normal form","author":"warners","year":"1996","journal-title":"Information Processing Letters"},{"key":"ref3","article-title":"Handbook of Satisfiability","volume":"185","author":"armin","year":"2009","journal-title":"Frontiers in AI and Applications"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21581-0_11"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/CADCG.2009.5246850"},{"key":"ref5","first-page":"258","article-title":"A sat-based approach for discovering frequent, closed and maximal patterns in a se-quence","author":"coquery","year":"2012","journal-title":"Proceedings of the 20th European Conference on Artificial Intelligence (ECAI'12)"},{"key":"ref8","first-page":"35","article-title":"Finding all solutions if you can find one","author":"dechter","year":"1992","journal-title":"Proc of the AAAI-92 Workshop on Tractable Reasoning"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"ref2","first-page":"108","article-title":"Efficient cnf encoding of boolean cardinality constraints","author":"bailleux","year":"2003","journal-title":"In CP 2003"},{"key":"ref9","first-page":"386","article-title":"Conflict-driven answer set solving","author":"gebser","year":"2007","journal-title":"Proceedings of the 20th International Joint Conference on Artificial Intelligence Hyderabad India January 6-12 2007(IJCAI‘2007)"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s10878-006-9029-1"},{"key":"ref20","first-page":"250","article-title":"Applying sat methods in unbounded symbolic model checking","author":"kenneth","year":"2002","journal-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV'02)"},{"key":"ref22","first-page":"297","article-title":"Pattern discovery on character sets and real-valued data: Linear bound on irredundant motifs and an efficient polynomial time algorithm","author":"parida","year":"2000","journal-title":"ACM-SIAM Symposium on Discrete Algorithms"},{"key":"ref21","first-page":"131","article-title":"Good Learning and Implicit Model Enumeration","author":"ant\u00f3nio","year":"2005","journal-title":"International Conference on Tools with Artificial Intelligence (ICTAI'2005)"},{"key":"ref24","first-page":"204","article-title":"Constraint programming for itemset mining","author":"de","year":"2008","journal-title":"ACM SIGKDD"},{"key":"ref23","article-title":"Bases of motifs for generating repeated patterns with wild cards","volume":"2","author":"pisanti","year":"2003","journal-title":"IEEEIACM TCBB'2003"},{"key":"ref26","first-page":"827","article-title":"Towards an optimal cnf encoding of boolean cardinality constraints","author":"sinz","year":"2005","journal-title":"CP'05"},{"key":"ref25","doi-asserted-by":"crossref","DOI":"10.1609\/aaai.v24i1.7707","article-title":"Constraint programming for data mining and machine learning","author":"de raedt","year":"2010","journal-title":"Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence (AAAI'10)"}],"event":{"name":"2014 IEEE International Conference on Information Reuse and Integration (IRI)","location":"Redwood City, CA, USA","start":{"date-parts":[[2014,8,13]]},"end":{"date-parts":[[2014,8,15]]}},"container-title":["Proceedings of the 2014 IEEE 15th International Conference on Information Reuse and Integration (IEEE IRI 2014)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7036233\/7051718\/07051971.pdf?arnumber=7051971","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,8]],"date-time":"2023-08-08T11:20:53Z","timestamp":1691493653000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7051971"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/iri.2014.7051971","relation":{},"subject":[],"published":{"date-parts":[[2014,8]]}}}