论文部分内容阅读
Einstein谜，亦称Zebra谜，是爱因斯坦在20世纪初提出的，他说世界上有98%的人答不出来。该问题是一个典型的逻辑推理题，可以通过SAT求解给出问题的答案。现将Einstein谜转换成SAT求解问题，并使用当前流行的SAT求解器，如MinSat，对Einstein谜进行自动求解。
Einstein谜的SAT求解
【摘 要】
：
Einstein谜，亦称Zebra谜，是爱因斯坦在20世纪初提出的，他说世界上有98%的人答不出来。该问题是一个典型的逻辑推理题，可以通过SAT求解给出问题的答案。现将Einstein谜转换成SAT求
【机 构】
：
西安电子科技大学计算理论与技术研究所,武汉大学软件工程重点实验室
【出 处】
：
计算机科学
【发表日期】
：
2010年5期
其他文献
语义Web Service（SWS）是应对商务对商务环境的挑战，是迈向自动Web服务的重要步骤。基于SWS的商务服务合成是服务计算领域最为活跃和开放的研究问题之一。提出了一种基于SWS的商
网络拥塞已经成为了人们普遍关注的问题。目前,针对网络拥塞控制的研究,提出了一些具体的方法和建议,但其都不能很好地解决网络拥塞。定性动态概率网络（QDPNs）是目前进行动态地
普适计算环境下用于授权决策的上下文条件满足程度、用户的信任程度以及授予用户权限后产生的安全风险程度都具有模糊性,现有的访问控制模型大都不支持对模糊信息的授权推理
将网络数据流聚类来实现负载平衡已经被广泛应用于集群入侵检测方法中。将相关性思想引入传统模糊C-均值聚类算法（FCM），给出数据流逻辑距离公式，提出了一种相关模糊C-均值聚类算（C
针对目前标准件库不支持异构CAD系统和标准件信息不完整两个主要问题,提出了一种基于细胞元本体的标准件库资源共享方法。该方法使用Web本体描述语言(Web Ontology Language,OWL)表示细胞元本体模型,制定语义映射规则,以细胞为转换单元,屏蔽了信息表示的异构性,使应用本体和细胞元本体成为具有语义关系的逻辑上的整体,实现了异构CAD系统对标准件库的共享及异构数据的实时转换。该方法应用
嵌入式软件的非功能性质是系统高可靠性的重要构成部分。传统的嵌入式软件可靠性保障技术主要关注于系统开发后期，缺乏有效工具对系统设计的非功能性质进行分析与验证。对基于
分析了威胁评佑中信息的不确定性以及计划识别存在的不足，将直觉模糊理论与计划识别相结合，提出了一种基于直觉模糊理论的多属性计划识别方法。建立了基于直觉模糊多属性计划识
针对当前软件开发效率低下、难以快速适应需求变化等问题，提出一种新的软件自动化开发技术。在一定的约束条件下通过PowerDesigner完成数据库概念模型的设计和物理模型转换，在C
根据车标区域及车体的对称性特征,提出了一种快速的车标定位方法。先通过垂直间隔差分和水平最大局部投影定位出车牌和车灯水平区域后,利用车牌、车灯和车标之间的几何位置和大小约束关系粗定位出车标区域,然后根据局部对称性和差分水平投影对粗定位区域进行二次定位,得到较精确的车标矩形区域。实验结果表明,平均定位准确率为94%,平均定位时间为21ms。
多描述编码可以有效地防止图像数据的丢失,防止对单份数据的依赖,保证接收端收到图像的质量。网络编码可以有效提高网络带宽利用率。为了适应数据在无线传感器网络中的可靠传