Данцин Е. Я. Две системы доказательства тавтологичности, основанные на методе расщеплений // Записки научных семинаров ЛОМИ, 1981, 105, 24–44.
Dantsin E., Goerdt A., Hirsch E. A., Schoening U. Deterministic algorithms for k-SAT based on covering codes and local search // Proceedings of the 27 International Colloquuium on Automata, Languages and Programming, ICALP'2000, vol. 1853 of LNCS, p. 236–247, Springer, July 2000. A journal version will appear in Theoretical Computer Science in 2002.
ИСТИНА