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?
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.