# Implicit State and Goals in QBF Encodings for Positional Games (extended version)

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 26 references that are in the map.
- First posted on arXiv 18 Jan 2023.

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

- [DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL](https://mlsanity.com/paper/1702.08256/) (2017)
- [Classical Planning as QBF without Grounding (extended version)](https://mlsanity.com/paper/2106.10138/) (2021)
- [Solving QBF by Abstraction](https://mlsanity.com/paper/1604.06752/) (2016)
- [QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties](https://mlsanity.com/paper/1904.12927/) (2019)
- [On the Complexity of Connection Games](https://mlsanity.com/paper/1605.04715/) (2016)
- [QFUN: Towards Machine Learning in QBF](https://mlsanity.com/paper/1710.02198/) (2017)

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

- [Concise QBF Encodings for Games on a Grid (extended version)](https://mlsanity.com/paper/2303.16949/) (2023)

## Abstract (arXiv)

We address two bottlenecks for concise QBF encodings of maker-breaker positional games, like Hex and Tic-Tac-Toe. Our baseline is a QBF encoding with explicit variables for board positions and an explicit representation of winning configurations. The first improvement is inspired by lifted planning and avoids variables for explicit board positions, introducing a universal quantifier representing a symbolic board state. The second improvement represents the winning configurations implicitly, exploiting their structure. The paper evaluates the size of several encodings, depending on board size and game depth. It also reports the performance of QBF solvers on these encodings. We evaluate the techniques on Hex instances and also apply them to Harary's Tic-Tac-Toe. In particular, we study scalability to 19×19 boards, played in human Hex tournaments.