Ho un dubbio sull’interpretazione del testo che dice:
Naturally, two entries of the PIN in the sequence do not overlap.
Si intende che nel file di input queste sovrapposizioni non si hanno oppure che si possono presentare e che in tal caso vanno gestite?
Inoltre i primi 2 costraints non garantiscono che sia N>=K ma forse lo garantisce il costraint 4?
It is guaranteed that the PIN can always be uniquely determinated.
In effetti leggendo le assunzioni non è del tutto chiaro, secondo il generatore non ci sono altre sequenze di K cifre che si ripetono più spesso del pin. Quindi le sovrapposizioni ci possono essere ma, di fatto, non dovrebbero cambiare la risposta.
grazie per la risposta, in sostanza chiedevo se (supponendo K=4) si può presentare la sequenza:
…x12121212y… o no? e se si ci sono 2 sequenze 1212 o 3? (suppongo 2 ma in tal caso il programma ne deve scartare 1 quella di mezzo)
Questa assunzione (almeno nelle mie intenzioni di allora 
) significa che il PIN esiste ed è unico; ovvero, che se S è la sequenza di lunghezza K che corrisponde al PIN e occorre s volte, non esiste nessun’altra sequenza S' di lunghezza K che occorre s' volte con s' \ge s.
Potenzialmente la sequenza che ti viene data è arbitraria; tuttavia ricorda che vale l’assunzione “two entries of the PIN in the sequence do not overlap”. Nell’esempio che proponi, se vuoi contare come occorrenza il primo “1212” allora quello in mezzo non può essere contato, visto che si sovrappone.
Spero di essere stato chiaro; se avessi ancora dubbi sull’interpretazione del testo, siamo qua 
.
Grazie per la risposta ma mi rimane uno dei due dubbi che sarà anche una pignoleria e che riformulo:
perchè un pin di lunghezza K esista deve essere N>=K ma esplicitamente questa garanzia non viene data.
Per averla si può utilizzare il costraint:
Citazione It is guaranteed that the PIN can always be uniquely determinated.
oppure è possibile che N sia minore di K.
Mi salvo in corner dicendo che è inclusa nell’assunzione che tu citi. In effetti, nel messaggio precedente ho scritto
Questa assunzione (almeno nelle mie intenzioni di allora
Per l’esistenza giustamente deve valere N \ge K (altrimenti ogni sequenza S di lunghezza K avrebbe 0 occorrenze e quindi non sarebbe vero che nessun’altra sequenza S' di lunghezza K non occorra s' volte con s' \ge s, visto che s' = s = 0 per ogni S, S').