UNIQUE SATISFIABILITY OF HORN SETS CAN BE SOLVED IN NEARLY LINEAR-TIME

被引：2

作者：

BERMAN, KA ^{[1
]}

FRANCO, J ^{[1
]}

SCHLIPF, JS ^{[1
]}

机构：

[1] UNIV CINCINNATI,DEPT COMP SCI,CINCINNATI,OH 45221

来源：

DISCRETE APPLIED MATHEMATICS | 1995年 / 60卷 / 1-3期

基金：

美国国家科学基金会;

关键词：

D O I：

10.1016/0166-218X(94)00043-D

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

If a Horn set I has a single satisfying truth assignment or model then that model is said to be unique for I. The question of determining whether a unique model exists for a given Horn set I is shown to be solved in O(alpha(L)*L) time, where L is the sum of the lengths of the clauses in I and alpha is the inverse Ackermann function. It is also shown that if L greater than or equal to A*log(A) where A is the number of distinct proposition letters then unique satisfiability can be determined in O(L) time.

引用

页码：77 / 91

页数：15

共 34 条

[21] Linear-time algorithms for counting independent sets in bipartite permutation graphs
Lin, Min-Sheng
Chen, Chien-Min
INFORMATION PROCESSING LETTERS, 2017, 122 : 1 - 7
[22] LTUR - A SIMPLIFIED LINEAR-TIME UNIT RESOLUTION ALGORITHM FOR HORN FORMULAS AND COMPUTER IMPLEMENTATION
MINOUX, M
INFORMATION PROCESSING LETTERS, 1988, 29 (01) : 1 - 12
[23] Nearly linear-time packing and covering LP solversAchieving width-independence and -convergence
Zeyuan Allen-Zhu
Lorenzo Orecchia
Mathematical Programming, 2019, 175 : 307 - 353
[24] Nearly linear-time packing and covering LP solvers: Achieving width-independence and -convergence
Allen-Zhu, Zeyuan
Orecchia, Lorenzo
MATHEMATICAL PROGRAMMING, 2019, 175 (1-2) : 307 - 353
[25] Simple linear-time algorithms for counting independent sets in distance-hereditary graphs
Lin, Min-Sheng
DISCRETE APPLIED MATHEMATICS, 2018, 239 : 144 - 153
[26] A nearly linear-time general algorithm for genome-wide bi-allele haplotype phasing
Casey, W
Mishra, B
HIGH PERFORMANCE COMPUTING - HIPC 2003, 2003, 2913 : 204 - 215
[27] BIN PACKING CAN BE SOLVED WITHIN 1+ETA IN LINEAR TIME
DELAVEGA, WF
LUEKER, GS
COMBINATORICA, 1981, 1 (04) : 349 - 355
[28] K-sets+: a Linear-time Clustering Algorithm for Data Points with a Sparse Similarity Measure
Chang, Cheng-Shang
Chang, Chia-Tai
Lee, Duan-Shin
Liou, Li-Heng
2017 IEEE SMARTWORLD, UBIQUITOUS INTELLIGENCE & COMPUTING, ADVANCED & TRUSTED COMPUTED, SCALABLE COMPUTING & COMMUNICATIONS, CLOUD & BIG DATA COMPUTING, INTERNET OF PEOPLE AND SMART CITY INNOVATION (SMARTWORLD/SCALCOM/UIC/ATC/CBDCOM/IOP/SCI), 2017,
[29] A LINEAR-TIME ALGORITHM TO CONSTRUCT A RECTILINEAR STEINER MINIMAL TREE FOR K-EXTREMAL POINT SETS
RICHARDS, DS
SALOWE, JS
ALGORITHMICA, 1992, 7 (2-3) : 247 - 276
[30] Linear-time algorithm for computing minimum checkpoint sets for simulation-based verification of HDL programs
Dubrova, E
2005 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS (ISCAS), VOLS 1-6, CONFERENCE PROCEEDINGS, 2005, : 2212 - 2215

← 1 2 3 4 →