Abstract
The formal verification problem is strongly correlated with the SAT and the QSAT problems. One approach in solving SAT and QSAT problems is based on using ZDD (Zero-Suppressed BDD) which is a variant of BDD (Binary Decision Diagram). When working with clauses, very often a big number of clauses are subsumed by other clauses. In such situation one may remove the subsumed clauses to simplify the formula. In this paper we reintroduce an operator for removing subsumed clauses, then we show how removing subsumed clauses may affect the efficiency of ZUNFOLD which is our 'Unfolding' based QSAT solver. © 2008 Springer-Verlag.
Author supplied keywords
Cite
CITATION STYLE
Ghasemzadeh, M., & Meinel, C. (2008). An operator for removal of subsumed clauses. In Communications in Computer and Information Science (Vol. 6 CCIS, pp. 714–717). https://doi.org/10.1007/978-3-540-89985-3_87
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
