Study On Complete Algorithm For MaxSAT Problem

There are many constraints in real life,plans must be made in the condition that all the constraints or as many constraints as possible can be satisfied in the plans.They are called constraint satisfaction problems in computer science.MaxSAT is a special constraint satisfaction problem that will be mainly discussed in the thesis.MaxSAT problem is defined as follows: finding an assignment that maximizes the number of satisfied clause in a conjunctive normal form.It is a typical NP-hard problem which has great impact on theory and industry.There are two classes of algorithms for MaxSAT: complete algorithms and heuristic algorithms.We mainly discuss the kind of complete.A new algorithm called Iter_maxsatz which based on maxsatz is designed and implemented.Every possible solution must be considered is the greatest feature of complete algorithm.Branch-and-Bound(BnB)Max-SAT solvers use strategies like unit propagation,inference rules and failed literal detect to improve the value of lower bound which makes the algorithm more efficient.The original formula is divided into a number of subsets,and then algorithm maxsatz is called to solve every subset in Iter_maxsatz.The optimal solution of every subset is used to compute the upper value of satisfied clause on the node of search in maxsatz.And most importantly,the upper value can be compute in linear time and be used to decide whether it is necessary to search the subtree below the current node or backtrack to a higher level in the search tree.Benchmarks on the website of MaxSAT Evaluation are used to test the efficiency of the new algorithm.The results of the experiment show that Iter_maxsatz is a feasible and potential algorithm.