Решение задач SAT/SMT требует представления в CNF и использования библиотек, таких как Z3, но время растет экспоненциально с увеличением размера задачи.

Roman Shiredchenko 2017.09.02 20:38 #39691

это и юмор и интересное

Roman Shiredchenko 2017.09.02 20:38 #39692

ИМХО

Dr. Trader 2017.09.02 22:41 #39693

Вот довольно быстрое решение задачки про 8 ферзей, на питоне у меня решается за 36 миллисекунд: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm (нужно найти заголовок "Eight Queens")

Нужна вот эта библиотека для питона https://github.com/Z3Prover/z3/releases и в самом коде первым делом выполнить "from z3 import *" и только потом тот код что по первой ссылке.

Миллион заработать не выйдет, время на решение экспоненциально растёт в зависимости от числа ферзей, например задача на 100 ферзей уже где-то полминуты решается.

Чистая математика, физика, логика Машинное обучение в трейдинге: Центовые сигналы, что будет

Oksana Berenko 2017.09.02 23:10 #39694

geratdc:

Задача не имеет решения. 7 ферзей перекрывают всю площадь шахматной доски.

Имеет:

Denis Sartakov 2017.09.03 01:13 #39695

во времена почти былинные... да ?

Andrey Kisselyov 2017.09.03 01:29 #39696

Dr. Trader:

Вот довольно быстрое решение задачки про 8 ферзей, на питоне у меня решается за 36 миллисекунд: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm (нужно найти заголовок "Eight Queens")

Нужна вот эта библиотека для питона https://github.com/Z3Prover/z3/releases и в самом коде первым делом выполнить "from z3 import *" и только потом тот код что по первой ссылке.

Миллион заработать не выйдет, время на решение экспоненциально растёт в зависимости от числа ферзей, например задача на 100 ферзей уже где-то полминуты решается.

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

с уважением.