Evaluating optimized decision procedures for propositional modal K(m) satisfiability

Ian Horrocks; Peter F. Patel-Schneider

doi:10.1023/A:1015063215934

Evaluating optimized decision procedures for propositional modal K(m) satisfiability

Ian Horrocks, Peter F. Patel-Schneider

Research output: Contribution to journal › Article › peer-review

Abstract

Heavily optimized decision procedures for propositional modal satisfiability are now becoming available. Two systems incorporating such procedures for modal K, DLP and KSATC, are tested on randomly generated CNF formulae with several sets of parameters, varying the maximum modal depth and ratio of propositional variable to modal subformulae. The results show some easy-hard-easy behavior, but there is as yet no sharp peak as in propositional satisfiability.

Original language	English
Pages (from-to)	173-204
Number of pages	31
Journal	Journal of Automated Reasoning
Volume	28
Issue number	2
DOIs	https://doi.org/10.1023/A:1015063215934
Publication status	Published - Feb 2002

Keywords

Optimization
Satisfiability
Tableaux

Access to Document

10.1023/A:1015063215934

Cite this

@article{f500b76ca06d4f7d8e1872a2e091653e,

title = "Evaluating optimized decision procedures for propositional modal K(m) satisfiability",

abstract = "Heavily optimized decision procedures for propositional modal satisfiability are now becoming available. Two systems incorporating such procedures for modal K, DLP and KSATC, are tested on randomly generated CNF formulae with several sets of parameters, varying the maximum modal depth and ratio of propositional variable to modal subformulae. The results show some easy-hard-easy behavior, but there is as yet no sharp peak as in propositional satisfiability.",

keywords = "Optimization, Satisfiability, Tableaux",

author = "Ian Horrocks and Patel-Schneider, {Peter F.}",

year = "2002",

month = feb,

doi = "10.1023/A:1015063215934",

language = "English",

volume = "28",

pages = "173--204",

journal = "Journal of Automated Reasoning",

issn = "1573-0670",

publisher = "Springer Nature",

number = "2",

}

TY - JOUR

T1 - Evaluating optimized decision procedures for propositional modal K(m) satisfiability

AU - Horrocks, Ian

AU - Patel-Schneider, Peter F.

PY - 2002/2

Y1 - 2002/2

N2 - Heavily optimized decision procedures for propositional modal satisfiability are now becoming available. Two systems incorporating such procedures for modal K, DLP and KSATC, are tested on randomly generated CNF formulae with several sets of parameters, varying the maximum modal depth and ratio of propositional variable to modal subformulae. The results show some easy-hard-easy behavior, but there is as yet no sharp peak as in propositional satisfiability.

AB - Heavily optimized decision procedures for propositional modal satisfiability are now becoming available. Two systems incorporating such procedures for modal K, DLP and KSATC, are tested on randomly generated CNF formulae with several sets of parameters, varying the maximum modal depth and ratio of propositional variable to modal subformulae. The results show some easy-hard-easy behavior, but there is as yet no sharp peak as in propositional satisfiability.

KW - Optimization

KW - Satisfiability

KW - Tableaux

U2 - 10.1023/A:1015063215934

DO - 10.1023/A:1015063215934

M3 - Article

SN - 1573-0670

VL - 28

SP - 173

EP - 204

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 2

ER -

Evaluating optimized decision procedures for propositional modal K(m) satisfiability

Abstract

Keywords

Access to Document

Fingerprint

Cite this