CNF input for SAT4J solver

Question

I am brand new to sol4j solution.

he says some cnf file should be specified as input

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

My rule will be:

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 solve this problem with sat4j solution?

Answer 1

Have you viewed SAT4J Howto on your website? It includes a link to a Postscript document that details the semantics of the CNF format. The format seems to support all the operators that you use in your example except “↔”, but this may be an omission in this particular “unofficial” document.

Answer 2

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

First you need to convert these text variables to 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 you need to know in order to convert your problem to CNF format.

 Syntax: OR = a space AND = a newline NOT = - Rules from De Morgan 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 read by SAT4J.

(see DIMACS to learn 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 will let you run SAT4J in this small example,

and he will give you the solution SATISFIABLE xor UNSATISFIABLE .

A little summation of what you need 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 helps few people.

Answer 3

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

I think Valentin Montmiril's answer is incorrect, as the link provided ( DIMACS ) says:

The sentence definition is interrupted by the final value "0".

Therefore, I think the correct answer would 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 30 minutes, I hope this helps future readers.