一种增加了对称破缺的改进子集可满足性算法

An improved sub-SAT algorithm of adding symmetry-breaking

为了消除子集可满足性算法在布线过程中带来运行时间增加的负面影响,提出了一种新的布线流程.针对子集可满足性算法在求解同时增加额外的变量和字句,而使得对称数量按指数级增长的问题,选用增加静态对称破缺的方法对合取范式(CNF)进行预处理,侦测并破缺其中的对称,从而达到减少搜索路径的目的.用简化图自同构的方法侦测所有对称,在增加合适的对称破缺判定(SBPs)后,限制搜索在空间的非对称领域进行,从而减少了搜索空间,而不影响CNF公式的可满足性.然后把预处理过的CNF送入布尔可满足性(SAT)解法器进行求解.试验结果表明,这种方法可以显著减少运行时间,加速求解过程.

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.