?

Log in

No account? Create an account
мини-цинк - Поклонник деепричастий [entries|archive|friends|userinfo]
Anatoly Vorobey

[ website | Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Links
[Links:| English-language weblog ]

мини-цинк [май. 25, 2018|01:30 am]
Anatoly Vorobey
[Tags|, ]

(программистское)

Потыкал немного в MiniZinc, язык для формулировки и решения проблем с ограничениями. В общем, довольно удобная штука, определяешь переменные и связи между ними на достаточно простом и гибком языке (есть поддержка целых чисел, плавающей точки, строк, массивов и множеств). Потом это компилируется в какую-то стандартную форму и скармливается программе-решателю (finite domain constraint solver), которых есть много разных, три поставляются вместе с самим MiniZinc. Чем эти решатели отличаются друг от друга и от SAT-решателей, я решительно не знаю, похоже, за последние 20 лет там наворотили кучу прогресса.

Не очень ясно, для каких серьезных вещей это нужно (но уверен, что есть такие, и кому надо - знают). Для всяких игрушечных целей это использовать легко и приятно, после первичной ассимиляции незнакомых понятий. Но надо помнить, что это не магия, в конечном итоге если будет много независимых переменных и слабые связи, он ничего не найдет. Скажем, для сравнения: найти расстановку 8 неатакующих ферзей на шахматной доске с помощью этого языка очень легко (и думаю, посчитать число решений тоже), а вот найти обход коня, покрывающий всю доску, наверное, невозможно - моя программа нашла обход длиной 30 за 15 секунд, а обход длиной 40 я устал ждать.

Всякого рода комбинаторные задачки, которые предназначены для решения вручную, можно щелкать как орешки. Вот для примера моя программа для решения следующего ребуса: МОРЕ+ШТОРМ=АВАРИЯ. https://pastebin.com/VeTXRQmg

Кстати, непростой ребус для решения вручную, попробуйте, если интересно (нужно найти, как заменить буквы на цифры, чтобы сложение было верным, при этом одной букве соответствует всегда одна и та же цифра, и разным буквам разные цифры). Я решал его вместе с женой и дочкой вчера, и у нас оказалось два разных решения. Я этой программой заодно проверил, есть ли еще, и нет - есть ровно два разных решения ребуса.
СсылкаОтветить

Comments:
[User Picture]From: dims12
2018-05-24 10:53 pm
Круто!
(Ответить) (Thread)
[User Picture]From: utnapishti
2018-05-24 11:02 pm
> непростой ребус для решения вручную

По-моему, как раз несложный:
А, Ш, В находятся сразу;
после этого для Р, И, О есть 8 вариантов;
два из них сразу дают единственное решение, остальные невозможны.
(Ответить) (Thread)
[User Picture]From: avva
2018-05-24 11:14 pm
Ну, "непростой" это относительное понятие :)
(Ответить) (Parent) (Thread)
[User Picture]From: utnapishti
2018-05-24 11:21 pm
ОК :) Просто обычно в таких задачах я не вижу, откуда можно было бы начать, и прихожу в отчаяние... А тут сразу было понятно, где можно хотя бы попытаться зацепиться.
(Ответить) (Parent) (Thread)
[User Picture]From: relf
2018-05-25 01:56 am

А сможет ли оно построить магический квадрат 3×3 из квадратов различных целых чисел? Вроде ограничения здесь сформулировать легко, а задачка до сих пор нерешённая.

(Ответить) (Thread)
[User Picture]From: toothedgoo
2018-05-25 07:23 am
Есть ли причина для вашего извращения, кроме извращенности ума (это я про решатель)?

Почему не так: constraint 10*(10*(10*m+o)+r)+e + 10*(10*(10*(10*s+t)+o)+r)+m = 10*(10*(10*(10*(10*a+v)+a)+r)+i)+y;
(Ответить) (Thread)
From: yacpdb
2018-05-25 02:32 pm
Мне кажется, такой подход будет практически эквивалентом полного перебора и практически не задействует бэктрекинг и всякие хитрые эвристики в решателях.
(Ответить) (Parent) (Thread)
[User Picture]From: toothedgoo
2018-05-25 06:43 pm
Какие такие эвристики. По моему этот миницинк тупее перебора и калькулятора.
Не может решить вот это

var float: x;
var int: y;
constraint x = 555;
constraint y > 0;
constraint y < x;
constraint abs(y - sqrt(x)) <= 0.5;
solve satisfy;

Хотя на калькуляторе элементарно round(sqrt(555)) = 24.

Второе место в рейтинге никчемности программ, после издающего пукающие звуки приложения для телефона.
(Ответить) (Parent) (Thread)
From: yacpdb
2018-05-26 06:24 am
> Какие такие эвристики

Most constrained variable, least constraining value и пр. - вот это все.

Я так понимаю, что идея состоит в том, что для некоторых(*) задач удачно(*) подобранный набор констрейнтов может(*) привести к большому выигрышу в быстродействии (против обычного перебора с возвратом).

(*) - а может и к пукающим звукам.

edit: constraining


Edited at 2018-05-26 06:25 (UTC)
(Ответить) (Parent) (Thread)
From: (Anonymous)
2018-05-25 09:26 am
А вы пробовали Sentient?
(Ответить) (Thread)
[User Picture]From: avva
2018-05-25 11:02 am
Этот? https://sentient-lang.org

Нет, не пробовал.
(Ответить) (Parent) (Thread)
[User Picture]From: lord_corwin
2018-05-25 10:36 am
А почему вы выбрали путь подсчета отдельных сумм и "ловли" переноса, а не путь подсчета всего равенства (с умножением на соответствующую позиции степень 10)?

Т. е. почему не стали делать так: constraint (M*1000 + O*100 + R*10 + E) + (S*10000 + T*1000 + O*100 + R*10 + M) == A*100000 + V*10000 + A*1000 + R*100 + I*10 + Q; ?
(Ответить) (Thread)
[User Picture]From: e2pii1
2018-05-25 02:41 pm
> для решения следующего ребуса: МОРЕ+ШТОРМ=АВАРИЯ.

Почему не написать просто цикл на обычном языке программирования и перебрать все варианты (на компилируемом языке вычислит быстро) ?

А думать лучше над более сложными задачами...


(Ответить) (Thread)
From: (Anonymous)
2018-05-25 03:09 pm
Чтобы почувствовать разницу, напишите Судоку на императивном и декларативном (напр. Пролог) языках.
(Ответить) (Parent) (Thread)
[User Picture]From: e2pii1
2018-05-25 03:14 pm
у аввы был пост когда-то, как двое (независимо) писали Судоку на императивном языкe - один нормальный, придумал идею и алгоритм и написал, а 2-й c agile фигнёй страдал


(Ответить) (Parent) (Thread)
[User Picture]From: occuserpens
2018-05-26 12:19 am
// Ворчливо

Честно говоря, Самба больше соответствует моим представлениям о домашнем уюте, чем такие вот языки. Все-таки какая ни на есть польза в хозяйстве.
(Ответить) (Thread)
[User Picture]From: gegmopo4
2018-05-26 02:02 pm

>>> def evalword(*args):
...     return int(''.join(map(str, args)))
... 
>>> import itertools
>>> for М,О,Р,Е,Ш,Т,А,В,И,Я in itertools.permutations(range(10)):
...     if М and Ш and А:
...         if evalword(М,О,Р,Е) + evalword(Ш,Т,О,Р,М) == evalword(А,В,А,Р,И,Я):
...             print(evalword(М,О,Р,Е), '+', evalword(Ш,Т,О,Р,М), '=', evalword(А,В,А,Р,И,Я))
... 
3625 + 97623 = 101248
6372 + 95376 = 101748
(Ответить) (Thread)
[User Picture]From: recoder
2018-05-29 05:48 pm
А это Пролог такой своеобразный?
(Ответить) (Thread)