# zbMATH — the first resource for mathematics

BREAKUP: A preprocessing algorithm for satisfiability testing of CNF formulas. (English) Zbl 0795.03018
Summary: 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 $${\mathbf I}{\mathbf S}$$ Algorithm. The complexity of this algorithm is shown to be of the order of $$O(nc\cdot nv)$$, where $$nc$$ is the number of clauses and $$nv$$ is the number of variables.

##### MSC:
 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68Q25 Analysis of algorithms and problem complexity
BREAKUP
Full Text: