The satisfiability problem is always a core problem in artificial intelligence and has been concerned for decades. Achievements in the research of the satisfiability problem have already been used in the research of other areas, such as computer aided design, database system. Now, there are many methods for the satisfiability problem, such as methods based on resolution, methods based on tableau, methods based on extension rule. By the study of extension rule, a conclusion can be drawn that the satisfiability of a clause set can be judged by the existence of a hitting set, which containing no complementary pairs of literals. With this conclusion, the algorithm CBHST (complementary binary hitting set tree) is designed. CBHST judge the existence of a hitting set without complementary pairs of literals in a binary tree. If the hitting set exists, CBHST will give the result that the clause set is satisfiable. Finally, CBHST is compared with an algorithm based on resolution DR and an algorithm based on extension rule IER. The test data shows that CBHST is efficient.
An Algorithm Based on Hitting Set for SAT Problem
01.10.2019
156917 byte
Aufsatz (Konferenz)
Elektronische Ressource
Englisch
Computing minimal hitting set based on immune genetic algorithm
Kraftfahrwesen | 2014
|Online Contents | 1996
Online Contents | 2005
Kraftfahrwesen | 2002
|