SAT as a programming environment for linear algebra and cryptanalysis
Marian Srebrny, Mateusz Srebrny, Lidia Stępień · 2008
on his 65th birthday 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