Задача
Решить задачу о 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.