- ISSN 0258-2724
- CN 51-1277/U
- EI Compendex
- Scopus
- Indexed by Core Journals of China, Chinese S&T Journal Citation Reports
- Chinese S&T Journal Citation Reports
- Chinese Science Citation Database
| Citation: | CHEN Qingshan, XU Yang, HE Xingxing. Heuristic Complete Algorithm for SAT Problem by Using Logical Deduction[J]. Journal of Southwest Jiaotong University, 2017, 30(6): 1224-1232. doi: 10.3969/j.issn.0258-2724.2017.06.025
|
|
COOK S A. The complexity of theorem-proving procedures[C]//3rd Annual ACM Symposium on Theory of Computing. New York:ACM, 1971:151-158.
|
|
DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theoremproving[J]. Communications of the ACM, 1962, 5(7):394-397.
|
|
MOSKEWICZ M W, MADIGAN C F, ZHAO Y. Chaff:engineering an efficient SAT solver[C]//Proceedings of the 38th Annual Design Automation Conference. New York:ACM, 2001:530-535.
|
|
EÉN N, SÖENSSON N. An extensible SAT solver[C]//SAT 2003. Heidelberg:Springer, 2015:502-518.
|
|
GOMES C P, SELMAN B, KAUTZ H.Boosting combinatorial search through randomization[C]//Proceeding of the Fifteenth National Conference on Artificial Intelligence. Madison:AAAI Press, 1998:431-437.
|
|
GOLDBERG E, NOVIKOV Y.BerkMin:a fast and robust SATsolver[C]//Proceedings of Design, Automation and Test in Europe Conference. Los Alamitos:IEEE Computer Society Press, 2002:142-149.
|
|
LEWIS M D T,SCHUBERT T, BECKER B. Speedup techniques utilized in modern SAT solvers[C]//International Conference in Theory and Applications of Satisfiability Testing. Heidelberg:Springer, 2005:437-443.
|
|
RYAN L. Efficient algorithms for clause-learning SAT solvers[D]. Vancouver:Simon Fraser University, 2004.
|
|
MARQUES-SILVA J P, LYNCE I, MALIK S. Conflict-driven clause learning SAT solvers[M]//In Handbook of Satisfiability. Amsterdam:IOS Press, 2009:127-149.
|
|
MARQUES-SILVA J P, SAKALLAH K A. Grasp:a new search algorithm for satisfiability[C]//Proceedings of the 1996 IEEE/ACM International Conference onComputer-aided Design. Los Alamitos:IEEE Computer Society Press, 1996:220-227.
|
|
BIERE A. Pico SAT essentials[J]. Journal on Satisfiability, Boolean Modeling and Computation, 2008, 4:75-97.
|
|
AUDEMARD G, SIMON L. Glucose 2.3 in the SAT 2013 Competition[C]//Theory and Applications of Satisfiability Testing-SAT 2008. Heidelberg:Springer, 2013:42-43.
|
|
BELOV A, DIEPOLD D, HEULE M J H, et al. SAT competition 2014 solver and benchmark descriptions. (2014-6-27)[2016-10-15]. https://helda.helsinki.fi/bitstream/handle/10138/135571/sc2014_proceedings.pdf?sequence=1.
|
|
JEROSLOW R E, WANG J. Solving propositional satisfiability problems[J]. Annals of Mathematics and Artificial Intelligence, 1990:167-187.
|
|
BURO M, KLEINE-BVING H.Report on a SAT competition[R]. Paderborn:University of Paderborn, 1992.
|
|
FREEMAN J W. Improvements to propositional satisfiability search algorithms[D]. Philadelphia:University of Pennsylvania, 1995.
|
|
LIANG J H, GANESH V,POUPART P, et al. Learning rate based branchingheuristic for SAT solvers[C]//In Theory and Applications of Satisfiability Testing-SAT 2016.[S.l.]:Springer, 2016:123-140.
|
|
BIERE A, FROHLICH A. Evaluating CDCL variable scoring schemes[C]//In Theory and Applications of Satisfiability Testing-SAT 2015.[S.l.]:Springer, 2015:405-422.
|
|
BIERE A. Adaptive restart strategies for conflict driven SAT solvers[C]//Theory and Applications of Satisfiability Testing-SAT 2008.Heidelberg:Springer, 2008:28-33.
|
|
CHANGC L, LEE R C T. Symbolic logic and mechanical theorem proving[M]. New York:Academic Press, 1973:130-162.
|
|
LOVELAND D W. A Linear Format for Resolution[M]. New York:Springer, 1970:147-162.
|
|
LUCKHAM D. Refinements in Resolution Theory[M]. New York:Springer, 1970:163-190.
|
DownLoad: