输入SAT4J求解器的CNF
输入SAT4J求解器的CNF
提问于 2010-10-15 23:23:19
我是一个全新的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求解器解决这个问题？
Stack Overflow用户
发布于 2015-07-29 21:05:17
如果你想使用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，
它将为您提供SATISFIABLE xor 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.我希望这个循序渐进的例子能帮助很少的人。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/3943646
复制相关文章
相似问题
腾讯云开发者
