A Propositional Programming Environment for Linear Algebra

• Autorzy: Srebrny M. , Stępień L.
• Języki publikacji: EN

Abstrakty

EN

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.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 81, nr 1-3
• Strony: 325--345
• Opis fizyczny: bibliogr. 16 poz., tab.

Twórcy

autor

Srebrny M.

autor

Stępień L.

• Institute of Computer Science, Polish Academy of Science, Ordona 21, 01-237 Warsaw, Poland,

Bibliografia

• [1] C.M.Cordes, TheWitt group and the equivalence of fields with respect to quadratic forms, J. of Algebra 26(1973), pp. 400-421.
• [2] M.Davis, G. Logemann and D. Loveland, A machine program for theorem proving, Communications of the ACM 5(1962), pp. 394-397.
• [3] M.Davis and H. Putnam, A computing procedure for quantification theory, Journal of the ACM 7(1960), pp. 201-215.
• [4] N. Eén and N. Sörensson, MiniSat v1.14, http://www.cs.chalmers.se/_een, November 2005.
• [5] T.Y. Lam, Introduction to Quadratic Forms over Fields, AMS Graduate Studies in Mathematics, vol.67, 2005.
• [6] M.Marshall, Abstract Witt Rings, Queen's Papers in Pure and Applied Math. 57, Queen's University, Kingston, Ontario, 1980.
• [7] R. Perlis, K. Szymiczek, P. E. Conner and R. Litherland, Matching Witts with global fields. In: W. B. Jacob, T.Y. Lam and R.O.Robson, eds., Recent Advances in real algebraic geometry and quadratic forms, Proceedings of the RAGSQUAD Year, Berkeley, CA, USA, 1990-1991,ContemporaryMathematics 155(1994), pp. 365-387, Amer. Math. Soc., Providence, RI.
• [8] A. Pfister, Multiplikative quadratische Formen. Arch Math. Soc. 16(1965), pp. 363-370.
• [9] A. Pfister, Zur Darstellung von -1 als Summe von Quadraten in einem Körper. J. London Math. Soc. 40(1965), pp. 159-165.
• [10] A. Pfister, Quadratische Formen in beliebigen Körpern. Invent. Math. 1(1966), pp. 116-132.
• [11] S. Prata, Je¸zyk C++. Szkoła programowania, Robomatic,Wrocław, 2003 (in Polish).
• [12] M. Ste¸pień, Automorphisms of products of Witt rings of local type, Acta Mathematica et Informatica Universitatis Ostraviensis 10(2002), pp. 125-131.
• [13] M. Ste¸pień, Automorphisms of Witt rings of elementary type, in: Mathematica. Proceedings of the Xith Slovak-Polish-Czech Mathematical School, Ru˘zomberok, June 2-5, 2004, Pedagogical Faculty Catholic University in Ruzomberok, 2004, pp. 62-67.
• [14] K. Szymiczek, Bilinear Algebra: An Introduction to the Algebraic Theory of Quadratic Forms, Algebra, Logic and Applications, Series Vol. 7, Gordon and Breach Science Publishers, 1997.
• [15] E.Witt, Theorie der quadratischen Formen in beliebigen Körpern, J. Reine Angew. Math. 176(1937), pp. 31-44.
• [16] L. Zhang, ZChaff, http://www.princeton.edu/_chaff/zchaff.html, 2004.