Heuristic 3-sat Into A 2-sat Dpll Algorithm

We study satisfiability problem to decide that whether there exists a truth assignment which can satisfy a given logical expression. Sat is very important to mathematical logic, artificial intelligence, computer algorithm design and analysis, engineering applications and other fields. SAT problem is the first problem which was proven NP-complete3SAT is a special satisfiability problem. It's clauses contain at most three literals. 3SAT is a NP-complete problem too. It can be abstracted from a lot of practical problems. 3SAT is widely applied to logical reasoning, artificial intelligence expert system, database maintenance and retrieval, VLSI design and test. People study it in-depth and in details due to its extensive application background.The solving algorithms of SAT are divided into complete algorithm and local search algorithm. The former mainly include methods of exhaustion, DPLL algorithm, and relaxation method. Representational algorithm of the latter is local search algorithm, such as GSAT. These algorithms decide the satisfiability of 3SAT directly. In this paper, we translate 3SAT into 2SAT instead of deciding the satisfiability of 3SAT directly. 2SAT can be decided in polynomial time. If 3SAT can be transformed into 2SAT in polynomial time, then the satisfiability of 3SAT can be decided in polynomial time either.In this paper, we combine heuristic strategy with DPLL algorithm and design algorithm which solves the problem rapidly. We first simplify the original formula by DP algorithm, then stat the positive appearance and negative appearance of the variable in formula, and choose resolution variables according to it. In this way, we can translate 3SAT into 2SAT rapidly. But this may bring contrary clauses. So we introduce a conflict resolution strategy to eliminate contrary clauses. We adopted a pre-detection method, that is, in each of the resolution process we search clauses which may bring conflict clauses. If conflict clauses are found, then we assign proper assignment to them to eliminate these clauses.