# Interactive configurator with FO(.) and IDP-Z3

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 49 references that are in the map.
- First posted on arXiv 1 Feb 2022.

## Builds on (most cited first, 3 of 3)

- [Multi-shot ASP solving with clingo](https://mlsanity.com/paper/1705.09811/) (2017)
- [ASP-Core-2 Input Language Format](https://mlsanity.com/paper/1911.04326/) (2019)
- [Predicate Logic as a Modelling Language: The IDP System](https://mlsanity.com/paper/1401.6312/) (2014)

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

- [VERUS-LM: a Versatile Framework for Combining LLMs with Symbolic Reasoning](https://mlsanity.com/paper/2501.14540/) (2025)
- [A Neurosymbolic Approach to Natural Language Formalization and Verification](https://mlsanity.com/paper/2511.09008/) (2025)

## Abstract (arXiv)

Industry abounds with interactive configuration problems, i.e., constraint solving problems interactively solved by persons with the assistance of a computer. The computer program, called a configurator, needs to perform a variety of reasoning tasks with the (often incomplete) information that the user provides. Imperative programming approaches make such systems difficult to implement and maintain. Knowledge-based configurators have been proposed to help engineers solve such problems, but many challenges remain. We present IDP-Z3, a new reasoning engine for the FO(.) KR language, and we report on its use for building configurators automatically from a knowledge base.