| [1] Cook S A. The complexity of theorem-proving procedures. InProc. the 3rd Symp. Theory of Comput., May 1971, pp.151-158.[2] Larrabee T. Test pattern generation using Boolean satisfiability.IEEE Trans. CAD, 1992, 11(1): 4-15.[3] Biere A, Cimatti A, Clarke E M, Fujita M, Zhu Y. Symbolicmodel checking using SAT procedures instead of BDDs. InProc. the 36th Conf. Design Automation, June 1999, pp.317-320.[4] Bjesse P, Leonard T, Mokkedem A. Finding bugs in an Alphamicroprocessor using satisfiability solvers. In Lecture Notes inComputer Science 2102, Berry G, Comon H, Finkel A (eds.),Springer-Verlag, 2001, pp.454-464.[5] Hung W N N, Narasimhan N. Reference model based RTLverification: An integrated approach. In Proc. the 9thHLDVT, November 2004, pp.9-13.[6] Hung W N N, Song X, Yang G, Yang J, Perkowski M. Optimalsynthesis of multiple output Boolean functions using aset of quantum gates by symbolic reachability analysis. IEEETrans. CAD, 2006, 25(9): 1652-1663.[7] Hung W N N, Gao C, Song X, Hammerstrom D. Defect tolerantCMOL cell assignment via satisfiability. IEEE SensorsJournal, 2008, 8(6): 823-830.[8] Wood R G, Rutenbar R A. FPGA routing and routability estimationvia Boolean satisfiability. In Proc. the 5th Int. Symp.Field-Programmable Gate Arrays, Feb. 1997, pp.119-125.[9] Song X, Hung W N N, Mishchenko A, Chrzanowska-Jeske M,Kennings A, Coppola A. Board-level multiterminal net assignmentfor the partial cross-bar architecture. IEEE Trans.VLSI Systems, 2003, 11(3): 511-514.[10] Hung W N N, Song X, Kam T, Cheng L, Yang G. Routabilitychecking for three-dimensional architectures. IEEE Trans.VLSI Systems, 2004, 12(12): 1371-1374.[11] Hung W N N, Song X, Aboulhamid E M et al. Segmentedchannel routability via satisfiability. Trans. Design Automa-tion of Electronic Systems, 2004, 9(4): 517-528.[12] He F, Hung W N N, Song X, Gu M, Sun J. A satisfiabilityformulation for FPGA routing with pin rearrangements. In-ternational Journal of Electronics, 2007, 94(9): 857-868.[13] Wang J, Chen M, Wan X, Wei J. Ant-colony-optimizationbasedscheduling algorithm for uplink CDMA nonreal-timedata. IEEE Trans. Vehicular Tech., 2009, 58(1): 231-241.[14] Wang J, Chen M,Wang J. Adaptive channel and power allocationof downlink multi-user MC-CDMA systems. Computersand Electrical Engineering, 2009, 35(5): 622-633.[15] Wang J, Chen H, Chen M et al. Cross-layer packet schedulingfor downlink multiuser OFDM systems. Science in ChinaSeries F: Inform. Sci., 2009, 52(12): 2369-2377.[16] Davis M, Putnam H. A computing procedure for quantificationtheory. J. ACM, 1960, 7(3): 201-215.[17] Davis M, Logemann G, Loveland D. A machine program fortheorem proving. Comms. ACM, 1962, 5(7): 394-397.[18] Gu J. Local search for satisfiability (SAT) problem. Trans.Systems, Man, and Cybernetics, 1993, 23(4): 1108-1129.[19] Selman B, Kautz H A, Cohen B. Noise strategies for improvinglocal search. In Proc. the 12th National Conference onArtificial Intelligence, July 31-August 4, 1994, pp.337-343.[20] Zhao C, Zhou H, Zheng Z, Xu K. A message-passing approachto random constraint satisfaction problems with growing domains.Journal of Statistical Mechanics: Theory and Experi-ment, 2011, P02019.[21] Zhao C, Zhang P, Zheng Z, Xu K. Analytical and beliefpropagation studies of random constraint satisfaction problemswith growing domains. Physical Review E, 2012,85(1/2): 016106.[22] Selman B, Levesque H, Mitchell D. A new method for solvinghard satisfiability problems. In Proc. the 10th NationalConference on Artificial Intelligence, July 1992, pp.440-446.[23] Zhang L, Madigan C, Moskewicz M et al. Efficient conflictdriven learning in a Boolean satisfiability solver. In Proc. Int.Conf. Computer-Aided Design, Nov. 2001, pp.279-285.[24] Goldberg E, Novikov Y. BerkMin: A fast and robust SATsolver.In Proc. Design Automation and Test in Europe,March 2002, pp.142-149.[25] Eén N, Sörensson N. Translating pseudo-Boolean constraintsinto SAT. Journal on Satisfiability, Boolean Modeling andComputation, 2006, 2(1/4): 1-26.[26] Pipatsrisawat K, Darwiche A. RSat 1.03: SAT solver description.Technical Report D-152, Automated Reasoning Group,Computer Science Department, UCLA, 2006.[27] Xu K, Li W. Exact phase transitions in random constraintsatisfaction problems. Journal of Artificial Intelligence Re-search, 2000, 12: 93-103.[28] Franco J, Paull M. Probabilistic analysis of the Davis Putnamprocedure for solving the satisfiability problem. Discrete Ap-plied Mathematics, 1983, 5(1): 77-87.[29] Xu L, Hutter F, Hoos H H et al. SATzilla: Portfolio-basedalgorithm selection for SAT. Journal of Artificial IntelligenceResearch, 2008, 32(1): 565-606.[30] Xu K, Li W. Many hard examples in exact phase transitions.Theoretical Computer Science, 2006, 355(3): 291-302.[31] Xu K, Boussemart F, Hemery F, Lecoutre C. Random constraintsatisfaction: Easy generation of hard (satisfiable) instances.Artificial Intelligence, 2007, 171(8/9): 514-534.[32] Jiang W, Liu T, Ren T, Xu K. Two hardness results on feedbackvertex sets. In Lecture Notes in Computer Science 6681,Atallah M, Li X, Zhu B (eds.), Springer, 2011, pp.233-243.[33] Liu T, Lin X, Wang C, Su K, Xu K. Large hinge width onsparse random hypergraphs. In Proc. the 22nd Int. JointConf. Artificial Intelligence, July 2011, pp.611-616.[34] Wang C, Liu T, Cui P, Xu K. A note on treewidth in randomgraphs. In Lecture Notes in Computer Science 6831, WangW, Zhu X, Du D (eds.), Springer-Verlag, 2011, pp.491-499.[35] Zhang L. SAT-solving: From Davis-Putnam to Zchaff and beyond,2003. http://research.microsoft.com/enus/people/lintaoz/sat-course1.pdf.[36] Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SATmodulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, 2006,53(6): 937-977.[37] Pullan W, Hoos H H. Dynamic local search for the maximumclique problem. Journal of Artificial Intelligence Research,2006, 25: 159-185.[38] Cai S, Su K, Sattar A. Local search with edge weighting andconfiguration checking heuristics for minimum vertex cover.Artificial Intelligence, 2011, 175: 1672-1696.[39] Cai S, Su K, Chen Q. EWLS: A new local search for minimumvertex cover. In Proc. the 24th AAAI Conference onArtificial Intelligence, July 2010, pp.45-50.[40] Richter C G S, Helmert M. A stochastic local search approachto vertex cover. In Proc. the 30th Annual German Confer-ence on Artificial Intelligence, Sept. 2007, pp.412-426. |