This repository contains code for solving and experimenting with variants of the Optimal Observability Problem (OOP), with a focus on bounded-memory formulations solved with Z3.
This repository is organized into subprojects with their own documentation.
- Current bounded-memory workflow: bounded_memory/README.md
- Legacy artifact and paper reproduction materials: previous_work/README.md