A Propositional Programming Environment for Linear Algebra

In this paper we present an application of the propositional SATisfiability environment to computing bases of some vector spaces. As a motivation we refer to certain computational tasks in the area of the algebraic theory of quadratic forms; more precisely, in the theory of Witt rings of quadratic forms. As known in algebra, the problem of finding all automorphisms of an elementary Witt ring can be reduced to searching for some special kind of bases of certain vector space over the two-element Galois field. We show how one can code a search for some kind of bases as a propositional formula in such a way that its satisfying valuations code the desired bases. Some encouraging experimental results are reported for the proposed propositional search procedure using the currently best SAT solvers.