Logical Redundancy in Random k-SAT Problems

Scott Clark, Cornell University

Photo of Scott Clark

Recently there has been a considerable amount of interest in random satisfiability problems both from an experimental and a theoretical point of view. The traditional way to generate random k-SAT instances involves sampling constraints from a distribution which allows for clauses to be redundant; they logically do not change the system in any way. While this is a rare event, it becomes much more likely when systems are nearly unsatisfiable, the system approaching a critical ratio between clauses and variables.

This work explores how these logically redundant clauses play a role in influencing the statistics of the largely experimental work involving k-SAT. Special attention is paid to how this influences the experimentally generated phase boundaries of satisfiability in random instances. We notice a phase transitions for various lengths k at these critical ratios after which almost all new clauses provide no new information. We also present a new model for generating random k-SAT instances in which redundant clauses are omitted, and a method for removing redundant clauses from pre-generated systems.

Abstract Author(s): Scott Clark