On 2-SAT and renamable horn

被引：0

作者：

del Val, A ^{[1
]}

机构：

[1] Univ Autonoma Madrid, ETS Informat, Madrid, Spain

来源：

SEVENTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-2001) / TWELFTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-2000) | 2000年

关键词：

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We introduce new linear time algorithms for satisfiability of binary propositional theories (2-SAT), and for recognition and satisfiability of renamable Horn theories. The algorithms are based on unit resolution, and are thus likely easier to integrate within general SAT solvers than other graph-based algorithms.

引用

页码：279 / 284

页数：6

共 13 条

[1]

[Anonymous], 1993, BUILDING PROBLEM SOL

[2] LINEAR-TIME ALGORITHM FOR TESTING THE TRUTH OF CERTAIN QUANTIFIED BOOLEAN FORMULAS [J].