启发式极性决策算法解SAT问题

提出了一种启发式极性决策的可满足性问题（SAT）新算法.该算法继承了当前SAT解决器的许多策略：快速BCP、子句记录、重启动搜索等.同时,该算法通过预先根据Karnaugh图的覆盖分布计算变量极性,将其加入到DPLL的决策过程中,大大降低了搜索过程中的冲突次数.实验表明采用该算法的解决器——DiffSat,能够解决许多目前最有效的解决器Zchaff和MiniSat所不能解决的实例.尤其是对于Bart基准系列中的每个实例,DiffSat都能够在0.03s内解决,而Zchaff和MiniSat在给定的900s内不能够解决大部分实例.而且,DiffSat解决器在某些实例上的特性远远优于具有代表性的基于不完全随机算法的解决器DLM.     

利用正交方法解SAT问题

提出了一种解决SAT问题的新算法.该算法首先定义了子句之间的正交关系;然后从消除子句之间的交叠信息出发,利用正交子句的特性,结合有效的简化技术,逐渐将问题简化为一组与原问题完全等价的正交子句组;最后,根据正交子句组对整个赋值空间的覆盖情况来判断SAT是否满足.该算法为SAT问题的解决提供了一个新的思路.     

基于R-CNN算法的分割检测算法

目前先进的目标检测算法大多基于R-CNN算法,如Fast R-CNN,Faster R-CNN,YOLO,SSD以及FPN+R-CNN.R-CNN算法利用了传统的Selective Search算法寻找可能包含物体的方框,将其送入CNN网络进行特征提取,以对方框内物体进行辨别.随着图片复杂度的升高和背景的多样化,Selective Search算法已无法满足精确性和实时性的要求.本文基于R-CNN算法,提出了一种优化分割检测算法.该算法将R-CNN与具有分割功能的FCN算法相结合,为目标检测算法提供了一种新的思路.测试结果与R-CNN算法相比,该算法在目标识别效果和耗时方面均有明显的提升.