Small Uniquely Satisfiable Patterns.

Satisfiability (SAT) is a fundamental problem in computer science. This paper investigates a specific subclass of satisfiable expressions: those with a unique satisfying assignment (USAT). We introduce the concept of minimal USAT patterns — graph structures that represent USAT expressions which cease to be USAT if any clause is removed. We outline a method for identifying and cataloguing these patterns, present empirical findings from a database of them, and examine their practical applications. Finding these minimal patterns in larger SAT instances can serve multiple purposes, such as a preprocessing step to simplify the problem, a generalisation of a unit clause during the execution of a SAT solver, or as a distinctive feature in classifying SAT instances.