基于MiniSAT的命题极小模型计算方法

计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正CNF(conjunctive normal form)公式,其极小模型的计算和验证都不是易处理的.当前,计算CNF公式极小模型的主要方法之一是将其转换为析取逻辑程序后用回答集程序(answer set programming,ASP)求解器计算其稳定模型回答集.针对计算CNF公式的极小模型的问题,提出一种基于可满足性问题(satisfiability problem,SAT)求解器的计算极小模型的方法MMSAT;然后结合最近基于极小归约的极小模型验证算法CheckMinMR,提出了基于极小模型分解的计算极小模型方法MRSAT;最后对随机生成的大量的3CNF公式和SAT国际竞赛上的部分工业基准测试用例进行测试.实验结果表明:MMSAT和MRSAT对随机3CNF公式和SAT工业测试用例都是有效的,且计算极小模型的速度都明显快于最新版的clingo,并且在SAT工业实例上发现了clingo有计算出错的情况,而MMSAT和MRSAT则更稳定.

基于遗传交叉算子的深度Q网络样本扩充

区别于传统深度强化学习中通过从经验回放单元逐个选择的状态转移样本进行训练的方式,针对采用整个序列轨迹作为训练样本的深度Q网络(Deep Q Network,DQN),提出基于遗传算法的交叉操作扩充序列样本的方法.序列轨迹是由智能体与环境交互的试错决策过程中产生,其中会存在相似的关键状态.以两条序列轨迹中的相似状态作为交叉点,能产生出当前未出现过的序列轨迹,从而达到扩充序列样本数量、增大序列样本的多样性的目的,进而增加智能体的探索能力,提高样本效率.与深度Q网络随机采样训练样本和采用序列样本向后更新的算法(Episodic Backward Update,EBU)进行对比,所提出的方法在Playing Atari 2600视频游戏中能取得更高的奖赏值.