Number representations of satisfiability
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part X, Tome 241 (1997), pp. 72-96
Voir la notice de l'article provenant de la source Math-Net.Ru
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.
@article{ZNSL_1997_241_a2,
author = {G. V. Davydov and I. M. Davydova},
title = {Number representations of satisfiability},
journal = {Zapiski Nauchnykh Seminarov POMI},
pages = {72--96},
publisher = {mathdoc},
volume = {241},
year = {1997},
language = {ru},
url = {http://geodesic.mathdoc.fr/item/ZNSL_1997_241_a2/}
}
G. V. Davydov; I. M. Davydova. Number representations of satisfiability. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part X, Tome 241 (1997), pp. 72-96. http://geodesic.mathdoc.fr/item/ZNSL_1997_241_a2/