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 条
1234