A novel EGs-based framework for systematic propositional-formula simplification

Jordina Francès de Mas*, Juliana Kuster Filipe Bowles

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation
Subtitle of host publication33rd International Symposium, LOPSTR 2023, Cascais, Portugal, October 23-24, 2023, Proceedings
EditorsRobert Glück, Bishoksan Kafle
PublisherSpringer
Pages169-187
Number of pages18
Volume14330
ISBN (Electronic)9783031457845
ISBN (Print)9783031457838
DOIs
Publication statusPublished - 2023
Event33rd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2023) - Lisbon, Portugal
Duration: 23 Oct 202324 Oct 2023
Conference number: 33
https://lopstr.github.io/2023/#page-top

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume14330
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference33rd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2023)
Abbreviated titleLOPSTR 2023
Country/TerritoryPortugal
CityLisbon
Period23/10/2324/10/23
Internet address

Keywords

  • Simplification
  • Existential graphs
  • Equivalence-preserving preprocessing
  • Propositional satisfiability
  • Diagrammatic reasoning
  • Knowledge representation
  • Implication graphs
  • Hypergraphs

Fingerprint

Dive into the research topics of 'A novel EGs-based framework for systematic propositional-formula simplification'. Together they form a unique fingerprint.

Cite this