MiniSAT求解器在电路故障诊断中的应用

MiniSAT求解器运用到电路故障诊断系统时,能够将判断一个电路是否存在故障问题转换为可满足性问题。本文将全加器的行为模型及观测分别使用合取范式(CNF)形式文件描述,调用MiniSAT求解器判定可满足性。该方法自动化程度高,能处理大规模的运算电路,具有较强的查找错误能力。

MiniSAT求解器在判定可满足性问题中的应用

目前布尔逻辑已成为计算机科学的重要理论基础之一,是研究人类思维规律的重要工具。可满足性问题是典型的NP问题,SAT求解器的开发使得判定可满足性问题更加自动化。以与门电路为例,描述了如何将电路问题转换成可满足性SAT问题并使用MiniSAT求解器进行求解,包括输入格式、选项以及输出格式要求。

基于MiniSat的多项式方程组求解实现

在许多分析验证研究中,经常要对问题中的多项式组进行求解。当多项式方程组规模较大时,求解比较困难,大大限制了分析研究的效率。针对该问题设计了一种算法,将具有一定格式的多项式转化为合取范式形式,使多项式求解问题转化为SAT求解问题。利用SAT求解器Mini Sat对二元域上的多项式组进行求解,使得密码分析过程更加高效。实验结果表明:该算法能正确地将多项式进行转化,并能快速利用Mini Sat求出结果。

基于重启策略的学习子句优化方法

以学习子句数据库优化为背景,在原MiniSAT求解器的基础上提出了一种新的学习子句的优化方法.该方法基于博弈论的思想,在若干次重启后,根据当前求解器的实时反馈信息改进MiniSAT原有的增长参数,尽可能靠近学习数据库中子句存储量的均衡点,从而使学习库的存储量尽可能达到Pareto最优.实验表明:所提的优化方法是有效的,并在随机SAT问题上胜过现有优化方法.该方法既不会因为学习数据库的子句过多而影响单元传播速度,也不会因为学习数据库中的子句过少而破坏学习的整体性.

基于模型诊断电路故障诊断系统的设计与实现

为了使电路故障诊断系统更加智能化、高效化,将基于模型诊断的故障诊断技术应用在智能消防小车电路中。根据小车的系统行为信息对小车进行建模,利用串口模块将描述文件在线输入到计算机中,再根据IsDS算法以及带有终止节点的CSSE-tree算法调用MiniSAT求解器求解诊断结果。实验表明,该系统能够迅速指示故障元件,诊断效率较高,具有较好的应用前景。

基于Python的电路故障诊断系统通信模块的实现

本文以与门电路为例,介绍电路故障诊断系统通信模块的实现方法。利用下位机将与门电路系统所构建CNF形式描述的系统行为描述,组件正常行为描述以及51单片机获取观测值以此建立的观测值描述文件上传到上位机。上位机采用Python语言实现上下位机之间的串口通信,将所接收数据输入运行在Liunx操作系统下的MiniSAT求解器求解三元组,并将诊断结果反馈下位机。实验结果表明基于Python的通信模块可以很好的实现51单片机与PC机之间的串口通信。

针对低轮PRESENT的代数攻击

基于MiniSAT2.0软件,研究对低轮PRESENT的代数攻击问题。提出将S盒表示为单项式个数较少的无冗余等效方程组的方法,将PRESENT的S盒表示为由14个单项式个数均≤6的8元布尔方程构成的等效方程组,并基于不同的已知明文量,利用MiniSAT软件对PRESENT进行代数攻击实验,获得了较好的攻击效果。实验表明,在已知明文条件下可以在121h内求出80bit密钥的5轮PRESENT的全部密钥比特,在选择明文条件下可以在203h内求出6轮PRESENT的全部密钥比特。

基于子句文字长度动态约束的变量消除算法

变量消除算法作为一种重要的预处理算法已经应用于多种预处理器中。对比研究了在不同约束条件下,变量消除算法对简化性能和求解性能的影响,提出了基于子句文字长度动态约束的变量消除算法。该算法只允许当变量分解后的子句文字长度比原有子句文字少时,执行变量消除替换操作。在此基础上实现了一个基于Mini Sat开源代码的可满足性问题预处理器Mini Sat BFS。实验结果表明,与现有的基于子句数目约束的算法相比,新算法不仅降低了子句、变量和文字的数目,而且缩短了预处理过程和求解过程的时间消耗。更重要的是,改进后的算法在限定时间内可以求解更多的可满足性问题。

利用一种SAT问题全解算法求Trivium可滑动对

Trivium是进入到eSTREAM计划最终方案的一个序列密码体制,而在其初始化过程中存在可滑动对。SAT求解器可以有效地求解非线性方程组,然而一般的SAT求解器在求出一个解之后便会结束。对MiniSAT求解器中的算法进行改进,使之可以得出方程所有解。将改进的算法应用于Trivium中可滑动对的求解,得到了初始化拍数从111到120的所有可滑动对。相比于使用Grbner基方法,求解效率有了极大的提高。

小卫星编队飞行应用研究

小卫星编队系统有着成本低、高性能、和较强的灵活性等众多优点,这些特有的优势使其成为目前航天领域的研究热点。通过阐述目前小卫星编队飞行应用的研究方向、关键技术和未来的研究发展趋势,指出了该技术具有广阔的发展前景和空间。

System Design and Implementation of Intelligent Fire Engine Path Planning based on SAT Algorithm

In this paper, in order to make intelligent fi re car complete autonomy path planning in simulation map. Proposed system design of intelligent fi re car path planning based on SAT. The system includes a planning module, a communication module, a control module. Control module via the communication module upload the initial state and the goal state to planning module. Planning module solve this planning solution,and then download planning solution to control module, control the movement of the car fi re. Experiments show this the system is tracking short time, higher planning effi ciency.

面向观测任务的小卫星轨道仿真优化设计

研究对地观测小卫星轨道设计问题,是以区域覆盖性能为优化目标,对小卫星进行轨道设计。传统轨道设计方法要建立复杂的轨道动力学模型,优化过程计算量大、效率低,优化结果对不确定因素考虑不足。针对以上问题,结合遗传算法(GA)与灵敏度分析对面向区域观测任务的小卫星轨道进行优化设计。通过连接STK与VC实现覆盖性能计算,利用遗传算法实现小卫星轨道优化,采用灵敏度分析方法研究优化后的轨道参数变化对覆盖性能的影响程度。仿真结果表明优化后的小卫星轨道满足设计要求,能够达到覆盖性能最优。仿真结论,改进方法简单有效,优化效率高,可为实际工程中的小卫星轨道设计提供借鉴。

LBlock分组密码代数旁路攻击

对轻型分组密码LBlock抗代数旁路攻击安全性进行了评估.给出了LBlock密码算法的代数方程表示方法,使用示波器采集微控制器ATMEGA324P上的LBlock实现功耗泄露,利用泊松相关系数方法推断加密中间状态汉明重,基于可满足性问题并转化为代数方程组,同LBlock密码算法代数方程联立,最后使用CryptoMinisat解析器进行方程组求解,成功恢复加密密钥.实验结果表明:微控制器上的LBlock实现易遭受代数旁路攻击,仅需一条功耗曲线,已知明密文下的3轮汉明重泄露、未知明密文条件下6轮汉明重泄露分别经2.4s和0.4s分析即可恢复80bit完整密钥.

基于GSM的网络环境监测系统的设计与实现

本文以与门电路为例,介绍电路故障诊断系统通信模块的实现方法。利用下位机将与门电路系统所构建CNF形式描述的系统行为描述,组件正常行为描述以及51单片机获取观测值以此建立的观测值描述文件上传到上位机。上位机采用Python语言实现上下位机之间的串口通信,将所接收数据输入运行在Liunx操作系统下的MiniSAT求解器求解三元组,并将诊断结果反馈下位机。实验结果表明基于Python的通信模块可以很好的实现51单片机与PC机之间的串口通信。