StatSat is ...

Statistical Satisfiability

Using Markov Random Fields to explore issues of representation and reasoning.

SAT

Boolean Satisfiability (SAT) is the problem of finding satisfying valuations for a collection of Boolean constraints. Every set of Boolean constraints can be represented by a set of disjunctive propositional clauses.
k-SAT restricts attention to clauses with at most k literals. Every SAT problem can be reduced, by the addition of additional variables, to 3-SAT.

MRF

A Markov Random Field (MRF) determines a probability distribution over a set of random variables.
We view a MRF over a set of Boolean variables as a natural generalisation of SAT, and use a MRF to represent knowledge accumulated from experience.
We can construct a MRF, top-down a priori — for example, from a Markov Logic Network (MLN Richardson & Domingos), or bottom-up a posteriori, from a set of data.

Our bottom-up procedures are iterative and adaptive, so an initial MRF can be established to represent a priori assumptions, then adapted to reflect a posteriori experience.