Traditionally, the satisfiability problem for propositional logics deals with formulas in Conjunctive Normal Form (CNF). A typical way to deal with non-CNF formulas requires (i) converting them into CNF, and (ii) applying solvers usually based on the Davis-Putnam (DP) procedure. A well known problem of this solution is that the CNF conversion may introduce many new variables, thus greatly widening the space of assignments in which the DP procedure has to search in order to find solutions. In this paper we present two variants of the DP procedure which overcome the problem outlined above. The idea underlying these variants is that splitting should occur only for the variables in the original formula. The CNF conversion methods employed ensure their correctness and completeness. As a consequence, we get two decision procedures for non-CNF formulas (i) which can exploit all the present and future sophisticated technology of current DP implementations, and (ii) whose space of assignments they have to search in, is limited in size by the number of variables in the original input formula. The preliminary analysis reported in [14] shows that these ideas can lead to a significant speed up of the search procedure
Applying the Davis-Putnam procedure to non-clausal formulas
Sebastiani, Roberto
1999-01-01
Abstract
Traditionally, the satisfiability problem for propositional logics deals with formulas in Conjunctive Normal Form (CNF). A typical way to deal with non-CNF formulas requires (i) converting them into CNF, and (ii) applying solvers usually based on the Davis-Putnam (DP) procedure. A well known problem of this solution is that the CNF conversion may introduce many new variables, thus greatly widening the space of assignments in which the DP procedure has to search in order to find solutions. In this paper we present two variants of the DP procedure which overcome the problem outlined above. The idea underlying these variants is that splitting should occur only for the variables in the original formula. The CNF conversion methods employed ensure their correctness and completeness. As a consequence, we get two decision procedures for non-CNF formulas (i) which can exploit all the present and future sophisticated technology of current DP implementations, and (ii) whose space of assignments they have to search in, is limited in size by the number of variables in the original input formula. The preliminary analysis reported in [14] shows that these ideas can lead to a significant speed up of the search procedureI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
