{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:24:18Z","timestamp":1745987058828,"version":"3.40.4"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,3,1]],"date-time":"2013-03-01T00:00:00Z","timestamp":1362096000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2013,3]]},"DOI":"10.1007\/s11390-013-1326-4","type":"journal-article","created":{"date-parts":[[2013,3,11]],"date-time":"2013-03-11T21:18:41Z","timestamp":1363036721000},"page":"247-254","source":"Crossref","is-referenced-by-count":2,"title":["Complete Boolean Satisfiability Solving Algorithms Based on Local Search"],"prefix":"10.1007","volume":"28","author":[{"given":"Wen-Sheng","family":"Guo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guo-Wu","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William N. N.","family":"Hung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoyu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,3,12]]},"reference":[{"key":"1326_CR1","doi-asserted-by":"crossref","unstructured":"Cook S A. The complexity of theorem-proving procedures. In Proc. the 3rd Symp. Theory of Comput., May 1971, pp.151-158.","DOI":"10.1145\/800157.805047"},{"issue":"1","key":"1326_CR2","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T Larrabee","year":"1992","unstructured":"Larrabee T. Test pattern generation using Boolean satisfiability. IEEE Trans. CAD, 1992, 11(1): 4\u201315.","journal-title":"IEEE Trans. CAD"},{"key":"1326_CR3","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E M, Fujita M, Zhu Y. Symbolic model checking using SAT procedures instead of BDDs. In Proc. the 36th Conf. Design Automation, June 1999, pp.317-320.","DOI":"10.1145\/309847.309942"},{"key":"1326_CR4","doi-asserted-by":"crossref","unstructured":"Bjesse P, Leonard T, Mokkedem A. Finding bugs in an Alpha microprocessor using satisfiability solvers. In Lecture Notes in Computer Science 2102, Berry G, Comon H, Finkel A (eds.), Springer-Verlag, 2001, pp.454-464.","DOI":"10.1007\/3-540-44585-4_44"},{"key":"1326_CR5","doi-asserted-by":"crossref","unstructured":"Hung W\u00a0N\u00a0N, Narasimhan N. Reference model based RTL verification: An integrated approach. In Proc. the 9th HLDVT, November 2004, pp.9-13.","DOI":"10.1109\/HLDVT.2004.1431221"},{"issue":"9","key":"1326_CR6","doi-asserted-by":"crossref","first-page":"1652","DOI":"10.1109\/TCAD.2005.858352","volume":"25","author":"WNN Hung","year":"2006","unstructured":"Hung W\u00a0N\u00a0N, Song X, Yang G, Yang J, Perkowski M. Optimal synthesis of multiple output Boolean functions using a set of quantum gates by symbolic reachability analysis. IEEE Trans. CAD, 2006, 25(9): 1652\u20131663.","journal-title":"IEEE Trans. CAD"},{"issue":"6","key":"1326_CR7","doi-asserted-by":"crossref","first-page":"823","DOI":"10.1109\/JSEN.2008.923261","volume":"8","author":"WNN Hung","year":"2008","unstructured":"Hung W\u00a0N\u00a0N, Gao C, Song X, Hammerstrom D. Defect tolerant CMOL cell assignment via satisfiability. IEEE Sensors Journal, 2008, 8(6): 823\u2013830.","journal-title":"IEEE Sensors Journal"},{"key":"1326_CR8","doi-asserted-by":"crossref","unstructured":"Wood R G, Rutenbar R A. FPGA routing and routability estimation via Boolean satisfiability. In Proc. the 5th Int. Symp. Field-Programmable Gate Arrays, Feb. 1997, pp.119-125.","DOI":"10.1145\/258305.258322"},{"issue":"3","key":"1326_CR9","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1109\/TVLSI.2003.812322","volume":"11","author":"X Song","year":"2003","unstructured":"Song X, Hung W\u00a0N\u00a0N, Mishchenko A, Chrzanowska-Jeske M, Kennings A, Coppola A. Board-level multiterminal net assignment for the partial cross-bar architecture. IEEE Trans. VLSI Systems, 2003, 11(3): 511\u2013514.","journal-title":"IEEE Trans. VLSI Systems"},{"issue":"12","key":"1326_CR10","doi-asserted-by":"crossref","first-page":"1371","DOI":"10.1109\/TVLSI.2004.837999","volume":"12","author":"WNN Hung","year":"2004","unstructured":"Hung W\u00a0N\u00a0N, Song X, Kam T, Cheng L, Yang G. Routability checking for three-dimensional architectures. IEEE Trans. VLSI Systems, 2004, 12(12): 1371\u20131374.","journal-title":"IEEE Trans. VLSI Systems"},{"issue":"4","key":"1326_CR11","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/1027084.1027090","volume":"9","author":"WNN Hung","year":"2004","unstructured":"Hung W\u00a0N\u00a0N, Song X, Aboulhamid E M et al. Segmented channel routability via satisfiability. Trans. Design Automation of Electronic Systems, 2004, 9(4): 517\u2013528.","journal-title":"Trans. Design Automation of Electronic Systems"},{"issue":"9","key":"1326_CR12","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1080\/00207210701650661","volume":"94","author":"F He","year":"2007","unstructured":"He F, Hung W\u00a0N\u00a0N, Song X, Gu M, Sun J. A satisfiability formulation for FPGA routing with pin rearrangements. International Journal of Electronics, 2007, 94(9): 857\u2013868.","journal-title":"International Journal of Electronics"},{"issue":"1","key":"1326_CR13","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1109\/TVT.2008.924983","volume":"58","author":"J Wang","year":"2009","unstructured":"Wang J, Chen M, Wan X, Wei J. Ant-colony-optimizationbased scheduling algorithm for uplink CDMA nonreal-time data. IEEE Trans. Vehicular Tech., 2009, 58(1): 231\u2013241.","journal-title":"IEEE Trans. Vehicular Tech."},{"issue":"5","key":"1326_CR14","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1016\/j.compeleceng.2009.01.003","volume":"35","author":"J Wang","year":"2009","unstructured":"Wang J, Chen M,Wang J. Adaptive channel and power allocation of downlink multi-user MC-CDMA systems. Computers and Electrical Engineering, 2009, 35(5): 622\u2013633.","journal-title":"Computers and Electrical Engineering"},{"issue":"12","key":"1326_CR15","doi-asserted-by":"crossref","first-page":"2369","DOI":"10.1007\/s11432-009-0219-1","volume":"52","author":"J Wang","year":"2009","unstructured":"Wang J, Chen H, Chen M et al. Cross-layer packet scheduling for downlink multiuser OFDM systems. Science in China Series F: Inform. Sci., 2009, 52(12): 2369\u20132377.","journal-title":"Science in China Series F: Inform. Sci."},{"issue":"3","key":"1326_CR16","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis M, Putnam H. A computing procedure for quantification theory. J. ACM, 1960, 7(3): 201\u2013215.","journal-title":"J. ACM"},{"issue":"7","key":"1326_CR17","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D. A machine program for theorem proving. Comms. ACM, 1962, 5(7): 394\u2013397.","journal-title":"Comms. ACM"},{"issue":"4","key":"1326_CR18","doi-asserted-by":"crossref","first-page":"1108","DOI":"10.1109\/21.247892","volume":"23","author":"J Gu","year":"1993","unstructured":"Gu J. Local search for satisfiability (SAT) problem. Trans. Systems, Man, and Cybernetics, 1993, 23(4): 1108\u20131129.","journal-title":"Cybernetics"},{"key":"1326_CR19","unstructured":"Selman B, Kautz H A, Cohen B. Noise strategies for improving local search. In Proc. the 12th National Conference on Artificial Intelligence, July 31-August 4, 1994, pp.337-343."},{"key":"1326_CR20","doi-asserted-by":"crossref","unstructured":"Zhao C, Zhou H, Zheng Z, Xu K. A message-passing approach to random constraint satisfaction problems with growing domains. Journal of Statistical Mechanics: Theory and Experiment, 2011, P02019.","DOI":"10.1088\/1742-5468\/2011\/02\/P02019"},{"issue":"1\/2","key":"1326_CR21","doi-asserted-by":"crossref","first-page":"016106","DOI":"10.1103\/PhysRevE.85.016106","volume":"85","author":"C Zhao","year":"2012","unstructured":"Zhao C, Zhang P, Zheng Z, Xu K. Analytical and belief-propagation studies of random constraint satisfaction problems with growing domains. Physical Review E, 2012, 85(1\/2): 016106.","journal-title":"Physical Review E"},{"key":"1326_CR22","unstructured":"Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. In Proc. the 10th National Conference on Artificial Intelligence, July 1992, pp.440-446."},{"key":"1326_CR23","unstructured":"Zhang L, Madigan C, Moskewicz M et al. Efficient conflict driven learning in a Boolean satisfiability solver. In Proc. Int. Conf. Computer-Aided Design, Nov. 2001, pp.279-285."},{"key":"1326_CR24","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y. BerkMin: A fast and robust SATsolver. In Proc. Design Automation and Test in Europe, March 2002, pp.142-149.","DOI":"10.1109\/DATE.2002.998262"},{"issue":"1\/4","key":"1326_CR25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190014","volume":"2","author":"N E\u00e9n","year":"2006","unstructured":"E\u00e9n N, S\u00f6rensson N. Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2006, 2(1\/4): 1\u201326.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"1326_CR26","unstructured":"Pipatsrisawat K, Darwiche A. RSat 1.03: SAT solver description. Technical Report D-152, Automated Reasoning Group, Computer Science Department, UCLA, 2006."},{"key":"1326_CR27","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1613\/jair.696","volume":"12","author":"K Xu","year":"2000","unstructured":"Xu K, Li W. Exact phase transitions in random constraint satisfaction problems. Journal of Artificial Intelligence Research, 2000, 12: 93\u2013103.","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"1","key":"1326_CR28","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","volume":"5","author":"J Franco","year":"1983","unstructured":"Franco J, Paull M. Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem. Discrete Applied Mathematics, 1983, 5(1): 77\u201387.","journal-title":"Discrete Applied Mathematics"},{"issue":"1","key":"1326_CR29","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu L, Hutter F, Hoos H\u00a0H et al. SATzilla: Portfolio-based algorithm selection for SAT. Journal of Artificial Intelligence Research, 2008, 32(1): 565\u2013606.","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"3","key":"1326_CR30","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/j.tcs.2006.01.001","volume":"355","author":"K Xu","year":"2006","unstructured":"Xu K, Li W. Many hard examples in exact phase transitions. Theoretical Computer Science, 2006, 355(3): 291\u2013302.","journal-title":"Theoretical Computer Science"},{"issue":"8\/9","key":"1326_CR31","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1016\/j.artint.2007.04.001","volume":"171","author":"K Xu","year":"2007","unstructured":"Xu K, Boussemart F, Hemery F, Lecoutre C. Random constraint satisfaction: Easy generation of hard (satisfiable) instances. Artificial Intelligence, 2007, 171(8\/9): 514\u2013534.","journal-title":"Artificial Intelligence"},{"key":"1326_CR32","doi-asserted-by":"crossref","unstructured":"Jiang W, Liu T, Ren T, Xu K. Two hardness results on feedback vertex sets. In Lecture Notes in Computer Science 6681, Atallah M, Li X, Zhu B (eds.), Springer, 2011, pp.233-243.","DOI":"10.1007\/978-3-642-21204-8_26"},{"key":"1326_CR33","unstructured":"Liu T, Lin X, Wang C, Su K, Xu K. Large hinge width on sparse random hypergraphs. In Proc. the 22nd Int. Joint Conf. Artificial Intelligence, July 2011, pp.611-616."},{"key":"1326_CR34","doi-asserted-by":"crossref","unstructured":"Wang C, Liu T, Cui P, Xu K. A note on treewidth in random graphs. In Lecture Notes in Computer Science 6831, Wang W, Zhu X, Du D (eds.), Springer-Verlag, 2011, pp.491-499.","DOI":"10.1007\/978-3-642-22616-8_38"},{"key":"1326_CR35","unstructured":"Zhang L. SAT-solving: From Davis-Putnam to Zchaff and beyond, 2003. http:\/\/research.microsoft.com\/enus\/people\/lintaoz\/sat-course1.pdf ."},{"issue":"6","key":"1326_CR36","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 2006, 53(6): 937\u2013977.","journal-title":"Journal of the ACM"},{"key":"1326_CR37","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1613\/jair.1815","volume":"25","author":"W Pullan","year":"2006","unstructured":"Pullan W, Hoos H\u00a0H. Dynamic local search for the maximum clique problem. Journal of Artificial Intelligence Research, 2006, 25: 159\u2013185.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"1326_CR38","doi-asserted-by":"crossref","first-page":"1672","DOI":"10.1016\/j.artint.2011.03.003","volume":"175","author":"S Cai","year":"2011","unstructured":"Cai S, Su K, Sattar A. Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artificial Intelligence, 2011, 175: 1672\u20131696.","journal-title":"Artificial Intelligence"},{"key":"1326_CR39","doi-asserted-by":"crossref","unstructured":"Cai S, Su K, Chen Q. EWLS: A new local search for minimum vertex cover. In Proc. the 24th AAAI Conference on Artificial Intelligence, July 2010, pp.45-50.","DOI":"10.1609\/aaai.v24i1.7539"},{"key":"1326_CR40","doi-asserted-by":"crossref","unstructured":"Richter C G\u00a0S, Helmert M. A stochastic local search approach to vertex cover. In Proc. the 30th Annual German Conference on Artificial Intelligence, Sept. 2007, pp.412-426.","DOI":"10.1007\/978-3-540-74565-5_31"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-013-1326-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-013-1326-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-013-1326-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T00:15:54Z","timestamp":1745972154000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-013-1326-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["1326"],"URL":"https:\/\/doi.org\/10.1007\/s11390-013-1326-4","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"type":"print","value":"1000-9000"},{"type":"electronic","value":"1860-4749"}],"subject":[],"published":{"date-parts":[[2013,3]]}}}