Percolation of unsatisfiability in finite dimensions

The optimization of two-dimensional Boolean formulas is studied using percolation theory, rare region arguments, and boundary effects. In contrast with mean-field results, there is no satisfiability transition as the constraint density is varied, although there is a logical connectivity transition. In the disconnected phase, there is a transition in the solution time. The thermodynamic ground state for this NP-hard optimization problem is unique; local solutions can be adjoined to find the global ground state. These results have implications for the computational study of disordered materials.