Research On The Exact Satisfiability Problem(XSAT)

The Satisfiability problem(SAT)is among the most important problems in computer science.Satisfiability plays an important role on computer science and study of computation intractable problems.In the industrial scene,SAT is fundamental in solving problems in a large area.Many practical applications could be reducted to an instance of satisfiability problem.SAT is also the first problem proved to be NP-complete.Unless P=NP,we couldn’t solve it in polynominal time.People tend to find an NP-complete problem with easier format to solve it with less time complexity when it comes to practical use.Exact satisfiability problem(XSAT)is a special case of general satisfiability problem which regulates number of satisfied literals in every clause of the formula.Most of researches about XSAT focus on parameterized algorithms on number of variables 9).In the past studies,resolution cannot guarantee always solving the XSAT problem efficiently because it might significantly increase the size of the instance.The main point of thesis is as follows:(1)We analyzed current best algorithms on XSAT in the aspect of variables with pending measure.By using Measure and Conquer method,we analyzed all the branch factors causing by variables with pending measure,then calculate it with our algorithm in the end.(2)We proved correctness and completeness of resolution on XSAT in general.It is proved in thesis that size of an XSAT instance couldn’t grow indefinitely,thus resolution can be used anytime whenever it is applicable.It is also proved in thesis that XSAT problem with every variables showing at most 2 times in the instance could be solved in polynominal time.We give a detailed algorithm to solve this case which is not presented in previous research.(3)We spotted some cases which weren’t studied in the traditional algorithm analysis and proved that they could be solved efficiently.For example,two clauses sharing at least 4variables,a variable with deg()≥ 3 showing at 3-clause,etc.For Linearly normalized formulas,it is proved that it could be solved efficiently when there is a variable with deg()≥ 4.