Исключение решателя ЭМБ SAT4J

я пытаюсь построить N * N Queen placement problem solver для моего школьного проекта. Я сделал программу, которая генерирует заявления CNF. Я пытался дать его адрес в качестве аргумента «SAT4J embeding solver» 7-я страница, 3.1 ,однако он продолжает бросать ParseFormatException. Я также попытался использовать этот текстовый файл, найденный на stackoverflow:

c you can put comment here.

c Formatted by StackOverFlow.

p cnf 9 12

-1 2

-2 1

-3 4

-4 3

1

3

-5 -4

-6 -4

-7 -4

-8 -4

-9 -4

-2 -4

Тоже не повезло. Единственное, что я отредактировал, — это блок catch исключения, поэтому я могу видеть, какой он. Я пытаюсь дать ему аргументы через меню конфигурации Alt + Shift+F10 в IntelliJ Idea Community edition.

Может кто-то, пожалуйста, помочь мне/направлять меня? Это мой первый раз, когда я работаю с кем-то еще code + there is nothing i would call tutorial available.

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

Код класса на данный момент.

1 ответ

  1. Вам просто нужно закончить ваши линии с 0, и избежать дополнительных новых линий, например

    c you can put comment here.
    p cnf 9 12
    -1 2 0
    -2 1 0
    -3 4 0
    -4 3 0
    1 0
    3 0
    -5 -4 0
    -6 -4 0
    -7 -4 0
    -8 -4 0
    -9 -4 0
    -2 -4 0
    

    должно работать нормально.