A novel framework for systematic propositional formula simplification based on existential graphs

TL;DR

This paper introduces a new framework for simplifying propositional formulas using rules inspired by Peirce's existential graphs, which preserves equivalence, reduces complexity, and enhances SAT preprocessing.

Contribution

It presents a novel simplification calculus based on existential graph rules, including a solver-agnostic procedure and an extension with n-ary implication graphs for comprehensive preprocessing.

Findings

The proposed rules guarantee a decrease in variables, clauses, and literals.

The TWSR rule generalizes existing SAT preprocessing methods.

The simplification procedure is formalized with complexity analysis.

Abstract

This paper presents a novel simplification calculus for propositional logic derived from Peirce's existential graphs' rules of inference and implication graphs. Our rules can be applied to propositional logic formulae in nested form, are equivalence-preserving, guarantee a monotonically decreasing number of variables, clauses and literals, and maximise the preservation of structural problem information. Our techniques can also be seen as higher-level SAT preprocessing, and we show how one of our rules (TWSR) generalises and streamlines most of the known equivalence-preserving SAT preprocessing methods. In addition, we propose a simplification procedure based on the systematic application of two of our rules (EPR and TWSR) which is solver-agnostic and can be used to simplify large Boolean satisfiability problems and propositional formulae in arbitrary form, and we provide a formal analysis of its algorithmic complexity in terms of space and time. Finally, we show how our rules can be further extended with a novel n-ary implication graph to capture all known equivalence-preserving preprocessing procedures.