Exact Algorithms For NP Hard Problems Based On Conflicts

Maximum Satisfiability(MaxSAT)problem,Maximum Clique(MC)problem and Maximum Common induced Subgraph(MCS)problem are classical NP Hard problems in computer science,also are claasic optimization problems in artificial intelligence and operations research.MaxSAT,MC and MCS are efficient models for real world problems.Designing the exact algorithms for them has a profound theoretical significance,as well as an important influence on the real world.The goals of MCS,MC and MaxSAT problems are different,but they can be induced to the conflicts solving.A conflict means that there is no sound solution to satisfy the given constraints.If there is at least one unsatisfied clause under any assignments,a conflict is found for MaxSAT problem.A conflict for MCS problem is that non-adjacent vertices can't build a clique.There is a conflict for MCS problem when the branch nodes make more vertices against the edge constraint and decrease the maximum number of matching vertex pairs.The methods of detecting clause conflict in MaxSAT problem can find the latent conflicts among the vertices of MC problem and MCS problem.The more conflicts there are,the better the bounds of branch-and-bound(BnB)algorithms are.Based on the idea of finding more conflicts and improving the bounds of algorithms,we studied the above three typical NP hard problems,and designed efficient BnB exact algorithms.(1)We proposed three strategies based on optimizing inconsistent set to efficiently improve the lower bound of MaxSAT problem.Inference rules in priority first deal with the inconsistent sets which use the minimum clauses.Changing the order of unit clause propagates the unit clauses in descending order of their scores.The score of a unit clause is the occurring times of its negative literal in binary clauses.Further detecting failed literals expands the search scope in order to find a large inconsistent set.Maxsatz2013 adopted three optimization strategies and outperformed in the 2013 MaxSAT Evaluation,which is No.1 in random class and No.2 in crafted class.(2)We proposed a cycle breaking rule for MaxSAT problem in order to solve the complex cycle structure.It is to find a unit clause which has the same literal with the first implicated node,remove the cycle.The new clauses are n binary clauses not 2(n-2)ternary clauses.Experimental results show that Brmaxsat can solve 20 Max2 SAT instances more than the sate-of-the-art ahmaxsat-ls-1.55 algorithm,and reduce the average running time.(3)We proposed the weight cover and designed the partition function for MC problem.Tranditional methods of computing upper bound put focuse on the adjacent relationships of the vertices,and the weights of independent sets(ISs)are always fixed.A relax upper bound of the maximum weighted clique is found.Weight covering changes the weights of ISs,solves varied conflicts which the ISs cover the weights of the vertices,and reduces the branches.Experimental results show that WC-MWC based on weight covering is four times faster than WLMC on some instances,and faster than the sate-of-the-art heuristic algorithm FastWCLq on 78% instances.(4)We proposed a new branching strategy for MCS problem to find the best solution faster.The more less vertice pairs there are,the better the upper bound is.The algorithm learns from the past search and computes the conflicts with the decrease of the upper bound.The value function is designed to accumulate the rewards of vertices in the past research.The new branching strategy based on reinforcement learning chooses the vertices in decreasing order of the vertices scores,and breaks all ties with the maximum degree.For twenty-one thousand large subgraph isomorphism instances,McSplit+RL adopting the new branching strategy solves 130 unlablled instances more than the best MCS algorithm--McSplit.Based on the above studies,we see that finding the basic conflicts in NP hard problems will help us find the ways of solving conflicts and improve the efficiency of the exact algorithms.