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 arbitrary propositional logic formulae (not only in CNF), are equivalence-preserving, guarantee a monotonically decreasing number of 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. We further show how this rule can be extended with a novel n-ary implication graph to capture all known equivalence-preserving preprocessing procedures. Finally, we discuss the complexity and implementation of our framework as a solver-agnostic algorithm to simplify Boolean satisfiability problems and arbitrary propositional formula.
Original language | English |
---|---|
Title of host publication | Logic-Based Program Synthesis and Transformation |
Subtitle of host publication | 33rd International Symposium, LOPSTR 2023, Cascais, Portugal, October 23-24, 2023, Proceedings |
Editors | Robert Glück, Bishoksan Kafle |
Publisher | Springer |
Pages | 169-187 |
Number of pages | 18 |
Volume | 14330 |
ISBN (Electronic) | 9783031457845 |
ISBN (Print) | 9783031457838 |
DOIs | |
Publication status | Published - 2023 |
Event | 33rd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2023) - Lisbon, Portugal Duration: 23 Oct 2023 → 24 Oct 2023 Conference number: 33 https://lopstr.github.io/2023/#page-top |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 14330 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 33rd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2023) |
---|---|
Abbreviated title | LOPSTR 2023 |
Country/Territory | Portugal |
City | Lisbon |
Period | 23/10/23 → 24/10/23 |
Internet address |
Keywords
- Simplification
- Existential graphs
- Equivalence-preserving preprocessing
- Propositional satisfiability
- Diagrammatic reasoning
- Knowledge representation
- Implication graphs
- Hypergraphs