SAT+MiniSAT三元可满足性问题的研究与实现(6)
(图4.1.1)
3.把这个文件转移到MiniSat文件夹中的debug文件夹中。
4.打开电脑中运行界面输入“cmd”,从dos界面进入MiniSat中的debug,输入代码如下：
cd c:\MiniSat-C_v1.14.1\Debug
(图4.1.2)
5.进入debug之后在输入如下：
Main.exe output1.cnf得到结果如下： (图4.1.3)
此处显示该cnf可解，解答结果是x0取真值，x1取真值，x2取非真值，x3取非真值。
以上是一个解答的例子，如果需要从结果中总结规律，则需要大量数据来总结，由于电脑系统的限制，无法完成较大的数据，现在只研究k为2-6之间，小数点后精确到1位（因为精确到两位则需要的数据位3位数，即100以上个元素）的3SAT合取范式。
4.2 第一步（确定存在极点）
先把2-6之间的k的情况作一个整体的解答（即k=2,3,4,5,6的情况），初步总结解答结果，数据如下：
(表4.2.1)
k v c k v c k v c k v c k v c
2 10 20 3 10 30 4 10 40 5 10 50 6 10 60
20 40 20 60 20 80 20 100 20 120
30 60 30 90 30 120 30 150 30 180
40 80 40 120 40 160 40 200 40 240
50 100 50 150 50 200 50 250 50 300
60 120 60 180 60 240 60 300 60 360
70 140 70 210 70 280 70 350 70 420
80 160 80 240 80 320 80 400 80 480
90 180 90 270 90 360 90 450 90 540
100 200 100 300 100 400 100 500 100 600