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

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.

Authors

• William E. Walsh and Michael P. Wellman University of Michigan

Keywords

No keywords are indexed for this paper.