{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T08:26:02Z","timestamp":1729671962722,"version":"3.28.0"},"reference-count":32,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,11]]},"DOI":"10.1109\/ictai.2013.153","type":"proceedings-article","created":{"date-parts":[[2014,2,13]],"date-time":"2014-02-13T21:07:37Z","timestamp":1392325657000},"page":"1020-1027","source":"Crossref","is-referenced-by-count":10,"title":["Compiling Pseudo-Boolean Constraints to SAT with Order Encoding"],"prefix":"10.1109","author":[{"given":"Naoyuki","family":"Tamura","sequence":"first","affiliation":[]},{"given":"Mutsunori","family":"Banbara","sequence":"additional","affiliation":[]},{"given":"Takehide","family":"Soh","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","first-page":"399","article-title":"Predicting learnt clauses quality in modern SAT solvers","author":"audemard","year":"2009","journal-title":"Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009)"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23786-7_47"},{"key":"18","article-title":"PBSugar: Compiling pseudo-boolean constraints to SAT with order encoding","author":"tamura","year":"0","journal-title":"July 2013 Presentation at the 4th International Workshop on Pragmatics of Sat (PoS 2013)"},{"key":"15","doi-asserted-by":"crossref","first-page":"467","DOI":"10.3233\/FI-2010-314","article-title":"A SAT-based method for solving the two-dimensional strip packing problem","volume":"102","author":"soh","year":"2010","journal-title":"Fundamenta Informaticae"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9064-x"},{"key":"13","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","article-title":"Efficient CNF encoding of Boolean cardinality constraints","author":"bailleux","year":"2003","journal-title":"Proceedings of the 9th International Conference on Principles and Practice of Constraint Programming (CP 2003)"},{"key":"14","article-title":"A new encoding of alldifferent into SAT","author":"gent","year":"2004","journal-title":"Proc 4th Int Works Modelling and Reformulating Constraint Satisfaction Problems"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9061-0"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_37"},{"key":"21","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","article-title":"The Sat4j library, release 2.2","volume":"7","author":"le berre","year":"2010","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"20","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/SAT190021","article-title":"A translation of pseudo Boolean constraints to SAT","volume":"2","author":"bailleux","year":"2006","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"22","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 (IJCAI 2007)"},{"key":"23","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190023","article-title":"On using cutting planes in pseudo-Boolean optimization","volume":"2","author":"manquinho","year":"2006","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_16"},{"key":"25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190014","article-title":"Translating pseudo-Boolean constraints into SAT","volume":"2","author":"een","year":"2006","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21581-0_34"},{"key":"27","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1007\/11564751_73","article-title":"Towards an optimal CNF encoding of Boolean cardinality constraints","author":"sinz","year":"2005","journal-title":"Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming (CP 2005)"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45193-8_79"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00144-6"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90009-O"},{"key":"2","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/3-540-45349-0_32","article-title":"Sat v csp","author":"walsh","year":"2000","journal-title":"Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP 2000)"},{"key":"10","first-page":"1092","article-title":"Experimental results on the application of satisfiability algorithms to scheduling problems","author":"crawford","year":"1994","journal-title":"Proceedings of the 12th National Conference on Artificial Int Elligence (AAAI 1994)"},{"key":"1","first-page":"290","article-title":"A comparison of atms and csp techniques","author":"de kleer","year":"1989","journal-title":"Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI 1989)"},{"key":"30","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1613\/jair.3653","article-title":"A new look at BDD s for pseudo-Boolean constraints","volume":"45","author":"abo","year":"2012","journal-title":"Journal of Artificial Intelligence Research"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74970-7_59"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2006.07.016"},{"key":"32","doi-asserted-by":"crossref","first-page":"103","DOI":"10.3233\/SAT190018","article-title":"The first evaluation of pseudo-Boolean solvers (PB05)","volume":"2","author":"manquinho","year":"2006","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"5","first-page":"253","article-title":"SAT-variable complexity of hard combinatorial problems","author":"iwama","year":"1994","journal-title":"Proceedings of the IFIP 13th World Computer Congress"},{"key":"31","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/978-3-642-02777-2_19","article-title":"New encodings of pseudo-Boolean constraints into CNF","author":"bailleux","year":"2009","journal-title":"Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009)"},{"key":"4","first-page":"121","article-title":"Arc consistency in SAT","author":"gent","year":"2002","journal-title":"Proceedings of the 15th European Conference on Artificial Intelligence (ECAI 2002)"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2011.53"},{"key":"8","first-page":"1","article-title":"Mapping problems with finitedomain variables into problems with Boolean variables","author":"ansotegui","year":"2004","journal-title":"Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004)"}],"event":{"name":"2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI)","start":{"date-parts":[[2013,11,4]]},"location":"Herndon, VA, USA","end":{"date-parts":[[2013,11,6]]}},"container-title":["2013 IEEE 25th International Conference on Tools with Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6734837\/6735210\/06735364.pdf?arnumber=6735364","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,15]],"date-time":"2020-08-15T10:33:16Z","timestamp":1597487596000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6735364\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":32,"URL":"https:\/\/doi.org\/10.1109\/ictai.2013.153","relation":{},"subject":[],"published":{"date-parts":[[2013,11]]}}}