/matlog2

Primary LanguagePython

Задача

Решить задачу о n ферзях, сведя её к SAT-задаче. Сгенерируйте входной файл для SAT-решателя программно и вызовите решатель. Ваша программа должна вернуть расстановку. См. https://ru.wikipedia.org/wiki/Задача_о_восьми_ферзях

Более конкретная спецификация: На вход подается число n Ваша программа должная вернуть расстановку. Делать это по следующей схеме

  • генерация формулы
  • перевод ее в cnf
  • запуск SAT решателя

Доп баллы можно получить за использование API солверов и любую креативность

Решение

Quickstart

Run

pip3 install -r requirements.txt

to install requirements, then run

python3 main.py

to start the solver.