拉曼喷泉原子钟

利用拉曼光场代替喷泉原子钟的微波腔实现拉曼喷泉原子钟。将分离拉曼光场技术与冷原子喷泉技术相结合,避免了在真空腔内放置微波腔,简化了真空系统,同时还保持了很高的准确度。采用半经典理论研究了冷原子喷泉与拉曼光场的相互作用过程,得到了冉赛(Ramsey)条纹。比较了拉曼喷泉原子钟与热铯束拉曼原子钟,前者有更小的体积和功耗,其精度可能达到或超过商用小铯钟。还比较了拉曼喷泉原子钟与微波喷泉原子钟的差别,分析了光子反冲的影响,提出利用同向传播和相向传播的两台拉曼原子钟测量精细结构常数。

可满足性问题研究

数理逻辑是计算机科学的基础，而逻辑公式的可满足性问题是计算机科学和人工智能领域中的一个著名而又重要的问题。它在计算机科学和人工智能研究中有广泛的应用。本文将重点介绍实际可用的判定算法及其相关技术。 本文的研究分两大方向，分别是命题逻辑的可满足性问题研究和一阶逻辑的可满足性问题研究。命题逻辑的可满足性问题（Satisfiability Problem）是一个历史悠久的问题，一般简称为 SAT问题。SAT 问题的求解算法有两大类，分别是确定性算法和非确定性算法。本文只研究确定性算法的相关内容，尤其是如何进行剪枝。我们充分调研了SAT求解算法和求解工具的相关知识，在此基础上，提出了local Lemma 这个剪枝技术，该技术可以更加充分地挖掘剪枝信息，达到进行更多剪枝的目的。 在一阶逻辑的可满足性问题研究方面，本文采取直接搜索可行的一阶逻辑模型的方法研究有限论域上的一阶逻辑的可满足性问题。该方法本质上就是深度优先的回溯搜索。因此，我们的研究重点就是如何找到问题的更高效的一阶逻辑的表示以及如何采用启发式的方式进行剪枝。在这个问题上，我的主要工作有两个：一个是模型搜索中适用于谓词的同构消去技术，包括Row by Row策略和Ramsey Number 策略两个技术；另一个是 DASH（Decision Assignment Scheme Heuristic），用来在生成有限模型的时候边搜索边消除同构子空间。DASH 能用近乎零代价保证输出的模型都是互不同构的。这两个技术都是基于有限论域中的元素的固有对称性，换言之，就是需要有限论域中的元素是两两可交换的。 在已有的成果的基础上，我们又尝试使用它们去求解一些数学中的实际问题，如拟群拉丁方，有限射影平面，正交拉丁方（组）等。我们给出了在这几个方面的一些尝试和初步结果，包括一个重要的定理和若干效率提高了几个数量级的改进。 值得一提的是，和马菲菲共同提出的横截矩阵（Transversal Matrix）概念是一个新颖的成果，使得正交拉丁方的表示和求解取得了明显的改进。在这个概念的基础上，进一步给出了几个定理，进行了理论上的拓展。实验数据表明，我们的求解途径和技术能有效解决拉丁方相关的问题。

一种非线性的分布式网格资源调价算法

针对网格环境下分布式异步动态调价算法存在均衡价格收敛过程缓慢、调价效率较低的缺点,提出了一种基于市场机制的非线性调价算法。该算法结合了当前超额需求和过去超额需求对资源价格变化的影响,较真实地刻画了需求变化后资源价格的波动过程。实验证明,非线性的调价算法明显地提高了价格收敛速度,降低了调价次数。