On subsumption removal and on-the-fly CNF simplification

被引：0
|
作者：
Zhang, LT [1 ]
机构：
[1] Microsoft Res Silicon Valley Lab, Sunnyvale, CA 94043 USA
来源：
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS | 2005年 / 3569卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
CNF Boolean formulas generated from resolution or solution enumeration often have much redundancy. Efficient algorithms are needed to simplify and compact such CNF formulas. In this paper, we present a novel algorithm to maintain a subsumption-free CNF clause database by efficiently detecting and removing subsumption as the clauses are being added. We then present an algorithm that compact CNF formula further by applying resolutions to make it Decremental Resolution Free. Our experimental evaluations show that these algorithms are efficient and effective in practice.
引用
收藏
页码：482 / 489
页数：8
相关论文
共 50 条
  • [1] On-the-fly simplification of genetic programming models
    Javed, Noman
    Gobet, Fernand
    36TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, SAC 2021, 2021, : 464 - 471
  • [2] On-The-Fly Lazy Clause Simplification based on Binary Resolvents
    Nabeshima, Hidetomo
    Iwanuma, Koji
    Inoue, Katsumi
    2013 IEEE 25TH INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI), 2013, : 987 - 995
  • [3] On-the-Fly Monitoring of the Capture and Removal of Nanoplastics with Nanorobots
    Velikov, Dean I.
    Jancik-Prochazkova, Anna
    Pumera, Martin
    ACS NANOSCIENCE AU, 2024, 4 (04): : 243 - 249
  • [4] On-the-fly training
    Melenchón, J
    Meler, L
    Iriondo, I
    ARTICULATED MOTION AND DEFORMABLE OBJECTS, PROCEEDINGS, 2004, 3179 : 146 - 153
  • [5] ON-THE-FLY ROUNDING
    ERCEGOVAC, MD
    LANG, T
    IEEE TRANSACTIONS ON COMPUTERS, 1992, 41 (12) : 1497 - 1503
  • [6] On-the-Fly Macros
    Chen, Hubie
    Gimenez, Omer
    LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, 2009, 5514 : 155 - +
  • [7] On-the-fly simplification of large iso-surfaces with per-cube vertex modifiability detection
    Hou, Tao
    Chen, Li
    JOURNAL OF VISUALIZATION, 2016, 19 (04) : 715 - 726
  • [8] On-the-fly simplification of large iso-surfaces with per-cube vertex modifiability detection
    Tao Hou
    Li Chen
    Journal of Visualization, 2016, 19 : 715 - 726
  • [9] CNF formula simplification using implication reasoning
    Arora, R
    Hsiao, MS
    NINTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2004, : 129 - 134
  • [10] ON-THE-FLY DISK COMPRESSION
    NANCE, B
    BYTE, 1992, 17 (06): : 357 - 357
12345