Вход CNF для решателя SAT4J - PullRequest
Новая
       68

Вход CNF для решателя SAT4J

4 голосов
/ 15 октября 2010

Я совершенно новичок в sat4j solver ..

он говорит, что некоторый файл 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 solver?

Ответы [ 3 ]

5 голосов
/ 29 июля 2015

Если вы хотите использовать 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.

Надеюсь, этот пошаговый пример поможет немногим.

2 голосов
/ 22 июня 2016

Я искал пример того, как использовать 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 минут, надеюсь, это поможет будущим читателям.

0 голосов
/ 16 октября 2010

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

...