Введите CNF для решателя SAT4J

Я совершенно новичок в решателе sat4j.

он говорит, что в качестве входных данных должен быть указан какой-то файл cnf

есть ли какой-либо способ ввести правило в качестве входных данных и узнать, выполнимо оно или нет?

мое правило будет таким:

Problem = ( 

     ( staff_1         <=>          staff_2 ) AND 
     ( doctor_1        <=>      physician_2 ) 

) AND ( 

     ( staff_1         AND         doctor_1 )

)  AND (

    NOT( ward_2             AND physician_2 ) AND 
    NOT( clinic_2           AND physician_2 ) AND 
    NOT( admission_record_2 AND physician_2 ) 

) AND (

   NOT( hospital_2          AND physician_2 ) AND 
   NOT( department_2        AND physician_2 ) AND 
   NOT( staff_2             AND physician_2 )
)

Может ли кто-нибудь помочь мне решить эту проблему с помощью решателя sat4j?


java nlp ontology sat-solvers sat4j
person karthi    schedule 15.10.2010    source источник
comment
Пожалуйста, предоставьте более подробную информацию. Что именно ты делаешь?   -  person Fred Foo    schedule 15.10.2010
comment
Мне нужно сравнить 2 онтологии, создать подобное выражение и проверить, выполнимо ли оно, я понятия не имею о решателе SAT или решателе SMT, какой из них будет обрабатывать такие выражения? и что будет лучше и проще в использовании?   -  person karthi    schedule 16.10.2010
comment
Я не знаю, что такое решатель SMT, но SAT должен помочь. Какой у вас формат ввода?   -  person Fred Foo    schedule 17.10.2010
comment
приведенное выше выражение является моим вводом.. но решатель спутников запрашивает ввод в файле cnf.. есть ли какой-либо конвертер для преобразования этого выражения в файл cnf?   -  person karthi    schedule 17.10.2010

Ответы (3)


arrow_upward
0
arrow_downward

Вы ознакомились с SAT4J Howto на их веб-сайте? Он включает ссылку на документ Postscript с подробным описанием семантика формата CNF. Похоже, что формат поддерживает все операторы, которые вы используете в своем примере, кроме «‹->», но это может быть упущением в этом конкретном «неофициальном» документе.

person Cerin    schedule 16.10.2010
comment
да .. но есть ли программа для автоматического преобразования данного выражения в формат CNF? так как я буду генерировать много таких выражений, и это невозможно сделать вручную. И в чем разница между решателем SMT и решателем SAT? - person karthi; 16.10.2010

arrow_upward
8
arrow_downward

Если вы хотите использовать SAT4J, вам необходимо преобразовать проблемный формат CNF.

Сначала вам нужно преобразовать эти текстовые переменные в целые числа.

1 = staff_1
2 = staff_2
3 = doctor_1
4 = physician_2
5 = ward_2 
6 = clinic_2
7 = admission_record_2 
8 = hospital_2
9 = department_2

Тогда вот правила и синтаксисы, которые вам нужно знать, чтобы преобразовать вашу проблему в формат CNF.

Syntax: 
    OR           = a space 
    AND          = a newline
    NOT          = -

Rules from De Morgan's laws: 
    A <=> B      = (A => B) AND (B => A)
    A  => B      = NOT(A) OR  B
    NOT(A AND B) = NOT(A) OR  NOT(B) 
    NOT(A OR  B) = NOT(A) AND NOT(B)

А вот ваш пример-задача, отформатированный так, чтобы его читал SAT4J.

(см. DIMACS, чтобы узнать больше об этом формате).

 c you can put comment here. 
 c Formatted by StackOverFlow.
 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

Я позволю вам запустить SAT4J на этом маленьком примере,

и это даст вам решение SATISFIABLE xor UNSATISFIABLE.

Небольшой итог того, что вам нужно сделать, чтобы использовать SAT4J:

 * Transform your `text_n` into a number.
 * Use the rule that I gave you to transform your problem into CNF.
 * Write the definition of your problem `p cnf nbVariables nbClauses`
 * Write everything in a FILE and run SAT4J on this file.

Я надеюсь, что этот пошаговый пример поможет мало кому.

person Valentin Montmirail    schedule 29.07.2015

arrow_upward
3
arrow_downward

Я искал пример использования SAT4J и нашел эту тему, которой 6 лет.

Я думаю, что ответ Валентина Монмирайя неверен, поскольку предоставлена ​​​​ссылка (DIMACS) говорит:

Определение предложения завершается окончательным значением «0».

Поэтому я думаю, что правильный ответ будет:

 c you can put comment here. 
 c Formatted by StackOverFlow.
 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

Я потерял 30 минут на этом, надеюсь, это поможет будущим читателям.

person ttben    schedule 22.06.2016
comment
Есть ли способ ограничить решение? Например, сказать, что переменная 4 должна быть единицей в решении. - person So S; 11.11.2016
comment
Я думаю, что если в решении должно быть 4, значит, 4 должно быть верно везде. Зачем вам такие требования? - person ttben; 26.11.2016
comment
Спасибо, ттбен. - person Abdulaziz; 11.08.2020