On Subsumption Removal and On-the-Fly CNF Simplification Export

@incollection{zsat05, abstract = {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.}, author = {Zhang, Lintao}, citeulike-article-id = {6032394}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/11499107_42}, citeulike-linkout-1 = {http://www.springerlink.com/content/gbv2hdluwxh2qe1v}, doi = {10.1007/11499107_42}, journal = {Theory and Applications of Satisfiability Testing}, keywords = {cnf, resolution, subsumption}, pages = {482--489}, posted-at = {2009-10-29 14:47:35}, priority = {2}, title = {On Subsumption Removal and On-the-Fly CNF Simplification}, url = {http://dx.doi.org/10.1007/11499107_42}, year = {2005} }

TY - CHAP ID - zsat05 L3 - citeulike-article-id:6032394 N2 - 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. JF - Theory and Applications of Satisfiability Testing EP - 489 TI - On Subsumption Removal and On-the-Fly CNF Simplification SP - 482 KW - cnf KW - resolution KW - subsumption AU - Zhang, Lintao PY - 2005/// UR - http://dx.doi.org/10.1007/11499107_42 ER -