SAT vs CSP: a commentary

TL;DR

This paper revisits and comments on a 2000 study comparing mappings between SAT and CSP problems, analyzing how different consistency techniques impact solving efficiency and the relationship between these two problem domains.

Contribution

It provides a reflective commentary on previous work, highlighting insights into SAT-CSP mappings and their implications for constraint solving methods.

Findings

Arc-consistency improves CSP solving efficiency

Unit propagation is effective for SAT problems

Mappings between SAT and CSP influence solver performance

Abstract

In 2000, I published a relatively comprehensive study of mappings between propositional satisfiability (SAT) and constraint satisfaction problems (CSPs) [Wal00]. I analysed four different mappings of SAT problems into CSPs, and two of CSPs into SAT problems. For each mapping, I compared the impact of achieving arc-consistency on the CSP with unit propagation on the corresponding SAT problems, and lifted these results to CSP algorithms that maintain (some level of ) arc-consistency during search like FC and MAC, and to the Davis- Putnam procedure (which performs unit propagation at each search node). These results helped provide some insight into the relationship between propositional satisfiability and constraint satisfaction that set the scene for an important and valuable body of work that followed. I discuss here what prompted the paper, and what followed.