SAT as a Programming Environment for Linear Algebra

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

Abstrakty

EN

In this paper we pursue the propositional calculus and the SATisfiability solvers as a powerful declarative programming environment that makes it possible to create and run the propositional declarative programs for computational tasks in various areas of mathematics. We report some experimental results on our application of the propositional SATisfiability environment to computing some simple orthogonal matrices and the orders of some orthogonal groups. Some encouraging (and not very encouraging) experiments are reported for the proposed propositional search procedures using off-the-shelf general-purpose SAT solvers. Our new software toolkit SAT4Alg is announced.

Słowa kluczowe

EN

satisfiability; linear algebra; orthogonal matrices; orthogonal groups; declarative programming

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 1
• Strony: 115--127
• Opis fizyczny: Bibliogr. 11 poz., tab.

Twórcy

autor

Srebrny M.

autor

Stępień L.

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

Bibliografia

• [1] Boole, G. 1847. The Mathematical Analysis of Logic, Being an Essay Towards a Calculus of Deductive Reasoning. Cambridge: Macmillan, Barclay, and Macmillan; reprinted Oxford: Basil Blackwell 1951.
• [2] Boole, G. 1854. An Investigation of The Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities. London: Macmillan; reprint by Dover 1958; also Bool, G. 2003 The Laws of Thought. New York: Prometheus.
• [3] Brown, M. 1990. Boolean Reasoning: The Logic of Boolean Equations. Kluwer.
• [4] Davis, M. and Putnam, H. 1960. A Computing Procedure for Quantification Theory. Journal of the ACM 7(1):201-215.
• [5] Davis, M.; Logemann, G. and Loveland, D.W. 1962. A Machine Program for Theorem Proving. Communications of the ACM 5(7):394-397.
• [6] Eén, N. and Sörensson, N. 2005. MiniSat v1.14. http://www.cs.chalmers.se/"een.
• [7] Marshall, M. 1980. Abstract Witt Rings. Queen's Papers in Pure and Applied Math. 57. Queen's University, Kingston, Ontario, 1980.
• [8] Srebrny, M., and Stępień, L. 2007. A propositional programming environment for linear algebra. Fundamenta Informaticae 81:325-345.
• [9] Stępień, L. 2009. Propositional calculus as a programming environment for linear algebra. PhD thesis (in Polish). Inst of Comp Science, Polish Academy of Sciences, Warsaw, Poland.
• [10] Witt, E. 1937. Theorie der quadratischen Formen in beliebigen Körpern. J. Reine Angew. Math. 176:31-44.
• [11] zChaff. 2007. www.princeton.edu/"chaff/zchaff.html.