# Skolem Functions for Factored Formulas

arXiv: https://arxiv.org/abs/1508.05497 · HTML: https://mlsanity.com/paper/1508.05497/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Aug 2015.

## Built on by (most cited first, 4 of 4)

- [Engineering an Efficient Boolean Functional Synthesis Engine](https://mlsanity.com/paper/2108.05717/) (2021)
- [A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis](https://mlsanity.com/paper/2104.14098/) (2021)
- [Synthesis with Explicit Dependencies](https://mlsanity.com/paper/2301.10556/) (2023)
- [Presburger Functional Synthesis: Complexity and Tractable Normal Forms](https://mlsanity.com/paper/2508.07207/) (2025)

## Abstract (arXiv)

Given a propositional formula F(x,y), a Skolem function for x is a function Psi(y), such that substituting Psi(y) for x in F gives a formula semantically equivalent to exists F. Automatically generating Skolem functions is of significant interest in several applications including certified QBF solving, finding strategies of players in games, synthesising circuits and bit-vector programs from specifications, disjunctive decomposition of sequential circuits etc. In many such applications, F is given as a conjunction of factors, each of which depends on a small subset of variables. Existing algorithms for Skolem function generation ignore any such factored form and treat F as a monolithic function. This presents scalability hurdles in medium to large problem instances. In this paper, we argue that exploiting the factored form of F can give significant performance improvements in practice when computing Skolem functions. We present a new CEGAR style algorithm for generating Skolem functions from factored propositional formulas. In contrast to earlier work, our algorithm neither requires a proof of QBF satisfiability nor uses composition of monolithic conjunctions of factors. We show experimentally that our algorithm generates smaller Skolem functions and outperforms state-of-the-art approaches on several large benchmarks.