Efficiently grounding FOL using bit vectors
Lucas Van Laer, Simon Vandevelde, Joost Vennekens
TL;DR
The paper addresses grounding bottlenecks in ground-and-solve declarative systems by introducing a bit-vector grounded representation that leverages already-interpreted symbols to reduce the size of the ground formula, formalized via $FO(\cdot)$ and Model Expansion $MX(\phi,S_0)$. It develops a framework for satisfying sets $[\phi :: \mathbf{x}]_S$ and demonstrates how to compose them using bitwise operations on bit-vectors, with multi-dimensional extensions and quantifier projection to support grounding reductions. A concrete Rust implementation, the SLI grounder, grounds FO$(\cdot)$ problems to SMT-LIB for Z3 and is evaluated on benchmarks showing competitive grounding times, with the bit-vector variants generally outperforming naive grounding except in highly sparse or triangle-graph scenarios. The work demonstrates the viability of satisfying-set-based grounding as a scalable alternative and discusses limitations and future directions, including compressed bitmaps for sparse data.
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.