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

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Boolean Satisfiability

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.