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.

翻译：本文提出了一种从皮尔士存在图推理规则与蕴含图推导出的命题逻辑新型简化演算。我们的规则可应用于嵌套形式的命题逻辑公式，具有等价保持性，能保证变量、子句和文字数量单调递减，并最大化保留问题的结构信息。该技术亦可视为更高层次的SAT预处理方法，我们展示了其中一条规则（TWSR）如何泛化并优化了大多数已知的等价保持型SAT预处理方法。此外，我们提出基于两条核心规则（EPR与TWSR）系统化应用的简化流程，该流程与求解器无关，可用于简化任意形式的大型布尔可满足性问题及命题公式，并对其算法复杂度进行了时空维度的形式化分析。最后，我们通过新型n元蕴含图进一步扩展了规则体系，使其能够涵盖所有已知的等价保持型预处理过程。