Resumen de A proof procedure for regular CNF-formulas

Felip Manyà Serres , Gonzalo Escalada Imaz

• In this paper we deal with the propositional satisfiability problem for a kind of multiple-valued clausal forms known as regular cnf-formulas. We present a Davis-Putnam-style satisfiability checking procedure for regular cnf-formulas and prove its completeness. Then, we propose improved regular branching rule is applied and some deletion strategies for eliminating irrelevant or redundant clauses.