×

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
Software:
BREAKUP
PDF BibTeX XML Cite
Full Text: DOI