5

私は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ソルバーを使用してこれを解決する方法を教えてもらえますか?

4

3 に答える 3

3

SAT4J の使用例を探していたところ、6 年前のこのトピックを見つけました。

提供されたリンク（ DIMACS）に次のように記載されているため、Valentin Montmirailの答えは正しくないと思います：

句の定義は、最終値「0」で終了します。

したがって、正解は次のようになると思います。

 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

私はこれで 30 分を失いました。将来の読者に役立つことを願っています。

于 2016-06-22T07:39:24.043 に答える
0

彼らのウェブサイトでSAT4Jハウツーをレビューしましたか？これには、CNF形式のセマンティクスを詳述したPostscriptドキュメントへのリンクが含まれています。この形式は、「<->」を除いて、例で使用するすべての演算子をサポートしているようですが、この特定の「非公式」ドキュメントでは省略されている可能性があります。

于 2010-10-16T00:01:32.690 に答える