Proceedings of the AAAI Conference on Artificial Intelligence, 21
Propositionalization of a first-order theory followed by satisfiability testing has proved to be a remarkably efficient approach to inference in relational domains such as planning and verification. More recently, weighted satisfiability solvers have been used successfully for MPE inference in statistical relational learners. However, fully instantiating a finite first-order theory requires memory on the order of the number of constants raised to the arity of the clauses, which significantly limits the size of domains it can be applied to. In this paper we propose LazySAT, a variation of the WalkSAT solver that avoids this blowup by taking advantage of the extreme sparseness that is typical of relational domains (i.e., only a small fraction of ground atoms are true, and most clauses are trivially satisfied). Experiments on entity resolution and planning problems show that LazySAT reduces memory usage by orders of magnitude compared to WalkSAT, while taking comparable time to run and producing the same solutions.