BREAKUP: A preprocessing algorithm for satisfiability testing of CNF formulas An algorithm called BREAKUP, which processes CNF formulas by separating them into “connected components”, is introduced. BREAKUP is then used to seed up the testing of some first-order formulas for satisfiability using Iwama’s 𝐈𝐒 Algorithm. The complexity of this algorithm is shown to be of the order of O(nc·nv), where nc is the number of clauses and nv is the number of variables.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Amir, Eyal; McIlraith, Sheila: Partition-based logical reasoning for first-order and propositional theories (2005)
- Amir, Eyal; McIlraith, Sheila: Improving the efficiency of reasoning through structure-based reformulation (2000)
- Chirkova, Rada; Genesereth, R.: Linearly bounded reformulations of unary databases (2000)
- Cowen, Robert; Wyatt, Katherine: BREAKUP: A preprocessing algorithm for satisfiability testing of CNF formulas (1993)