An improved sub-SAT algorithm of adding symmetry-breaking
1.School of Information Technology,Jiangnan University,Wuxi,Jiangsu 214122,China; 2.China Electronics Technology Group Corporation No.58 Research Institute,Wuxi,Jiangsu 214035,China
Abstract：In order to eliminate the negative effect of increasing running time of sub-SAT algorithm in the routing process,a new routing flow was proposed.Additional variables and clauses were introduced by sub-SAT,and the number of symmetries was made with exponential growth in the solving process.In responseto this problem,static symmetry-breaking was used to carry out pretreatment of conjunctive normalform（CNF）,detect and break the symmetries therein.Consequently,the purpose of reducing the search path was achieved.The method of reduction to graph automorphism was used to detect all symmetries.After adding appropriate symmetry-breaking predicates（SBPs）,the search space was confined to non-symmetric regions of the space without affecting the satisfiability to the CNF formula.A SAT solver was then applied to the preprocessed CNF formula.Results of experiments show that this approach can reduce the runtime and speed up the solving process.
2010, Vol. 31 
