A Propositional Programming Environment for Linear Algebra

Issue title: Topics in Logic, Philosophy and Foundations of Mathematics and Computer Science. In Recognition of Professor Andrzej Grzegorczyk

Article type: Research Article

Authors: Srebrny, Marian | St�pień, Lidia

Affiliations: Institute of Computer Science, Polish Academy of Sciences Warsaw, Poland. E-mail: [email protected] | Institute of Mathematics and Computer Science, Jan Długosz University Cz�stochowa, Poland. E-mail: [email protected]

Abstract: 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.

Journal: Fundamenta Informaticae, vol. 81, no. 1-3, pp. 325-345, 2007