Как использовать Picat для создания файлов CNF из файлов Minizinc?

Меня интересует подсчет количества решений проблемы (не перечисление решений). Для этого у меня есть инструменты, использующие файлы CNF. Я хочу преобразовать файлы Minizinc (формат mzn или Flatzinc fzn) и преобразовать их в CNF.

Я узнал, что Picat может выгружать файл CNF после загрузки ограничений. Более того, в Picat есть умный модуль, который интерпретирует базовые файлы Flatzinc. Я изменил модуль fzn_picat_sat.pi, чтобы выгрузить файл CNF. Итак, что я делаю, так это то, что я конвертирую файл Minizinc в Flatzinc с помощью mzn2fzn, затем я пытаюсь преобразовать его в CNF, используя мой (немного) измененная версия fzn_picat_sat.pi.

Чего я хочу: я ожидаю, что Picat загрузит файлы Flatzinc и выгрузит соответствующий файл CNF. Если исходные проблемы имеют X решений, я ожидаю, что соответствующая CNF будет иметь X решений.

Что происходит: большинство файлов Flatzinc, которые я пробовал, работали нормально. Но некоторые, похоже, дают нежелательные результаты. Например, следующий mzn переводится как этот файл Flatzinc. В этом файле всего 211 решений, но сохранен файл CNF от Picat насчитывает более 130 тыс. решений. Многие решатели SAT могут показать, что файл CNF содержит более 211 решений (например, cryptominisat с опцией --maxsol ). Как ни странно, когда я прошу Picat решить файл Flatzinc без перевода в CNF, Picat находит только 211 решений. Проблема вроде где-то в переводе. Наконец, даже если в файле CNF имеется достаточное количество решений с использованием Picat, я получаю сообщение об ошибке % fzn_interpretation_error.

Если кто-то попробовал что-то подобное и преуспел, или если кто-нибудь знает, как переводить с языка программирования с ограничениями на CNF, это будет очень признательно. Спасибо всем.


constraint-programming minizinc sat picat
person Exeloz    schedule 18.08.2020    source источник
comment
1) Как именно перевести файл mzn в формат .fzn? Включаете ли вы при этом глобальные определения Пиката? 2) Как получить спутниковый решатель для генерации всех решений?   -  person hakank    schedule 18.08.2020
comment
@hakank: cryptominisat имеет --maxsol параметр для перечисления решений. В противном случае можно было бы добавить предложение со всеми инвертированными литералами решения, чтобы запретить повторное нахождение этого решения.   -  person Axel Kemper    schedule 19.08.2020
comment
Может быть, перевод Пика добавляет вспомогательные переменные, а полученные решения отличаются только этими вспомогательными переменными?   -  person Axel Kemper    schedule 19.08.2020
comment
Один из способов перечислить все решения - точно так, как говорит @AxelKemper, и использовать --maxsol of cryptominisat. Многие (если не все) решатели SAT будут иметь такую ​​возможность.   -  person Exeloz    schedule 19.08.2020
comment
@hakank На второй вопрос я ответил своим предыдущим комментарием. Для первого вопроса, как указано в вопросе, я использую mzn2fzn, который, кажется, является известным инструментом, поскольку он упоминается в файле fzn_picat_sat.pi. И если я не ошибаюсь, вы являетесь частью команды, которая сделала возможным этот модуль, поэтому я надеюсь, что то, что я говорю, понятно.   -  person Exeloz    schedule 19.08.2020
comment
@AxelKemper Может быть, Picat добавляет вспомогательные переменные, которые изменяют количество решений. Но я могу привести несколько примеров, очень похожих на приведенный выше, где полученная CNF отлично работает и дает ожидаемое количество решений. Возможно, я что-то неправильно понимаю во всем этом, это очень возможно. Но даже с добавленными переменными я надеюсь получить ожидаемое количество решений. Итак, если это так, есть ли способ узнать, какие переменные следует удалить, когда я считаю решения?   -  person Exeloz    schedule 19.08.2020
comment
@AxelKemper Спасибо за подсказку о криптоминизате. Тестированные мной решатели SAT (minisat, lingeling, глюкоза) не поддерживают все известные мне решения. Я также нашел bc_minisat_all.   -  person hakank    schedule 19.08.2020
comment
@Exeloz Причина появления fzn_interpretation_error заключается в том, что fzn_picat_sat пытается преобразовать выходную переменную MiniZInc в CNF, но для этого требуется, чтобы переменные были созданы, а это не тот случай, когда используется [dump]. Я не уверен, повлияет ли это на остальную часть перевода. Хотя я тестировал простую модель с 8 ферзями и получил 288 решений вместо 92, что-то странно. Можете ли вы сделать ссылку на модель MiniZinc, если бы вы получили правильное решение с помощью решателя SAT?   -  person hakank    schedule 19.08.2020
comment
@hakank Вообще-то могу. Я тестировал 8 ферзей, используя небинарные переменные в файле Minizinc. Вот простой файл mzn и соответствующий fzn и соответствующий CNF, предоставленный Пикатом, имеющим решение 92.   -  person Exeloz    schedule 19.08.2020
comment
@Exeloz Спасибо за модель королевы. Могу подтвердить, что версия CNF дает 92 решения. Однако CNF для этой модели (hakank.org/minizinc/queens4,mzn) (с использованием all_different ограничения) дают 288 решений. Кажется, что ограничение all_different дает дополнительные внутренние переменные.   -  person hakank    schedule 19.08.2020
comment
@Exeloz По поводу fzn_interpretation_error: если вы закомментируете вызовы fzn_output в программе Picat, сообщение об ошибке должно исчезнуть.   -  person hakank    schedule 19.08.2020
comment
@hakank По поводу ошибки спасибо за подсказку. Что касается модели королевы, я согласен, что моя модель была неоптимальной во многих отношениях, поскольку я не использовал никаких глобальных ограничений. Я попытался избежать этого ограничения, поскольку заголовок fzn_picat_sat.pi предупреждает, что mzn2fzn не должен разлагать alldifferent / 1. Я также хотел бы отметить, что я не использую никаких глобальных ограничений в Sequence.mzn, связанных с вопросом. Поэтому, даже если alldifferent / 1 дает дополнительные внутренние переменные, я ничего не понимаю в Sequence.mzn. Но здесь определенно что-то происходит   -  person Exeloz    schedule 19.08.2020
comment
@Exeloz Я думаю, что ответ Микаэля в том, что касается внутренних переменных. В случае с последовательностью существует множество дополнительных переменных, созданных в файле FlatZinc (тот, что с var_is_introduced), хотя решатели FlatZinc выводят только те решения, в которых переменные, помеченные как output_array, различны. Я не знаю, как избежать обработки внутренних переменных в файле CNF (ну, они являются частью модели, поэтому они должны быть включены в модель) или идентифицировать их каким-либо разумным способом.   -  person hakank    schedule 19.08.2020
comment
@hakank Достаточно честно, это имеет большой смысл, это точно. Но я все же надеюсь найти инструмент, который мог бы выполнить эту работу, но, в конце концов, это будет уже другой вопрос.   -  person Exeloz    schedule 19.08.2020
comment
Позвольте нам продолжить это обсуждение в чате.   -  person hakank    schedule 19.08.2020

Ответы (1)


arrow_upward
2
arrow_downward

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

predicate separated(var int: x, var int: y) = 
    let {
      var int: z
    } in
     x < z /\ z < y;
     
var 1..10: x;
var 1..10: y;

constraint separated(x, y);

solve satisfy;

Здесь предикат separated добавляет другую переменную, которая используется как свидетельство того, что между x и y есть какое-то число (предикат эквивалентен abs(x-y)>0).

В модели 36 решений (1,3, 1,4, ..., 8,10). Однако, если вы рассмотрите решение 3,8, есть 5 различных вариантов z, которые делают предикат истинным. В общем, пользователя, скорее всего, интересуют только решения, которые отличаются выходными переменными.

При переводе приведенного выше MiniZinc в CNF внутренняя z-переменная предиката не будет отличаться от реальных проблемных переменных x и y. Для подсчета решений вам нужно будет различать литералы, которые соответствуют областям выходных переменных в модели, и инструктировать решателю SAT рассматривать только два разных решения, если эти литералы разные (не уверен, что это функция, которая доступен).

person Zayenz    schedule 19.08.2020
comment
На самом деле у меня есть инструменты, позволяющие учитывать только подмножество переменных при подсчете решений. (Это не предлагается в известном мне решателе). Итак, если бы был способ узнать, какие переменные являются выходными переменными, я бы мог делать все, что я пытаюсь сделать. Вы знаете, как это сделать? Кстати, спасибо за объяснение. - person Exeloz; 19.08.2020
comment
Эти ответы имеют смысл и имеют очень убедительную модель. Я ценю время, которое вы потратили. Я приму этот ответ и все еще надеюсь найти способ выбрать правильные переменные при подсчете. - person Exeloz; 19.08.2020
comment
Спасибо. Поскольку я никогда не использовал Picat, я не могу вам с этим помочь. - person Zayenz; 20.08.2020
comment
Выходные переменные @Exeloz удобно помечать как таковые с помощью аннотации в файле FlatZinc, который создается компилятором mzn2fzn (или minizinc). Вы можете проверить парсер Picat, чтобы узнать, сохраняет ли он эти теги. В противном случае вы можете создать внутренние структуры данных, чтобы запоминать их, а затем использовать их по своему усмотрению. - person Patrick Trentin; 31.08.2020