О sat4j, как использовать sat4j для решения псевдобулевых задач?

У меня есть псевдобулевы проблемы, и мне нужно решить их с помощью sat4j.

Кто-нибудь может мне помочь?

Вот моя проблема:

  • У меня есть список переменных с именами: a,b,c,d,e,f

  • И у меня есть список значений, представленных: #1, #2, #3.....

  • h(a,#1) означает присвоить #1 a

У меня есть несколько примеров ограничений:

h(a,#1)=1
h(a,#1)+h(b,#1)+h(c,#1)=1
h(a,#1)+h(a,#5)>=1
h(b,#2)+h(b,#3)+h(b,#4)>=1

Так много ограничений, как в приведенных выше примерах. Наконец, я хочу, чтобы результат присвоения значений каким значениям.

Как я могу решить это с помощью sat4J? Как я должен представлять ограничения?


java boolean constraint-satisfaction sat-solvers sat4j
person JulieZhu    schedule 17.08.2017    source источник
comment
Я бы не стал использовать решатель CNF для этого. SMT подходит гораздо лучше.   -  person Kyle Jones    schedule 17.08.2017
comment
какой решатель SMT? можете ли вы порекомендовать один мне? мне нужно интегрировать код с моим java-проектом, поэтому мне нужен инструмент, который одновременно решает логическую проблему песудо и предлагает java API.   -  person JulieZhu    schedule 18.08.2017
comment
Z3 — популярный SMT-решатель, который я использовал для развлечения. Я не пытался использовать Java для общения с ним, но другие пытались, по крайней мере, согласно Google. В любом случае простой синтаксис ввода/вывода Z3 LISPy не составит труда проанализировать.   -  person Kyle Jones    schedule 18.08.2017
comment
да, я знаю инструмент z3, но он не предлагает java API.   -  person JulieZhu    schedule 18.08.2017
comment
Похоже, что другие люди уже сделали работу с API. Я подозреваю, что использовать Z3 будет проще, чем кодировать сумматоры и схемы сравнения, что вам нужно сделать, чтобы использовать решатель на основе CNF.   -  person Kyle Jones    schedule 18.08.2017
comment
@KyleJones Псевдобулев решатель, такой как org.sat4j.pb, не требует вручную созданных сумматоров и компараторов для выражения этих ограничений.   -  person Anders Kaseorg    schedule 05.11.2017

Ответы (1)


arrow_upward
0
arrow_downward

Если я правильно понимаю вашу проблему как псевдобулеву проблему удовлетворения, вы можете напрямую закодировать ее как файл OPB:

* #variable= 7 #constraint= 4
1 x1 = 1;
1 x1 1 x2 1 x3 = 1;
1 x1 1 x4 >= 1;
1 x5 1 x6 1 x7 >= 1;

где я произвольно закодировал h(a,#1) как x1, h(b,#1) как x2, h(c,#1) как x3, h(a,#5) как x4, h(b,#2) как x5, h(b,#3) как x6 и h(b,#4) как x7. (Возможно, вы захотите добавить такие ограничения, как

-1 x1 -1 x4 >= -1;
-1 x2 -1 x5 -1 x6 -1 x7 >= -1;

утверждая, что каждая переменная имеет не более одного значения, или = ровно для одного значения.)

Затем запустите

java -jar org.sat4j.pb.jar yourfile.opb

который выводит (игнорируя многие строки комментариев, начинающиеся с c):

s SATISFIA@KyleJones You don’t need to manually build adders and comparators to use a pseudo-boolean solver like `org.sat4j.pb`.BLE
v x1 -x2 -x3 -x4 x5 -x6 -x7

означает, что x1 и x5 истинны, а x2, x3, x4, x6 и x7 ложны.

(Я уверен, что есть способ сделать то же самое, используя org.sat4j.pb API Java, но, возможно, этот рецепт командной строки даст вам отправную точку, которая поможет вам в этом разобраться.)

person Anders Kaseorg    schedule 05.11.2017