标签: sat4j

我是一个全新的sat4j求解器..

它说一些cnf文件应该作为输入

是否有任何可能的方法将规则作为输入并获得它是否可满足？

我的规则将是那种:

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

有人可以帮我解决这个问题,使用sat4j求解器吗？