On subsumption removal and on-the-fly CNF simplification
In: Theory and applications of satisfiability testing (St Andrews, 19-23 June 2005)Lecture notes in computer science :482-489
Konferenz
- print, 12 ref
Zugriff:
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.
Titel: |
On subsumption removal and on-the-fly CNF simplification
|
---|---|
Autor/in / Beteiligte Person: | LINTAO, ZHANG |
Link: | |
Quelle: | Theory and applications of satisfiability testing (St Andrews, 19-23 June 2005)Lecture notes in computer science :482-489 |
Veröffentlichung: | Berlin: Springer, 2005 |
Medientyp: | Konferenz |
Umfang: | print, 12 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|