minisat 安装指南-程序员宅基地

技术标签: minisat  

以下操作均需要在linux环境下执行。

首先到http://www.minisat.se/MiniSat.html下载minisat-2.2.0.tar.gz这个安装包,并解压缩,可以看到压缩包中有一个README,其中就包含了安装方法:

1.进入解压缩后的文件夹

2.export MROOT=文件夹所在路径    //这句的意义是声明一个环境变量保存文件夹路径,下面的make命令会调用这个环境变量以完成安装

3.cd core 或 cd simp   //两个版本的minisat,通常用第一个,即执行cd core

4.make rs         //开始编译程序,按照文件夹中makefile的规定。makefile已写好无需改动。

5.cp minisat_static /usr/bin/minisat    //上一步make之后生成了一个名为minisat_static的可执行程序,将其拷入/usr/bin/minisat 中,使该程序在任意路径下都可执行。


minisat所需实验数据可以从http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html下载,下载的数据文件需要将最后一行那个0删去才能正常调用。


如果要修改程序,可以直接在core或 simp中修改main文件,然后仍然按照那五步进行编译。

版权声明:本文为博主原创文章,遵循 CC 4.0 BY-SA 版权协议,转载请附上原文出处链接和本声明。
本文链接:https://blog.csdn.net/Baoli1008/article/details/47030409

智能推荐

vue中 同步,异步获取后台数据并在另外的方法中调用该数据_vue中success的结果传出-程序员宅基地

文章浏览阅读1.2k次。【代码】vue中 同步,异步获取后台数据并在另外的方法中调用该数据。_vue中success的结果传出

Web入门之VScode连接数据库sql server(超详细)_vscode连接sql server-程序员宅基地

文章浏览阅读2.5w次,点赞53次,收藏292次。Web入门之VScode连接数据库sql server(超详细)今天我们终于开始连接数据库啦,作为一个登录页面,怎么能不连接我们已经建立好的school数据库呢,下面,我们一起来连接吧,非常简单哦。打开数据库第一步当然就是打开我们的数据库啦,以前我们可能常常使用本机地址一键登录,不过这次我们需要使用密码登录喽。身份验证这里我们选择SQL Server 身份验证,登录名一般默认都是sa,输入密码,密码我们之前设好过,如果忘记也没关系,是可以修改的,如果忘记的话,之后我会写一篇文章,介绍如何修改密码。_vscode连接sql server

性能监控系统的搭建(转)-程序员宅基地

文章浏览阅读253次。引言前阵子在w3ctech的走进名企 - 百度前端 FEX 专场上曾“夸下海口”说听完讲座后七天就可以打造自己的前端性能监控系统,既然说出去了也不能食言。从前一篇文章前端数据之美相信大家对前端数据有了一定的了解,下面就针对其中的性能数据及其监控进行详细阐述。开始行动本文中的性能主要指 web 页面加载性能,对性能还不了解?不用担心,接下来的“每一天”跟我一起进入前端性能的世界。Da..._用ssm搭建远程服务器性能监控系统

npm使用国内淘宝镜像(最新地址)_npm最新淘宝镜像-程序员宅基地

文章浏览阅读5.1w次,点赞143次,收藏203次。我们前端程序员在使用使用国外的镜像源速度很慢并且容易下载失败,有时候需要尝试多次才有可能下载成功,很麻烦,但是可以切换为国内镜像源,下面我介绍下如何使用淘宝镜像源。通过上述的操作,我们可以轻松地配置和使用淘宝镜像来加速npm包的下载、安装和更新。_npm最新淘宝镜像

hive case when的选择顺序优先级问题_hive case when then-程序员宅基地

文章浏览阅读9.1k次,点赞6次,收藏9次。hive 中有case when 的语法是:case when 条件1 then 结果1when 条件2 then 结果2when 条件3 then 结果3......else 结果x end那如果被查询的行同时符合条件1和条件3呢?结果会是出现“结果1”还是“结果3”呢?根据测试,是符合结果1,原因是语句先“碰见” when 条件1 then 结果1这一句。如果语句改为:se..._hive case when then

中北网安实训笔记-(20200628)-域名信息、端口信息收集、nmap手册网址、敏感信息收集、GIT信息泄露_中北网络域名-程序员宅基地

文章浏览阅读232次。今天内容1.信息收集(收集目标所有可以收集的信息) 工具 客户端 网页端域名信息(子域名)站点信息端口信息敏感信息2.扫描探测(awvs xray)漏洞的入口点——————————————————PPT:域名解析过程:用户–>浏览器输入baidu.com -->浏览器DXS服务器缓存–>系统缓存dns服务器缓存C://windows/system32/drivers/etc/host–>dns服务器(发送请求)whois查询备案域名划分子域名_中北网络域名

随便推点

多账号自媒体工具,多平台同时发布_多ip 多账号 多平台 文章自动发布 开源-程序员宅基地

文章浏览阅读699次。现在使用自媒体工具进行头条号内容发布的自媒体人有很多,尤其是头条号作为自媒体主流平台,在各大平台里,所占的人数也具有一定的数量,很多人不是只运营头条号一个平台,其他的平台也有在运营。由于平台账号的增加,大多数人在内容分发上面花费的时间越来越多,这个时候大家就可以用到蚁小二自媒体工具,5分钟就可以把内容发布到多个平台,还能批量导入上百个账号,检测文章原创度。同时在给大家分享几个我们在自媒体运营中需要用到的小工具。1.找素材工具关于素材方面的工具,大家应该也见过很多,像易撰素材采集工具这.._多ip 多账号 多平台 文章自动发布 开源

分布式文件存储系统minio、大文件分片传输_miniio 分片写入文件-程序员宅基地

文章浏览阅读991次。MD5计算将整个文件或者字符串,通过其不可逆的字符串变换计算,产生文件或字符串的MD5散列值。如果传入的是一个负数,那么这个偏移量将会从数据的末尾从后到前开始计算。因为如果文件、字符串的MD5散列值不一样,说明文件内容也是不一样的。包含了一套完整的事件模型,用于捕获读取文件时的状态,下面这个表格归纳了这些事件。通过slice方法,从blob1中创建出一个新的blob对象,size等于3。的一个下标,这个下标-1的对应的字节将会是被拷贝进新的。,其中 3 个用以读取文件,另一个用来中断读取。_miniio 分片写入文件

华为OD机试真题2023(JAVA)_华为机试-程序员宅基地

文章浏览阅读1.1w次,点赞53次,收藏214次。在华为od岗的薪资问题,并没有比市场上多多少,具体根据个人职级和绩效而定,初入职场的应届生薪资大概在20K-30K左右,相对于其他行业来说,华为的起薪是比较高的。华为OD机试通常由多个题目组成,包括算法设计、编程、调试等多个环节,考察候选人的基础知识、实际能力和算法编写能力等多个方面,是华为招聘流程中非常重要的一环。大家有什么不懂的,想看的,都可以留言,或者私信哪吒。总的来说,OD岗位的晋升空间相对较广,但是需要候选人不断提升自身能力,积极参与公司的内部培训和发展计划,才能在职业生涯中获得更好的发展机会。_华为机试

html中两个块之间有空隙,css标签之间引发空隙问题解决办法-程序员宅基地

文章浏览阅读1.2k次。首先看这段空隙对应的源代码如下代码看起来没有任何问题,那么问题真的来了:空隙去哪里了啊?问题原因:图片文字等inline元素默认是和父级元素的baseline对齐的,而baseline又和父级底边有一定距离(这个距离和font-size,font-family相关,不一定是5px),所以设置vertical-align:top/bottom/text-top/text-bottom都可以..._html父元素和子元素间始终有空格

JTable冻结列的简单实现_用jtable实现excel冻结列-程序员宅基地

文章浏览阅读2.8k次。JTable实现冻结列的示例_用jtable实现excel冻结列

highlight.js网页代码高亮插件左侧怎么展示行号_highlightjs/vue-plugin 行号-程序员宅基地

文章浏览阅读288次。前几天分享了一篇网页代码高亮插件highlight.js,效果还不错,因为highlight.js本身没有行号展示,对于观感和体验上来源还是有点不太友好哈,恩。这几天越看越难受,忍不了还是弄一下吧。操作完成,上面代码框展示的就是配置后的效果了,因为我不大喜欢侧那块灰色的条,所以在css里面注释了,因人而异吧,喜欢的可以自己打开试下效果。_highlightjs/vue-plugin 行号

推荐文章

热门文章

相关标签