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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Small Uniquely Satisfiable Patterns

  • Uroš Čibej

摘要

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.