MiniSat v1.13 - A SAT Solver with Conflict-Clause Minimization
作者： Niklas Sorensson , Niklas Een
DOI:
关键词:
摘要: In this poster we summarize the features of MiniSat version en- tering SAT Competition 2005. The main new feature is a resolution based conflict clause minimization technique on self-subsuming resolution. Ex- periments show that industrial examples, it not unusual for more than 30% literals in to be redundant. Removing these re- duces memory consumption and produce stronger clauses which may propagate under fewer decisions DPLL search procedure. We also want raise attention particular VSIDS im- plemented MiniSat, believe consistent improvement over original decision heuristic same magnitude as many recently proposed alternatives (GY02,Ry03).
minisat.se 参考文章(6)
Niklas Eén, Niklas Sörensson, An Extensible SAT-solver theory and applications of satisfiability testing. ,vol. 2919, pp. 502- 518 ,(2003) , 10.1007/978-3-540-24605-3_37
Niklas Eén, Armin Biere, Effective Preprocessing in SAT Through Variable and Clause Elimination Theory and Applications of Satisfiability Testing. ,vol. 3569, pp. 61- 75 ,(2005) , 10.1007/11499107_5
Lawrence Ryan, Efficient algorithms for clause-learning SAT solvers ,(2004)
J.P. Marques-Silva, K.A. Sakallah, GRASP: a search algorithm for propositional satisfiability IEEE Transactions on Computers. ,vol. 48, pp. 506- 521 ,(1999) , 10.1109/12.769433
E. Goldberg, Y. Novikov, BerkMin: A Fast and Robust Sat-Solver design, automation, and test in europe. pp. 142- 149 ,(2002) , 10.5555/882452.874512
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik, Chaff Proceedings of the 38th conference on Design automation - DAC '01. pp. 530- 535 ,(2001) , 10.1145/378239.379017