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.