[1] DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theorem proving[J]. Communications of the ACM, 1962, 5(7):394-397. [2] MOSKEWICZ M W, MADIGAN C F, ZHAO Y, et al. Chaff:engineering an efficient sat solver[C]//Proceedings of the 38th Annual Design Automation Conference. New York:ACM, 2001:530-535. [3] ANSÓTEGUI C, BONET M L, LEVY J. SAT-based MaxSAT algorithms[J]. Artificial Intelligence, 2013, 196:77-105. [4] KOSHIMURA M, ZHANG T, FUJITA H, et al. QMaxSAT:a partial Max-SAT solver system description[J]. Journal on Satisfiability, Boolean Modeling and Computation, 2012, 8(1/2):95-100. [5] ZHANG L T, MADIGAN C F, MOSKEWICZ M H, et al. Efficient conflict driven learning in a boolean satisfiability solver[C]//ICCAD 2001:Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design. Piscataway, NJ:IEEE, 2001:279-285. [6] LIU Y L, LI C M, HE K, et al. Breaking cycle structure to improve lower bound for Max-SAT[C]//FAW 2016:Proceeding of the 11th International Workshop on Frontiers in Algorithmics, LNCS 9711. Berlin:Springer, 2016:111-124. [7] AUDEMARD G, SIMON L. Predicting learnt clauses quality in modern SAT solvers[C]//IJCAI 2009:Proceeding of the 2009 International Joint Conference on Artificial Intelligence. San Francisco, CA:Morgan Kaufmann, 2009:399-404. [8] AUDEMARD G, LAGNIEZ J M, SIMON L. Improving glucose for incremental SAT solving with assumption:application to MUS extraction[C]//SAT 2013:Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing. Berlin:Springer, 2013:309-317. [9] DE KLERK E. Aspects of Semidefinite Programming[M]. Berlin:Springer, 2002:211-228. [10] 刘燕丽,李初民,何琨.基于优化冲突集提高下界的MaxSAT完备算法[J].计算机学报,2013,36(10):2087-2095.(LIU Y L, LI C M, HE K. Improved lower bounds in MAXSAT complete algorithm based optimizing inconsistent set[J]. Chinese Journal of Computers, 2013, 36(10):2087-2095.) [11] 刘燕丽,黄飞,张婷.基于环型扩展推理规则的MaxSAT完备算法[J].南京大学学报(自然科学版),2015,51(4):762-771.(LIU Y L, HUANG F, ZHANG T. MaxSAT complete algorithm based cycle extended inference rules[J]. Journal of Nanjing University (Natural Sciences), 2015, 51(4):762-771.) [12] AUDEMARD G, SIMON L. Lazy clause exchange policy for parallel SAT solvers[C]//SAT 2014:Proceedings of the 201417th International Conference on Theory and Applications of Satisfiability Testing, LNCS 8561. Berlin:Springer, 2014:197-205. |