Constructing Optimal Kobon Triangle Arrangements via Table Encoding, SAT Solving, and Heuristic Straightening

TL;DR

This paper introduces innovative methods combining table encoding, SAT solving, and heuristics to construct and verify optimal Kobon triangle arrangements, achieving new solutions for 23 and 27 lines.

Contribution

It presents a novel compact table notation, heuristic recovery tools, and a SAT-based approach to find and verify optimal Kobon arrangements, including previously unknown solutions.

Findings

Successfully recovered arrangements for many known optimal solutions.

Discovered new optimal arrangements for 23 and 27 lines.

Confirmed the non-existence of solutions in certain cases using SAT solving.

Abstract

We present new methods and results for constructing optimal Kobon triangle arrangements. First, we introduce a compact table notation for describing arrangements of pseudolines, enabling the representation and analysis of complex cases, including symmetrical arrangements, arrangements with parallel lines, and arrangements with multiple-line intersection points. Building on this, we provide a simple heuristic method and tools for recovering straight-line arrangements from a given table, with the ability to enforce additional properties such as symmetries. The tool successfully recovers arrangements for many previously known optimal solutions. Additionally, we develop a tool that transforms the search for optimal Kobon arrangement tables into a SAT problem, allowing us to leverage modern SAT solvers (specifically Kissat) to efficiently find new solutions or to show that no other solutions exist (for example, confirming that no optimal solution exists in the 11-line case). Using these techniques, we find new optimal Kobon arrangements for 23 and 27 lines, along with several other new results.