SAT as a Programming Environment for Linear Algebra

In this paper we present an application of the propositional SATisfiability environment to computing some simple orthogonal matrices and some interesting tasks in the area of cryptanalysis. We show how one can code a search for some kind of desired objects as a propositional formulae in such a way that their satisfying valuations code such objects. Some encouraging (and not very encouraging) experimental results are reported for the proposed propositional search procedures using the currently best SAT solvers. In this paper we pursue a propositional programming paradigm. To solve your problem: (1) translate the problem to SAT (in such a way that a satisfying valuation represents a solution to the problem); (2) run the currently best SAT checker to solve it for you. The propositional encoding formula can be thought of as a declarative program. The hope you can get a solution relatively fast is based on the fact that the SAT solving algorithm is one of the best optimized. A SAT solving...

• Type: Journal
• Year: 2010
• Where: FUIN
• Authors: Marian Srebrny, Lidia Stepien
• Keywords: FUIN 2010, Propositional, Propositional Satisfiability Environment, Satisfying Valuation