From arithmetic expressions to propositional formulae

In papers [3], [4], [5] Authors presented a new method of solving some kinds of computational tasks in the area of linear algebra by applying SAT-solver as the highly optimized algorithms for solving the problem of propositional satisfiability. On input SAT-solver (cf. [1], [2]) takes a propositional formula in the clause form. In this paper we show in detail how any arithmetical expression can be translated into propositional formula in the CNF form skipping out its traditional form. For this, we define the notion of consistency of arithmetic and boolean valuations.