MarketSAT: An Extremely Decentralized (but Really Slow) Algorithm for Propositional Satisfiability

Abstract

We describe MarketSAT, a highly decentralized, marketbased algorithm for propositional satisfiability. The approach is based on a formulation of satisfiability as production on a supply chain, where producers of particular variable assignments must acquire licenses to fail to satisfy particular clauses. MarketSAT employs a market protocol for general supply chain problems, which we show to be expressively equivalent to 3SAT. Experiments suggest that MarketSAT reliably converges to market allocations corresponding to satisfiable truth assignments. We experimentally compare the computational performance with GSAT, a centralized local search algorithm. Introduction Decentralization comprises constraints on the distribution of information and authority among participants in a distributed system. In a decentralized system, the information state of an individual is considered private, and is disseminated only by voluntary communication acts. This contrasts with centralized syste...