Efficiently grounding FOL using bit vectors

TL;DR

This paper explores using bit vectors to efficiently simplify first-order logic formulas during grounding, leveraging fast hardware operations, with experimental results showing both advantages and limitations.

Contribution

It introduces a novel approach of applying bit vectors for formula simplification in grounding, improving efficiency on modern hardware.

Findings

Bit vectors can speed up formula simplification for certain problems.

There are notable limitations of bit vectors in some cases.

Experimental analysis demonstrates the practical benefits and constraints.

Abstract

Several paradigms for declarative problem solving start from a specification in a high-level language, which is then transformed to a low-level language, such as SAT or SMT. Often, this transformation includes a "grounding" step to remove first-order quantification. To reduce the time and size of the grounding, it can be useful to simplify formulas along the way, e.g., by already taking into account the interpretation of symbols that are already known. In this paper, we investigate the use of bit vectors to efficiently simplify formulas, thereby taking advantage of the fact that, on modern hardware, logical operations on bit vectors can be executed extremely fast. We conduct an experimental analysis, which shows that bit vectors are indeed fast for certain problems, but also have limitations.