A Structure-Preserving Clause Form Translation

By D. Plaisted, Steven Greenbaum. 1986

Most resolution theorem provers convert a theorem into clause form before attempting to find a proof. The conventional translation of a first-order formula into clause form often obscures the structure of the formula, and may increase the length of the formula by an exponential amount in the worst case. We present a non-standard clause form translation that preserves more of the structure of the formula than the conventional translation. This new translation also avoids the exponential increase in size which may occur with the standard translation. We show how this idea may be combined with the idea of replacing predicates by their definitions before converting to clause form. We give a method of lock resolution which is appropriate for the non-standard clause form translation, and which has yielded a spectacular reduction in search space and time for one example. These techniques should increase the attractiveness of resolution theorem provers for program verification applications, since the theorems that arise in program verification are often simple but tedious for humans to prove.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Learning Optimal Decision Trees with SAT (2018, methodology): “Moreover, standard clausiﬁcation techniques are assumed [Plaisted and Greenbaum, 1986].”
Towards an Optimal CNF Encoding of Boolean Cardinality Constraints (2005, methodology): “This technique, that preserves satisfiability of the whole set of equivalences, was introduced by Tseitin [9] and was later re-invented and extended by different authors [10, 11, 7, 8].”
The Quest for Efficient Boolean Satisfiability Solvers (2002, background): “[24]) to transform any propositional formula into a CNF formula that has the same satisfiability as the original one.”
Semantic Matching: Algorithms and Implementation (2007, methodology): “In order to avoid the space explosion, which may arise when converting a formula into CNF (see for instance Eq. 28), we apply a set of structure preserving transformations [ 41 ,19].”
Understanding script-based stories using commonsense reasoning (2004, methodology): “(Happens(e, t) ∧ Initiates(e, f, t))⇒ HoldsAt(f, t+ 1).”
Bounded Model Checking Using Satisfiability Solving (2001, methodology): “To avoid the exponential explosion, we use a structure preserving clause form transformation [28].”
Hypertableau Reasoning for Description Logics (2009, background): “Normalization can be seen as a variant of the well-known structural transformation (Plaisted & Greenbaum, 1986; Nonnengart & Weidenbach, 2001).”
Interpolation and SAT-Based Model Checking (2003, background): “A suitable translation that is linear in the formula size can be found in [20].”
Efficient SAT-Based Encodings of Conditional Cardinality Constraints (2018, background): “Two decades later, after Tseitin’s seminal paper, Plaisted and Greenbaum presented an improved CNF translation that essentially produces a subset of Tseitin’s representation [14].”
Proof theory of many-valued logic—linear optimization—logic design: connections and interactions (1997, background): “In classical logic the growth at least of CNFs can be kept within polynomial bounds with so-called structure preserving CNF transformations [47, 32 ].”
Effective Preprocessing in SAT Through Variable and Clause Elimination (2005, methodology): “One way of speeding up SAT solving is to work on sophisticated CNF encoding algorithms such as [3,12,18,23].”
SAT-Based Encodings for Optimal Decision Trees with Explicit Paths (2020, methodology): “State-of-the-art SAT solvers typically accept input in CNF. Non-CNF formulas are converted to CNF by standard equisatisﬁable clausiﬁcation methods [31].”
An interpolating theorem prover (2005, background): “It is well known that satisfiability of an arbitrary formula f can be reduced in linear time to satisfiability of a clause form formula [11].”
HermiT: An OWL 2 Reasoner (2014, background): “, by removing duplicate or irrelevant conjuncts or disjuncts) and then converts the result into a particular normal form; the normalisation step can be seen as a variant of the well-known structural transformation [31, 32].”