Using Symmetries to Lift Satisfiability Checking

TL;DR

This paper introduces a novel symmetry-based method to compress structures for satisfiability checking, enabling faster solutions in complex logical problems through a two-step translation and verification process.

Contribution

It proposes a new two-step approach using symmetry to compress structures and verify satisfiability more efficiently, with a practical translation for typed first-order logic with aggregates.

Findings

Large speedups in generative configuration problems

Effective translation for typed first-order logic with aggregates

Potential applications in software verification

Abstract

We analyze how symmetries can be used to compress structures (also known as interpretations) onto a smaller domain without loss of information. This analysis suggests the possibility to solve satisfiability problems in the compressed domain for better performance. Thus, we propose a 2-step novel method: (i) the sentence to be satisfied is automatically translated into an equisatisfiable sentence over a ``lifted'' vocabulary that allows domain compression; (ii) satisfiability of the lifted sentence is checked by growing the (initially unknown) compressed domain until a satisfying structure is found. The key issue is to ensure that this satisfying structure can always be expanded into an uncompressed structure that satisfies the original sentence to be satisfied. We present an adequate translation for sentences in typed first-order logic extended with aggregates. Our experimental evaluation shows large speedups for generative configuration problems. The method also has applications in the verification of software operating on complex data structures. Our results justify further research in automatic translation of sentences for symmetry reduction.