Local Search Strategies for Equational Satisfiability

摘要

The search for models of an algebra is an important and demanding aspect of automated reasoning. Typically, a model is represented in the form of a matrix or a set of matrices. When a model is found that satisfies all the given theorems of an algebra, it is called a solution model. This paper considers algebras that can be represented by using a single operation, by way of the Sheffer stroke. The characteristic of needing only one operation to represent an algebra reduces the problem by requiring a search through all instances of a single matrix. This search is simple when the domain size is small, say 2, but for a larger domain size, say 10, the search space increases dramatically. Clearly, a method other than a brute-force, global search is desirable. Most modern model-finding programs use a global search; instead of checking every possible matrix, however a set of heuristics is used that allows the search space to be dramatically smaller and thus increases the likelihood of reaching a solution. An alternative approach is local search. This paper discusses several local search strategies that were applied to the problem of equational satisfiability.