### Abstract

In 1980, Monien and Speckenmeyer and (independently) Dantsin proved that the satisfiability of a propositional formula in CNF can be checked in less than 2^{N} steps (N is the number of variables). Later, many other upper bounds for SAT and its subproblems were proved. A formula in CNF is in CNF- (1, ∞) if each positive literal occurs in it at most once. In 1984, Luckhardt studied formulas in CNF-(1, ∞). In this paper, we prove several a new upper bounds for formulas in CNF-(l.∞) by introducing new signs separation principle. Namely, we present algorithms working in time of order 1.1939^{K} and 1.0644^{L} for a formula consisting of K clauses containing L literal occurrences. We also present an algorithm for formulas in CNF-(1, ∞) whose clauses are bounded in length.

Original language | English |
---|---|

Pages (from-to) | 442-463 |

Number of pages | 22 |

Journal | Journal of Mathematical Sciences |

Volume | 98 |

Issue number | 4 |

DOIs | |

Publication status | Published - 1 Jan 2000 |

### Scopus subject areas

- Statistics and Probability
- Mathematics(all)
- Applied Mathematics