Initial Experiments in Stochastic Satisfiability

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Satisfiability

This paper looks at the rich intersection between satisfibility problems and probabilistic models, opening the door for the use of satisfiability approaches in probabilistic domains. A generic stochastic satisfiability problem is examined, which can function for probabilistic domains as Sat does for deterministic domains. The paper defines a Davis-Putnam-Logemann-Loveland-style procedure for solving stochastic satisfiability prob- lems, and reports on a preliminary empirical exploration of the complexity of the algorithm for a collection of randomly generated probabilistic problems. The results exhibit the familiar easy-hardest-hard pattern for the diffculty of random Sat formulae. Special cases of the stochastic satisfiability problem lie in different complexity classes, and one counterintuitive result is that the computational complexity and the empirical complexity of the problems examined do not track each other exactly|problems in the hardest complexity class are not the hardest to solve.