Compact normal forms in propositional logic and integer programming formulations

An alternative linear time algorithm for achieving a clausal form equivalent to a given logical proposition is developed. The two algorithms are compared on a set of test problems and savings in computation are demonstrated. The style of the revised algorithm suggests a natural compact representation of logical propositions as integer programming inequalities and this representation is developed. Other elaborations of connections between logical propositions and mixed integer programming are developed involving conjunctive representations.