毕业论文

打赏
当前位置: 毕业论文 > 计算机论文 >

SAT+MiniSAT三元可满足性问题的研究与实现(6)

时间:2017-01-06 13:21来源:毕业论文
(图4.1.1) 3.把这个文件转移到MiniSat文件夹中的debug文件夹中。 4.打开电脑中运行界面输入cmd,从dos界面进入MiniSat中的debug,输入代码如下: cd c:\MiniSat-C_v1.14.


 
(图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 SAT+MiniSAT三元可满足性问题的研究与实现(6):http://www.youerw.com/jisuanji/lunwen_1929.html
------分隔线----------------------------
推荐内容