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

8

如果你想使用 SAT4J，你需要转换你的问题 CNF 格式。

您首先需要将这些文本变量转换为整数。

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

然后，这里是将问题转换为 CNF 格式所需了解的规则和语法。

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)

这是您的示例问题，其格式应由 SAT4J 读取。

（请参阅DIMACS以了解有关此格式的更多信息）。

 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

我让你在这个小例子上运行 SAT4J，

它会给你解决方案SATISFIABLExor UNSATISFIABLE。

使用 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.

我希望这个循序渐进的示例对少数人有所帮助。

于 2015-07-29T13:05:16.570 回答
3

我正在寻找一个如何使用 SAT4J 的示例，并找到了这个已有 6 年历史的主题。

我认为 Valentin Montmirail 的答案不正确，因为提供的链接（DIMACS）说：

子句的定义以最终值“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 Howto？它包括一个详细说明 CNF 格式语义的Postscript 文档的链接。该格式似乎支持您在示例中使用的所有运算符，除了“<->”，但这可能是这个特定的“非官方”文档中的一个遗漏。

于 2010-10-16T00:01:32.690 回答