SAT as a Programming Environment for Linear Algebra

8 years 10 months ago
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...
Marian Srebrny, Lidia Stepien
Added 25 Jan 2011
Updated 25 Jan 2011
Type Journal
Year 2010
Where FUIN
Authors Marian Srebrny, Lidia Stepien
Comments (0)