BREAKUP: a preprocessing algorithm for satisfiability testing of CNF formulas.
Robert H. Cowen, Katherine Wyatt · Notre Dame Journal of Formal Logic · 1993
An algorithm called BREAKUP, which processes CNF formulas by separating them into "connected components," is introduced.BREAKUP is then used to speed up the testing of some first-order formulas for satisfiability using Iwama's IS Algorithm.The complexity of this algorithm is shown to be on the order of O(nc-nv), where nc is the number of clauses and nv is the number of variables.