Standard

Two new upper bounds for SAT. / Hirsch, Edward A.

1998. 521-530 Paper presented at Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms, San Francisco, CA, USA.

Research output: Contribution to conference › Paper › peer-review

Harvard

Hirsch, EA 1998, 'Two new upper bounds for SAT', Paper presented at Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms, San Francisco, CA, USA, 25/01/98 - 27/01/98 pp. 521-530.

APA

Hirsch, E. A. (1998). Two new upper bounds for SAT. 521-530. Paper presented at Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms, San Francisco, CA, USA.

Vancouver

Hirsch EA. Two new upper bounds for SAT. 1998. Paper presented at Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms, San Francisco, CA, USA.

Author

Hirsch, Edward A. / Two new upper bounds for SAT. Paper presented at Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms, San Francisco, CA, USA.10 p.

BibTeX

@conference{d33eb66fe6a547e897986e849367cc2f,
title = "Two new upper bounds for SAT",
abstract = "In 1980 B. Monien and E. Speckenmeyer proved that satisfiability of a propositional formula consisting of K clauses can be checked in time of the order 2K/3. Recently O. Kullmann and H. Luckhardt proved the bound 2L/9, where L is the length of the input formula. The algorithms leading to these bounds (like many other SAT algorithms) are based on splitting, i.e., they reduce SAT for a formula F to SAT for several simpler formulas F1, F2, ..., Fm. These algorithms simplify each of F1, F2, ..., Fm according to some transformation rules such as the elimination of pure literals, the unit propagation rule etc. In this paper we present a new transformation rule and two algorithms using this rule. These algorithms have the bounds 20.30897 K and 20.10537 L respectively.",
author = "Hirsch, {Edward A.}",
year = "1998",
month = dec,
day = "1",
language = "English",
pages = "521--530",
note = "Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms ; Conference date: 25-01-1998 Through 27-01-1998",

}

RIS

TY - CONF

T1 - Two new upper bounds for SAT

AU - Hirsch, Edward A.

PY - 1998/12/1

Y1 - 1998/12/1

N2 - In 1980 B. Monien and E. Speckenmeyer proved that satisfiability of a propositional formula consisting of K clauses can be checked in time of the order 2K/3. Recently O. Kullmann and H. Luckhardt proved the bound 2L/9, where L is the length of the input formula. The algorithms leading to these bounds (like many other SAT algorithms) are based on splitting, i.e., they reduce SAT for a formula F to SAT for several simpler formulas F1, F2, ..., Fm. These algorithms simplify each of F1, F2, ..., Fm according to some transformation rules such as the elimination of pure literals, the unit propagation rule etc. In this paper we present a new transformation rule and two algorithms using this rule. These algorithms have the bounds 20.30897 K and 20.10537 L respectively.

AB - In 1980 B. Monien and E. Speckenmeyer proved that satisfiability of a propositional formula consisting of K clauses can be checked in time of the order 2K/3. Recently O. Kullmann and H. Luckhardt proved the bound 2L/9, where L is the length of the input formula. The algorithms leading to these bounds (like many other SAT algorithms) are based on splitting, i.e., they reduce SAT for a formula F to SAT for several simpler formulas F1, F2, ..., Fm. These algorithms simplify each of F1, F2, ..., Fm according to some transformation rules such as the elimination of pure literals, the unit propagation rule etc. In this paper we present a new transformation rule and two algorithms using this rule. These algorithms have the bounds 20.30897 K and 20.10537 L respectively.

UR - http://www.scopus.com/inward/record.url?scp=0032284428&partnerID=8YFLogxK

M3 - Paper

AN - SCOPUS:0032284428

SP - 521

EP - 530

T2 - Proceedings of the 1998 9th Annual ACM SIAM Symposium on Discrete Algorithms

Y2 - 25 January 1998 through 27 January 1998

ER -

ID: 49830187