On Satisfiability Solving Systems Based On Dynamical Automated Deduction With Contradiction Separation For Propositional Logic

Satisfiability(SAT)problem is not only a special class of constraint satisfaction problem(CSP),but also a famous decision one in the information science community.In the field of theory application,many classical computational problems,e.g.,coverage problem,packing problem,routing problem,scheduling problem and so on,are transformed into the SAT problem for solving.Moreover,in the field of practical application,model testing,software formal verification,hardware formal verification,intelligent planning and knowledge compilation,as well as other combinational optimization problem,are also postulated as the SAT problem for solving.Therefore,it is of great significance to investigate the efficient solving algorithm for SAT problem.Due to that the SAT problem is an NP complete one,none of SAT solver is always in a leading position.In terms of the disadvantages of the state-of-the-art CDCL solving algorithm,we start from the automated deduction theory based on contradiction separation proposed by Prof.Yang Xu,and perform the deep research in constructing the dynamic,multivariate deduction algorithm of contradiction separation.Moreover,two solvers,i.e.,automated deduction solver based on contradiction separation for propositional logic,and the solver of fusing the core of automated deduction solver with CDCL,have been developed independently.First of all,by implementing the basic algorithm of automated deduction solver based on contradiction separation for propositional logic and to investigate the mechanism of avoiding the potential searching conflict in CDCL,a clause learning algorithm with contradiction reconstruction is proposed.Specifically,the decision information between the backtracking level given by the conflict analysis in CDCL solver and the current conflict level is utilized to reconstruct the contradiction by selecting the appropriate clauses and further generate the learnt clauses.Reconstruction and CDCL conflict analysis can be simultaneously performed such that the uncertainty issues of deducing clauses,deducing literals,and deducing depth during the construction process of contradiction are addressed.Meanwhile,two learnt clauses are obtained once in CDCL solver,which represent two different spaces of conflict search respectively.As such,the capability of avoiding the conflict for the CDCL solver is enhanced.An extended solving algorithm based on contradiction separation is presented to address the issue that the single-branch decision mechanism for the CDCL solver is inefficient.This algorithm begins with the decision literals from the CDCL solver,and constructs the contradiction in the remaining unsatisfied clauses.Meanwhile,a group of locally assignment sequence is generated,which guides the solver to first search the solution space associated with the assignment sequence.And then the problem scale is gradually decreased by continuously constructing the contradiction and separating the satisfied clauses from the remaining clauses group by group.As far as the satisfied CNF formula are concerned,the locally satisfied solutions will be expanded to the globally satisfied ones by iteratively calling the deduction process.On the other hand,for the unsatisfied equations,if there exist empty clause in deducing results,we can directly make the decision.The locally satisfied assignment sequence is concluded from the contradiction construction,which itself reflects the potential searching conflict and has the higher decision efficiency compared with the decision mechanism only yielding one-branch decision texts once.Furthermore,we have studied the heuristic branching decision scheme,for which the heuristic branching literal selection algorithm based on activity evaluation is introduced after analyzing the scenario that the existing heuristic branching algorithms cannot effectively choose the next branch variable.In the process of conflict analysis,when the variables appear in conflict clauses and learnt clauses,the increment of their underlying activity is closely related to the decision level associated with the variables and the total conflict times of variables being assigned.The decision level indicates the partitioning relation of the corresponding subspaces to local search,while the total conflict times present the conflict varying trend in global search.The proposed algorithm comprehensively takes into account the relation between the decision level and the total conflict times,and introduces the functional factor to adjust these two quantities.The experimental results illustrate that the proposed algorithm is more reasonable to the classical EVSIDS evaluation way.The deletion algorithm of the learnt clauses has been researched.In view that the randomness is large and the utilization of the kept clauses is not high for the existing deletion algorithm of learnt clauses,two deletion algorithms are proposed respectively based on conflict analysis frequency and based on dynamic trend evaluation.The first deletion algorithm(randomly)retains the frequently-used clauses but forces to delete the hardly-used clauses to significantly improve the solving performance.The other deletion algorithm presents the quantization method of trend strength of learnt clauses as well as the light-weight implementation algorithm.The random and discrete time distribution is transformed into the continuous cumulative trend strength by building the transition model of trend strength of learnt clauses.When the deletion period is arrived at,the clauses with little possibility of being used in the subsequent search process will be deleted by setting the threshold of trend strength.This algorithm can significantly outperform the activity evaluation algorithm in efficiency,but having the comparable performance with the LBD algorithm.Finally,we study how to identify the repeated deduction path and put forward the identification algorithm of searching path based on vector space model by analyzing the issues on high randomicity of trigger condition and not too tight relation between restart algorithm and searching process.The Luby sequence is utilized to trigger the delaying restart decision,which converts current path and the searched paths to vector space models(VSMs)such that the similarity of VSMs is calculated to judge whether the current search process will get into the repetitive search space.Once the underlying similarity reaches a given threshold,the restart is triggered,otherwise it will be delayed.The comparative results show that the proposed algorithm can not only effectively avoid the repetitive search space,but also obviously improve the solving efficiency.