【摘 要】
：
为了提高可满足性求解器的效率,提出了一种利用电路可观无关性的方法.以带可观无关条件的CNF理论为基础,通过在可观无关条件计算时不使用变量排序,减少可观无关条件丢失.通过不对只出现在可观无关条件中的变量赋值,保证电路的控制唯一性.理论分析和实验结果表明,用该方法实现的可满足性求解器的搜索空间小、速度快.
【机 构】
：
哈尔滨工程大学计算机科学与技术学院,黑龙江科技学院计算机与信息工程学院
【基金项目】
：
基金项目：国家自然科学基金（60273081）.
论文部分内容阅读
为了提高可满足性求解器的效率,提出了一种利用电路可观无关性的方法.以带可观无关条件的CNF理论为基础,通过在可观无关条件计算时不使用变量排序,减少可观无关条件丢失.通过不对只出现在可观无关条件中的变量赋值,保证电路的控制唯一性.理论分析和实验结果表明,用该方法实现的可满足性求解器的搜索空间小、速度快.
其他文献
为了在CAGD中有效地求解三角域上Bézier曲面的最小平方逼近问题,给出了三角域上双变量Jacobi基和Bernstein基的相互转换矩阵.首先利用Bernstein基构造了三角域上的Jacobi多项式;然后利用单变量Jacobi基和Bernstein基的转换关系,给出了三角域上双变量Bernstein基与Jacobi基的相互转换矩阵.进一步,利用该矩阵得到了在加权L2范数下基于正交基的Bézi
几何建模是虚拟手术仿真的重要部分,如何构建高精度的软组织模型和提高建模速度是目前该领域的研究重点.根据断层医学图像理论,提出一种高效和高质量的Delaunay四面体软组织建模方法——限定性Delaunay逐点递增插入法.首先在传统的Delaunay逐点递增算法上增加了有利于边界恢复的限定性条件,以减少Delaunay四面体建模过程中丢失边界的数量,较好地保证了模型的完整性;其次针对建模过程中丢失边
随着社会主义市场经济的不断推进,以及经济结构的不断调整,我国的城市化进程也在不断加快。由于财政税收政策是城市经济增长的基础和保证,财政税收政策的合理与否,直接决定着
在新能源汽车的研究、生产以及使用过程中,企业不仅需要巨大的资金投入,而且受到诸多不确定性因素的影响,使得目前新能源汽车企业在发展过程中面临着较大的风险。因此,如何通
针对海量层次信息可视化问题,提出嵌套圆鱼眼视图及实现方法.首先分析了相关工作;然后构造了针对同层兄弟节点的变形函数,给出了针对焦点节点同层兄弟节点的外切圆变形排列算法、变形后节点的子节点的嵌套圆递归排列算法及将二维鱼眼视图映射为三维鱼眼视图的方法;最后将该方法应用于计算机文件系统可视化.实验结果表明:该方法在相对小的显示空间内,既能显示海量信息的整体视图,又能突出局部焦点细节信息,具有较高的任务完
财务主管一般指的是单位财务工作负责人,如总会计师、财务总监等,既是单位的大管家,也是财务部门的领头羊。进入新时代,作为行政事业单位的财务主管,如何能够更新观念、提升
集成电路可布性评估在集成电路物理设计中针对布局结果进行有效的评估,作为对布局的反馈信息,并指导后续布线阶段的工作,避免了当后续布线无法完成时再回到前面布局阶段进行重新布局的被动局面,减少了物理设计的迭代周期.提出一种快速可布性评估算法,采用新的基于概率模型的估计算法,利用边界框进行拥挤度的预估,并在概率指导下进行实际布线.文中算法可以在很短的运行时间内对拥挤情况进行较为准确、客观的分析,线长较短.
在三维模型最优视点选择中,将模型的浮雕显著性信息度量引入模型视点互信息的信息熵分析,提出一种结合视觉显著性的模型视见描述子刻画方法.针对模型视点球的各个视点计算模型可见面片浮雕显著性信息熵驱动的视见描述子,并从中选择视见描述子值最大的视点作为模型的最优观察视点.实验结果表明,由该方法获取的最优视点得到的视图能够反映和展示三维模型的视觉显著特征.
为了抑制地震数据噪声,增强可视化效果,保证地质特征识别算法有效,提出一种基于地震数据局部结构属性与全局纹理属性的三边滤波算法.在局部结构属性中定义数据强度、空间距离和朝向权值函数,使得滤波算法能够综合考虑边结构特征及其类型;全局纹理属性分析则借助于鲁棒紊乱度地震属性估计与条件参数定义,采用参数自动调整办法自适应调整滤波效果.通过数据体噪声层的结构残留量以及层位识别结果比较,解决了评价地震数据滤波算
设计更改的连锁反应效应可能导致不可预计的后果,为了更好地获取更改在零件间的传播过程,提出基于装配关节图的更改传播求解方法.装配关节图以机件内部所有与装配特征相关的几何特征为研究对象,零件间的连接关系和零件内几何特征间的空间关系分别用装配关节和变换矩阵表示;作用于几何特征的设计更改表达为特征坐标系下的变换矩阵,更改在关节图上的传播按机器人学中的正运动学问题求解,并在关节处根据自由度进行消解;在装配关