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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    An Algorithm Based on Hitting Set for SAT Problem


    Contributors:
    Xu, Youjun (author) / Ma, Yingrui (author) / Li, Zi (author)


    Publication date :

    2019-10-01


    Size :

    156917 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Computing minimal hitting set based on immune genetic algorithm

    Zhou,G. / Feng,W. / Jiang,B. et al. | Automotive engineering | 2014


    Hitting home

    Online Contents | 1996


    BALL HITTING DEVICE

    KAWASAKI AKIMITSU / NAGAI TOMOHITO | European Patent Office | 2019

    Free access

    Hitting on target

    Online Contents | 2005


    Heavy hitting SUVs

    Mead,S. / General Motors,US / Ford Motor,US et al. | Automotive engineering | 2002