On k-positive satisfiability problem

Xiong Huang; Wei Li

doi:10.1007/BF02948732

On k-positive satisfiability problem

Xiong Huang
, Wei Li

School of Computer Science and Engineering

Beihang University

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

Abstract

An algorithm for solving the satisfiability problem is presented. It is proved that this algorithm solves 2-SAT and Horn-SAT in linear time and k-positive SAT (in which every clause contains at most k positive literals) in time O(|F| · ξ_kⁿ), where |F| is the length of input F, n is the number of atoms occurring in F, and ξ_k is the greatest real number satisfying the equation x = 2-1/x^k. Compared with previous results, this nontrivial upper bound on time complexity could only be obtained for k-SAT, which is a subproblem of k-positive SAT.

Original language	English
Pages (from-to)	309-313
Number of pages	5
Journal	Journal of Computer Science and Technology
Volume	14
Issue number	4
DOIs	https://doi.org/10.1007/BF02948732
State	Published - Jul 1999

Access to Document

10.1007/BF02948732

Cite this

@article{93f83f4eaf8e4c2ab1b9c481d44ab4b6,

title = "On k-positive satisfiability problem",

abstract = "An algorithm for solving the satisfiability problem is presented. It is proved that this algorithm solves 2-SAT and Horn-SAT in linear time and k-positive SAT (in which every clause contains at most k positive literals) in time O(|F| · ξkn), where |F| is the length of input F, n is the number of atoms occurring in F, and ξk is the greatest real number satisfying the equation x = 2-1/xk. Compared with previous results, this nontrivial upper bound on time complexity could only be obtained for k-SAT, which is a subproblem of k-positive SAT.",

author = "Xiong Huang and Wei Li",

year = "1999",

month = jul,

doi = "10.1007/BF02948732",

language = "英语",

volume = "14",

pages = "309--313",

journal = "Journal of Computer Science and Technology",

issn = "1000-9000",

publisher = "Springer New York",

number = "4",

}

TY - JOUR

T1 - On k-positive satisfiability problem

AU - Huang, Xiong

AU - Li, Wei

PY - 1999/7

Y1 - 1999/7

N2 - An algorithm for solving the satisfiability problem is presented. It is proved that this algorithm solves 2-SAT and Horn-SAT in linear time and k-positive SAT (in which every clause contains at most k positive literals) in time O(|F| · ξkn), where |F| is the length of input F, n is the number of atoms occurring in F, and ξk is the greatest real number satisfying the equation x = 2-1/xk. Compared with previous results, this nontrivial upper bound on time complexity could only be obtained for k-SAT, which is a subproblem of k-positive SAT.

AB - An algorithm for solving the satisfiability problem is presented. It is proved that this algorithm solves 2-SAT and Horn-SAT in linear time and k-positive SAT (in which every clause contains at most k positive literals) in time O(|F| · ξkn), where |F| is the length of input F, n is the number of atoms occurring in F, and ξk is the greatest real number satisfying the equation x = 2-1/xk. Compared with previous results, this nontrivial upper bound on time complexity could only be obtained for k-SAT, which is a subproblem of k-positive SAT.

UR - https://www.scopus.com/pages/publications/0032627579

U2 - 10.1007/BF02948732

DO - 10.1007/BF02948732

M3 - 文章

AN - SCOPUS:0032627579

SN - 1000-9000

VL - 14

SP - 309

EP - 313

JO - Journal of Computer Science and Technology

JF - Journal of Computer Science and Technology

IS - 4

ER -

On k-positive satisfiability problem

Abstract

Access to Document

Other files and links

Fingerprint

Cite this