Random Formula Generators

TL;DR

This paper introduces three uniform random formula generators for propositional logic, capable of sampling formulae with specified depth and atomic sets, supported by cardinality proofs ensuring uniformity.

Contribution

It presents novel algorithms for generating propositional formulae uniformly at random with controlled depth and atomic inclusion, along with theoretical proofs of their uniformity.

Findings

Three generators for propositional formulae with specified parameters.

Proofs of uniformity based on cardinality results.

Generators can produce all formulae in their respective spaces with equal probability.

Abstract

In this article, we provide three generators of propositional formulae for arbitrary languages, which uniformly sample three different formulae spaces. They take the same three parameters as input, namely, a desired depth, a set of atomics and a set of logical constants (with specified arities). The first generator returns formulae of exactly the given depth, using all or some of the propositional letters. The second does the same but samples up-to the given depth. The third generator outputs formulae with exactly the desired depth and all the atomics in the set. To make the generators uniform (i.e. to make them return every formula in their space with the same probability), we will prove various cardinality results about those spaces.