An instance of finite satisfiability is a first-order sentence in negation normal form, presented as a finite structure: its elements are the nodes of the sentence's parse DAG, its variables, its relation symbols and their argument positions, with relations marking the conjunction, disjunction and quantifier nodes, the child relation, the variable a quantifier binds, the equality and atomic literals with their arguments and the signature of each symbol, the root, and a linear order on the syntax along which children precede their parents. A model of such an instance is a finite nonempty type with a local interpretation of the symbols, local meaning that the value of a symbol depends only on the positions of its signature; the truth of a node under an environment is the least fixed point of the Tarski clauses, one per node kind. The instance is satisfiable when it is well-formed and the universal closure of its root has a finite model, the problem of Trakhtenbrot (1950); see Libkin (2004), chapter 9. FINSAT is the decision problem of the structures isomorphic to a satisfiable instance.