Memory-Efficient Inference in Relational Domains
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.