Input CNF for SAT4J solver

Question

I a totally new to sat4j solver..

it says some cnf file should be given as input

is there any possible way to give the rule as input and get whether it is satisfiable or not?

my rule will be of the kind :

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 )
)

Can someone help me how to solve this using sat4j solver?

Answer 1

If you want to use SAT4J, you need to transform your problem CNF format.

You first need to transform these text variables into integer.

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 

Then, here are the rules and syntaxes that you need to know to transform your problem into CNF format.

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) 

And here is your example-problem, formatted as it should be to be read by SAT4J.

(see DIMACS to know more about this format).

 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

I let you run SAT4J on this little example,

and it will give you the solution SATISFIABLE xor UNSATISFIABLE.

Little sum-up of what you have to do to use 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.

I hope this step-by-step example will help few people.