Transalg

Transalg: A Tool for Translating Procedural Descriptions of Discrete Functions to SAT. In this paper we present the Transalg system, designed to produce SAT encodings for discrete functions, written as programs in a specific language. Translation of such programs to SAT is based on propositional encoding methods for formal computing models and on the concept of symbolic execution. We used the Transalg system to make SAT encodings for a number of cryptographic functions.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 4 articles , 1 standard article )

Showing results 1 to 4 of 4.
Sorted by year (citations)

  1. Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
  2. Semenov, Alexander A.: Merging variables: one technique of search in pseudo-Boolean optimization (2019)
  3. Semenov, A. A.; Otpuschennikov, I. V.: On a class of decision diagrams (2016)
  4. Otpuschennikov, I. V.; Semenov, A. A.: Technology for translating combinatorial problems into Boolean equations (2011)