Papers › Interactive configurator with FO(.) and IDP-Z3

Interactive configurator with FO(.) and IDP-Z3

1 Feb 2022arXiv:2202.00343archive 2025-07-28

Pierre Carbonnelle, Simon Vandevelde, Joost Vennekens, Marc Denecker

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.

PaperPDFCode

In Syntology Open this paper in Syntology's Atlas, the map of the papers in Syntology's graph and their citations.

Code

gitlab.com/krr/idp-z3 officialmentioned in paper report

Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.

Code Syntology ran Syntology

Not run by Syntology. Nothing on this page verifies that the listed code works.

Results from the paper archive 2025-07-28

No leaderboard rows for this paper in the archive.

Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections