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?

Peeve

Please provide more details. What exactly where you doing? – Dollar

I have to compare 2 ontologies, create an expression like this and check whether it is satisfiable, i dont have any idea on SAT solver or SMT solver, which one would handle expressions like these? and which will be better and easier ti use? – Peeve

I don't know what an SMT solver is, but SAT should do the trick. What is your input format? – Dollar

the above expression is my input.. but sat solver asks for input in cnf file.. is there any converter to convert this expression to cnf file? – Peeve

Answer 1

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.

Lw

yes.. but is there any program to convert given expression automatically to CNF format? as I'll be generating many such expressions and it cant be manually done.. And what is the difference between SMT solver and SAT solver? – Peeve

Answer 2

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.

Demagnetize

Answer 3

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.

Sarsenet

Is there also a way to restrict the solution? For instance to say that variable 4 has to be one in the solution. – Xantho

I think that if 4 has to be in the solution, therefore 4 must be true everywhere. Why do you need such requirements? – Sarsenet

Thank you ttben. – Filler