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

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

We describe MarketSAT, a highly decentralized, market-based 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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.