Článek popisuje plně automatickou metodu pro reformulaci problému splňování omezujících podmínek přidáním implikovan ých podmínek získaných metodou jednotkové konzistence.