Number representations of satisfiability

Propositional formulas are represented by real-valued matrices in such way that unsatisfiability is proved to be equivalent to stable non-negative solvability of linear algebraic systems. Complete calculus for the generation of all non-negatively solvable linear homogeneous systems is presented as consequence.
Solvability of systems of linear inequalities with real coefficients and Boolean variables is reduced to satisfiability of some formula. Alternative's theorem is proved for solvability of such systems. The technique of implicit enumeration for the search of solutions both in considering systems and in a wide range of discrete optimization problems is described.