Input CNF for SAT4J solver

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      开发者_如何学C  <=>      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?

---

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.

---

I was looking for an example of how using SAT4J and found this topic which is 6 years old.

I think the answer of Valentin Montmirail is not correct since the link provided (DIMACS) says :

The definition of a clause is terminated by a final value of "0".

Therefore, I think the correct answer will be :

 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 lost 30min on this, I hope it will help future readers.

---

Did you review the SAT4J Howto on their website? It includes a link to a Postscript document detailing the semantics of the CNF format. The format seems to support all the operators you use in your example, except "<->", but that just might be an omission in this specific "unofficial" document.