Research Of Algorithms For #SAT Problem Based On Incremental Solving

The satisfiability problem(SAT)is a decision problem of judging whether or not a conjunctive normal form is true,its computational complexity is NP-complete.Many problems in the field of artificial intelligence such as constraint model checking,circuit delay fault testing and so on,can be converted into SAT problem to solve,and there is no lack of a series of similar problems among them.Early SAT solver can't use instance similarity,every problem must solve from scratch.In recent years,with the emergence of incremental SAT algorithm and the widespread application,the efficiency of solving this series of instance has a very clearly improvement.As an extension of the SAT problem,model counting problem(#SAT)is need to calculate the satisfiable assignment number of a conjunctive normal form,its computational complexity is #p-complete.The problem has been widely used in such fields as consistency planning and probability reasoning,which also contains a lot of similar problems.Due to the difficulty of solving the problem,so it is more important to realize the using of reusable information in #SAT solver.In order to solve the similar #SAT problems in real life more effective,we improve the basic precise cachet algorithm in this paper,and propose the incremental model counting algorithm.Firstly,compare multiple instance and find out the update clauses,then put them in the input file according to the specified format.Then,solve the original formula,and cache the reusable information in the process of solving.After that we read the input file again,analyze and process the update clauses according to the satisfiability and the cache information.Do loop like this until finishing the solving of the entire input file.In addition,we also used a similar incremental approach to improve the weighted #SAT algorithm,which provides a new idea of handling multiple similar weighted problems.To test the algorithm's efficiency,we first select randomly fields and graph coloring fields instances,and make contrast experiments between cachet and the algorithm in this paper.Then we select the difficult instances in the field of probabilistic inference,and make contrast experiments between general weighed #SAT algorithm and the incremental algorithm in this paper.The experimental results confirmed the effectiveness of the incremental algorithm in these fields.