命题逻辑中合取范式 (CNF) 的可满足性问题 (SAT)是当代理论计算机科学的核心问题, 是┅典型的NP 完全问题.在定义可满足性问题SAT之前，先引进一些逻辑符号
一个 SAT 问题是指: 对于给定的 CNF 是否存在一组关于命题变元的真值指派使得A 為真. 显然, 如果A 为真, 则 CNF 的每个子句中必有一个命题变元为 1 (真) 。
Las Vegas 算法是利用随机值做出随机选择的一种概率算法并且不会产生不正确的***。在计算过程中所做出的随机选择可能使算法比其他算法更快地得到所要求的解。
拉斯维加斯算法不会得到不正确的解一旦用拉斯维加斯算法找到一个解，这个解就一定是正确解但有时用拉斯维加斯算法找不到解。与蒙特卡罗算法类似拉斯维加斯算法找到正确解的概率随着它所用的计算时间的增加而提高。对于所求解问题的任一实例用同一拉斯维加斯算法反复对该实例求解足够多次，可使求解失败的概率任意小
Las Vegas 算法用来搜索包含目标结点的解空间。它用一些随机选择来移动而不需要在每个结点都计算一个新的结点。如果荿功结点的比例在解空间中相当高则找到目标结点的概率可能很高。当下一个结点的计算比较困难或者系统化地搜索没有什么必要时采用Las Vegas
算法，会提高计算的效率当然，下一个结点的随机选择有可能导致找不到成功的结点但是我们可以重复多次运行，来提高目标结點的效率拉斯维加斯算法的一个显著特征是它所作的随机性决策有可能导致算法找不到所需的解，但是通过重复多次运行来克服在求解NP难问题时，用它往往会收到奇效
为了测试Las Vegas 的计算效果, 我们用随机产生的3-SAT 模型(每个子句的长度 l= 3, 且子句里的变元兩两不同) 做实例。每种取值执行20次考虑有可能找不到解的情况，当搜索次数超过十万次认为此样例不可满足。得到的结果为：
[1] 张德富.算法设计与分析（高级教程）[M].国防工业出版社2007.