{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T06:01:17Z","timestamp":1783749677406,"version":"3.55.0"},"reference-count":59,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"12","license":[{"start":{"date-parts":[[2010,12,1]],"date-time":"2010-12-01T00:00:00Z","timestamp":1291161600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2010,12]]},"DOI":"10.1109\/tcad.2010.2061631","type":"journal-article","created":{"date-parts":[[2010,11,30]],"date-time":"2010-11-30T21:08:25Z","timestamp":1291151305000},"page":"2027-2040","source":"Crossref","is-referenced-by-count":4,"title":["A Novel SAT-Based Approach to the Task Graph Cost-Optimal Scheduling Problem"],"prefix":"10.1109","volume":"29","author":[{"given":"Sergio","family":"Nocco","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.126"},{"key":"ref38","author":"barth","year":"1995","journal-title":"A Davis-Putnam enumeration algorithm for linear pseudo-Boolean optimization"},{"key":"ref33","first-page":"695","author":"roussel","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.842808"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(90)90139-4"},{"key":"ref30","first-page":"852","article-title":"solving the minimum cost satisfiability problem using sat based branch and bound search","author":"fu","year":"2006","journal-title":"Proc Int Conf Comput -Aided Design"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_19"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065775"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_19"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/43.998623"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1996.545572"},{"key":"ref29","author":"li","year":"2004","journal-title":"Optimization algorithms for the minimum-cost satisfiability problem"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/43.62794"},{"key":"ref1","author":"de micheli","year":"1994","journal-title":"Synthesis and Optimization of Digital Circuits"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1059816.1059823"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1287\/trsc.34.2.180.12302","article-title":"Scheduling aircraft landings: The static case","volume":"34","author":"abramson","year":"2000","journal-title":"Transport Sci"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/EURMIC.1999.794484"},{"key":"ref24","first-page":"220","volume":"2988","author":"larsen","year":"2004","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref23","first-page":"493","article-title":"as cheap as possible: efficient cost-optimal reachability for priced timed automata","author":"behrmann","year":"2001","journal-title":"Proc Comput -Aided Verification"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1992.279335"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0014-1"},{"key":"ref50","author":"en","year":"2009","journal-title":"The Minisat SAT Solver"},{"key":"ref51","first-page":"1","article-title":"Translating pseudo-Boolean constraint into SAT","volume":"2","author":"en","year":"2006","journal-title":"Int JSAT"},{"key":"ref59","first-page":"209","article-title":"On using cutting planes in pseudo-Boolean optimization","volume":"2","author":"manquinho","year":"2006","journal-title":"Int JSAT"},{"key":"ref58","first-page":"165","article-title":"Pueblo: A hybrid pseudo-Boolean SAT solver","volume":"2","author":"sheini","year":"2006","journal-title":"Int JSAT"},{"key":"ref57","first-page":"543","article-title":"Temporal induction by incremental SAT solving","author":"en","year":"2003","journal-title":"Proc 1st Int Workshop BMC"},{"key":"ref56","year":"0","journal-title":"Standard Task Graph Set"},{"key":"ref55","author":"behrmann","year":"2006","journal-title":"The Uppaal Tool"},{"key":"ref54","author":"manquinho","year":"2009","journal-title":"Results of the fourth pseudo Boolean competition"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/s12532-008-0001-1"},{"key":"ref52","year":"0","journal-title":"The SCIP (Solving Constraint Integer Programs) Solver"},{"key":"ref10","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1109\/43.75629","article-title":"a formal approach to the scheduling problem in high-level synthesis","volume":"10","author":"hwang","year":"1991","journal-title":"IEEE Trans Comput -Aided Design"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/43.31522"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"ref12","first-page":"41","article-title":"automatic scheduling to minimize shipbuilding cost","author":"dain","year":"2005","journal-title":"Proc 12th Int Conf Comput Applicat Shipbuilding"},{"key":"ref13","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1145\/288548.289074","article-title":"efficient encoding for exact symbolic automata-based scheduling","author":"haynal","year":"1998","journal-title":"Proc Int Conf Comput -Aided Design"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82547-2"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA.1999.811256"},{"key":"ref17","first-page":"43","article-title":"guided synthesis of control programs using uppaal","volume":"8","author":"hune","year":"2001","journal-title":"Nordic J Comput"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v8i3.20457"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45351-2_8"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/43.486271"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1109\/43.75629","article-title":"a formal approach to the scheduling problem in high level synthesis","volume":"10","author":"hwang","year":"1991","journal-title":"IEEE Trans Comput -Aided Design"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/581199.581252"},{"key":"ref5","author":"haynal","year":"1999","journal-title":"Automata-based scheduling for looping DFGs"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0170-9"},{"key":"ref49","first-page":"312","article-title":"using decision procedures efficiently for optimization","author":"streeter","year":"2007","journal-title":"Proc Int Conf Automat Plan Schedul"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2002.1106801"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190053"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2003.1213431"},{"key":"ref45","first-page":"27","article-title":"Task scheduling in multiprocessor systems","volume":"28","author":"el-rewini","year":"1995","journal-title":"IEEE Trans Comput"},{"key":"ref48","first-page":"827","article-title":"toward an optimal cnf encoding of boolean cardinality constraints","author":"sinz","year":"2005","journal-title":"Proc Int Conf Principles Pract Constr Programm"},{"key":"ref47","first-page":"108","article-title":"efficient cnf encoding of boolean cardinality constraints","volume":"lncs 2833","author":"bailleux","year":"2003","journal-title":"Proc Int Conf Principles Pract Constr Programm"},{"key":"ref42","first-page":"1194","article-title":"Pushing the envelope: Planning, propositional logic, and stochastic search","author":"kautz","year":"1996","journal-title":"Proc 13th Nat Conf AAAI"},{"key":"ref41","first-page":"359","article-title":"Planning as satisfiability","author":"kautz","year":"1992","journal-title":"Proc Eur Conf Artif Intell"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"ref43","first-page":"5","article-title":"An overview of recent algorithms for AI planning","volume":"2","author":"rintanen","year":"2001","journal-title":"Knstliche Intelligenz"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/43\/5621029\/05621035.pdf?arnumber=5621035","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,23]],"date-time":"2021-12-23T16:17:02Z","timestamp":1640276222000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5621035\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12]]},"references-count":59,"journal-issue":{"issue":"12"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2010.2061631","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12]]}}}