Local search strategies for equational satisfiability.

Keefe, K.

Argonne National Laboratory

关键词: Algebra;    Computer Calculations;    Matrices;    Mathematical Models;    99 General And Miscellaneous//Mathematics, Computing, And Information Science;   

DOI  :  10.2172/834713
RP-ID  :  ANL/MCS-TM-269
RP-ID  :  W-31-109-ENG-38
RP-ID  :  834713

美国|英语

来源: UNT Digital Library

【 摘 要 】

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.