合取范式3可满足问题的局部搜索近似算法.pdf

书书书 第 卷 第 期 年 月 计 算 机 学 报 收 稿 日 期 最 终 修 改 稿 收 到 日 期 本 课 题 得 到 国 家 自 然 科 学 基 金 和 教 育 部 博 士 点 基 金 资 助 朱 大 铭 男 年 生 博 士 教 授 博 士 生 导 师 主 要 从 事 算 法 设 计 与 分 析 计 算 分 子 生 物 学 研 究 马 绍 汉 男 年 生 教 授 博 士 生 导 师 主 要 从 事 算 法 设 计 与 分 析 人 工 智 能 研 究 张 平 平 男 年 生 硕 士 工 程 师 主 要 从 事 算 法 设 计 与 分 析 软 件 工 程 研 究 合 取 范 式 可 满 足 问 题 的 局 部 搜 索 近 似 算 法 朱 大 铭 马 绍 汉 张 平 平 山 东 大 学 计 算 机 科 学 技 术 学 院 济 南 摘 要 合 取 范 式 最 大 可 满 足 问 题 是 理 论 计 算 机 科 学 的 核 心 问 题 局 部 搜 索 被 许 多 求 解 实 践 证 明 是 解 答 合 取 范 式 最 大 可 满 足 问 题 十 分 有 效 的 方 法 但 未 见 关 于 局 部 搜 索 算 法 解 答 该 问 题 性 能 分 析 的 结 果 文 中 讨 论 最 大 可 满 足 问 题 的 局 部 搜 索 算 法 并 分 析 算 法 性 能 证 明 问 题 的 一 位 跳 变 局 部 搜 索 算 法 的 近 似 性 能 比 为 证 明 一 位 跳 变 局 部 搜 索 后 跟 有 条 件 全 体 跳 变 算 法 解 答 问 题 的 近 似 性 能 比 为 设 计 一 位 跳 变 加 全 体 跳 变 的 新 局 部 搜 索 算 法 证 明 新 算 法 解 答 问 题 的 近 似 性 能 比 为 将 近 似 局 部 搜 索 算 法 推 广 为 解 答 犽 问 题 的 局 部 搜 索 算 法 证 明 算 法 的 近 似 性 能 比 为 犽 犽 犽 设 计 解 答 犽 问 题 的 两 位 跳 变 局 部 搜 索 算 法 证 明 两 位 跳 变 局 部 搜 索 算 法 的 近 似 性 能 比 为 犽 犽 犽 狀 犽 犽 局 部 搜 索 算 法 经 多 次 运 行 可 进 一 步 提 高 求 解 性 能 文 中 结 果 显 示 局 部 搜 索 算 法 在 合 取 范 式 最 大 可 满 足 问 题 求 解 实 践 中 表 现 出 高 性 能 有 其 必 然 性 关 键 词 算 法 复 杂 性 近 似 性 能 比 可 满 足 性 局 部 搜 索 中 图 法 分 类 号 犇 犗 犐号 犜 犺 犲 犔 狅 犮 犪犾 犛 犲 犪 狉 犮 犺 犃 犾犵 狅 狉犻狋 犺 犿 狊 犳 狅 狉 犕 犪 狓 犻 犿 狌 犿 犛 犪 狋犻狊犳犻犪 犫 犾犻犾犻狋 狔 犘 狉 狅 犫 犾犲 犿 犛 犮 犺 狅 狅 犾 狅 犳 犆 狅 犿 狆 狌 狋犲 狉 犛 犮犻犲 狀 犮 犲 犪 狀 犱 犜 犲 犮 犺 狀 狅 犾 狅 犵 狔 犛 犺 犪 狀 犱 狅 狀 犵 犝 狀 犻 狏 犲 狉 狊犻狋 狔 犑 犻 狀 犪 狀 犃 犫 狊狋狉 犪 犮狋 犽 犽 犽 犽 犽 犽 犽 犽 狀 犽 犽 犓 犲 狔 狑 狅 狉 犱 狊 引 言 合 取 范 式 最 大 可 满 足 问 题 是 理 论 计 算 机 科 学 的 核 心 问 题 由 布 尔 变 量 集 合 与 项 集 合 给 定 的 布 尔 表 达 式 即 是 合 取 范 式 合 取 范 式 最 大 可 满 足 问 题 要 求 计 算 布 尔 变 量 赋 值 使 可 满 足 的 项 数 目 最 大 该 问 题 简 称 为 因 是 且 是 因 此 其 近 似 算 法 和 实 用 算 法 设 计 研 究 成 为 该 问 题 研 究 的 重 心 最 先 设 计 了 解 答 问 题 的 近 似 算 法 并 证 明 算 法 的 近 似 性 能 比 为 证 明 算 法 的 近 似 性 能 比 实 际 为 于 年 给 出 解 答 问 题 的 随 机 算 法 平 均 近 似 性 能 比 为 与 利 用 线 性 规 划 松 弛 法 给 出 一 个 更 为 简 单 的 随 机 近 似 算 法 其 近 似 性 能 比 仍 为 限 制 项 含 有 字 母 数 的 子 问 题 在 问 题 研 究 中 占 有 重 要 位 置 也 是 计 算 机 科 学 工 作 者 最 早 尝 试 讨 论 算 法 与 复 杂 性 所 研 究 的 问 题 之 一 本 文 将 每 个 项 含 有 不 多 于犽个 字 母 的 子 问 题 称 为 犽 问 题 将 每 个 项 含 有 不 少 于 犽个 字 母 的 子 问 题 称 为 犽 问 题 早 在 年 就 设 计 了 犽 问 题 的 组 合 近 似 算 法 近 似 性 能 比 为 犽 犽 实 际 上 为 每 个 布 尔 变 量 以 概 率 随 机 赋 值犜或犉 的 方 法 解 答 犽 的 平 均 近 似 性 能 比 即 为 犽 犽 与 于 年 给 出 了 解 答 问 题 的 近 似 随 机 算 法 他 们 所 采 用 的 半 定 规 划 松 弛 法 突 破 了 原 有 近 似 算 法 的 设 计 进 一 步 提 高 了 算 法 性 能 与 利 用 同 样 方 法 进 一 步 将 算 法 的 近 似 性 能 比 改 进 为 利 用 半 定 规 划 松 弛 法 也 可 适 当 改 进 解 答 问 题 的 算 法 性 能 与 将 解 答 问 题 算 法 的 近 似 性 能 比 改 进 为 与 又 将 算 法 近 似 性 能 比 改 进 为 与 将 归 约 为 得 到 问 题 的 近 似 算 法 又 将 解 答 问 题 的 近 似 性 能 比 改 进 为 并 将 解 答 问 题 的 近 似 性 能 比 改 进 为 另 一 方 面 证 明 若 则 每 个 项 均 含 有 恰 好 个 字 母 的 子 问 题 不 能 多 项 式 时 间 近 似 到 小 于 因 此 若 则 问 题 和 问 题 均 不 能 多 项 式 时 间 近 似 到 小 于 而 为 布 尔 变 量 随 机 赋 值 的 简 单 算 法 解 答 每 个 项 均 含 有 个 字 母 的 子 问 题 恰 好 使 平 均 近 似 性 能 比 达 到 与 给 出 解 答 问 题 的 半 定 规 划 松 弛 法 解 答 可 满 足 实 例 的 近 似 性 能 比 能 够 达 到 后 来 他 们 证 明 该 方 法 解 答 任 意 实 例 的 近 似 性 能 比 也 为 与 又 给 出 了 解 答 问 题 的 半 定 规 划 松 弛 算 法 近 似 性 能 比 为 算 法 是 我 们 所 知 解 答 问 题 性 能 最 好 的 确 定 近 似 算 法 与 给 出 的 半 定 规 划 松 弛 法 是 我 们 所 知 解 答 问 题 性 能 最 好 的 随 机 近 似 算 法 实 际 上 前 述 近 似 算 法 中 仅 有 算 法 为 确 定 算 法 其 他 算 法 均 为 随 机 近 似 算 法 因 此 算 法 近 似 性 能 比 均 为 平 均 近 似 性 能 比 因 为 随 机 算 法 去 随 机 过 程 的 时 间 复 杂 性 太 大 这 些 算 法 的 实 用 性 仍 显 不 足 以 寻 找 问 题 精 确 解 为 目 标 的 实 用 算 法 设 计 研 究 在 求 解 实 践 中 同 样 显 示 出 活 力 这 样 的 算 法 可 分 为 回 溯 搜 索 法 和 局 部 最 优 搜 索 法 两 大 类 回 溯 算 法 要 得 到 精 确 解 总 不 能 摆 脱 指 数 时 间 或 弱 指 数 时 间 复 杂 性 多 数 程 序 设 计 者 更 倾 向 于 采 用 局 部 搜 索 方 法 设 计 解 答 犽 及 犽 问 题 的 求 解 算 法 这 是 因 为 局 部 搜 索 算 法 步 骤 简 单 且 实 际 求 解 经 验 表 明 局 部 搜 索 算 法 的 求 解 性 能 往 往 十 分 理 想 最 早 的 局 部 搜 索 算 法 研 究 可 追 溯 到 计 算 机 学 报 年 与 等 的 求 解 实 验 以 及 与 的 理 论 分 析 问 题 局 部 搜 索 算 法 的 基 本 步 骤 为 随 机 为 布 尔 变 量 赋 初 值 重 复 修 正 部 分 布 尔 变 量 赋 值 以 改 善 当 前 解 质 量 直 到 不 能 修 正 为 止 这 种 局 部 搜 索 算 法 需 要 重 新 选 择 初 始 赋 值 多 次 运 行 才 能 保 证 以 较 大 概 率 获 得 精 确 解 另 一 类 局 部 搜 索 算 法 其 修 正 布 尔 变 量 赋 值 的 步 骤 也 是 随 机 的 可 保 证 算 法 只 需 选 择 一 次 初 始 赋 值 就 可 概 率 为 地 获 得 精 确 解 合 取 范 式 可 满 足 问 题 的 算 法 及 其 复 杂 性 的 其 他 研 究 结 果 可 见 文 献 虽 然 实 践 表 明 局 部 搜 索 算 法 的 求 解 性 能 十 分 理 想 但 未 见 有 人 给 出 过 局 部 搜 索 算 法 解 答 问 题 及 其 子 问 题 的 性 能 分 析 结 果 本 文 研 究 解 答 问 题 的 局 部 搜 索 算 法 并 分 析 算 法 的 求 解 性 能 证 明 一 位 跳 变 局 部 搜 索 算 法 解 答 问 题 的 近 似 性 能 比 为 证 明 一 位 跳 变 加 全 体 跳 变 的 局 部 搜 索 算 法 解 答 问 题 的 近 似 性 能 比 为 在 前 述 性 能 分 析 的 基 础 上 设 计 一 个 解 答 问 题 的 新 局 部 搜 索 算 法 证 明 新 局 部 搜 索 算 法 的 近 似 性 能 比 为 我 们 可 针 对 个 算 法 分 别 给 出 实 例 使 算 法 解 答 它 们 的 近 似 性 能 比 恰 好 达 到 前 面 所 证 明 的 近 似 性 能 比 根 据 的 反 面 结 果 新 算 法 所 能 达 到 的 近 似 性 能 比 是 多 项 式 时 间 能 够 逼 近 问 题 的 最 好 近 似 性 能 比 另 外 可 将 解 答 问 题 的 近 似 局 部 搜 索 算 法 推 广 为 解 答 犽 问 题 的 局 部 搜 索 算 法 近 似 性 能 比 为 犽 犽 犽 最 后 设 计 解 答 犽 问 题 的 两 位 跳 变 局 部 搜 索 算 法 证 明 算 法 近 似 性 能 比 为 犽 犽 犽 狀 犽 犽 本 文 局 部 搜 索 算 法 可 以 运 行 多 次 从 中 寻 找 最 好 的 解 因 为 每 次 运 行 的 近 似 性 能 比 最 大 为 所 以 多 次 运 行 后 算 法 得 到 的 解 往 往 十 分 接 近 最 优 或 已 经 是 最 优 解 算 法 虽 然 解 答 问 题 的 近 似 性 能 比 也 为 但 算 法 每 次 运 行 只 能 得 到 同 样 的 解 随 机 算 法 虽 然 通 过 去 随 机 过 程 可 以 保 证 算 法 能 够 达 到 其 平 均 近 似 性 能 比 但 去 随 机 的 时 间 复 杂 性 太 高 影 响 算 法 的 实 用 性 第 节 给 出 解 答 问 题 的 一 位 跳 变 局 部 搜 索 算 法 证 明 其 近 似 性 能 比 为 第 节 给 出 问 题 的 一 位 跳 变 后 跟 全 体 跳 变 局 部 搜 索 算 法 证 明 其 近 似 性 能 比 为 第 节 仍 然 利 用 一 位 跳 变 和 全 体 跳 变 设 计 解 答 问 题 的 新 局 部 搜 索 算 法 证 明 其 近 似 性 能 比 为 第 节 利 用 解 答 问 题 的 局 部 搜 索 方 法 设 计 解 答 犽 问 题 的 局 部 搜 索 算 法 第 节 分 析 两 位 跳 变 局 部 搜 索 算 法 的 性 能 一 位 跳 变 的 近 似 局 部 搜 索 算 法 问 题 形 式 化 描 述 为 实 例 布 尔 变 量 集 合犝 狌 狌狀 项 集 合 犆 犆 犆犿 每 个 项 均 含 有 不 少 于 个 布 尔 变 量 字 母 犆 狋 狓 狋 狓 狋 犽 狋 其 中狓 狋 犼 狌 狌狀 狌 狌 狀 狋 犿 犼 犽狋 犽狋 询 问 求犝中 布 尔 变 量 的 赋 值犪 犝 犜 犉 最 大 化 犆 狋 犪 狓 狋 犪 狓 狋 犽 狋 犜 在 实 例 中 狌 犻和狌 犻均 被 称 为 布 尔 变 量 字 母 狌 犻 狌 犻 称 为狌 犻 狌犻 的 反 变 量 或 反 变 量 字 母 犻 狀 布 尔 变 量 赋 值 也 称 为 布 尔 变 量 字 母 赋 值 犪 狓 狋 犼 表 示 由犪为犝中 布 尔 变 量 赋 值 后 布 尔 变 量 字 母狓 狋 犼 的 取 值 为 表 述 简 单 我 们 总 是 假 设 每 个 项 含 有 个 布 尔 变 量 字 母 并 只 针 对 这 种 问 题 实 例 给 出 算 法 和 性 能 分 析 适 当 修 改 算 法 即 可 用 于 解 答 那 些 每 个 项 含 有 不 少 于 个 字 母 的 实 例 近 似 性 能 比 分 析 的 结 论 仍 然 成 立 设犝的 赋 值犪使犪 狓 狋 犪 狓 狋 犪 狓 狋 犜 则 称犆狋被犪满 足 下 面 也 直 接 称犆狋 被 满 足 为犆 狋满 足 犆 狋不 被 满 足 为犆狋不 满 足 若 一 个 项 同 时 含 有狌 犻和狌 犻 则 无 论狌 犻怎 样 赋 值 这 个 项 均 被 满 足 因 此 下 面 总 是 假 设 实 例 中 任 意 项 均 不 同 时 含 有狌 犻和狌 犻 定 义 给 定 布 尔 变 量 赋 值犪 犝 若 项犆 狋含 有 布 尔 变 量 字 母狌 犻且犪 狌 犻 犜 或犆 狋含 有 布 尔 变 量 字 母狌 犻且犪 狌 犻 犉 称犆 狋被犪 狌 犻 满 足 若 项犆 狋含 有 布 尔 变 量 字 母狌 犻且犪 狌 犻 犉 或犆 狋含 有 布 尔 变 量 字 母狌 犻且犪 狌 犻 犜 称犆 狋不 被犪 狌 犻 满 足 将犆 狋被 犪 狌犻 满 足 简 记 为犪 犆狋 狌犻 犜 犆狋不 被犪 狌犻 满 足 简 记 为犪 犆 狋 狌犻 犉 若犆 狋不 含 有 布 尔 变 量 字 母狌犻 则 记犪 犆 狋 狌犻 犖 犆狋被犪 狌犻 满 足 则犆狋肯 定 被犪 犝 满 足 考 虑 期朱 大 铭 等 合 取 范 式 可 满 足 问 题 的 局 部 搜 索 近 似 算 法 如 下 的 局 部 搜 索 方 法 先 任 意 选 择犝中 布 尔 变 量 的 赋 值 然 后 选 择 一 个 布 尔 变 量 将 其 赋 值 取 反 以 增 加 犆中 被 满 足 的 项 数 目 重 复 选 择 布 尔 变 量 并 将 赋 值 取 反 的 步 骤 一 直 进 行 到 不 存 在 布 尔 变 量 将 其 赋 值 取 反 可 增 加犆中 被 满 足 的 项 数 目 为 止 将 这 种 方 法 称 为 解 答 问 题 的 一 位 跳 变 算 法 设犆 犼 犜 表 示 被犪 狌 犼 满 足 但 不 被 其 它 布 尔 变 量 赋 值 满 足 的 项 集 合 犆 犼 犉 表 示 不 被犪 狌 犼 满 足 且 不 满 足 的 项 集 合 即犆 犼 犜 犆 狋 犪 犆 狋 狌犼 犜 犪 犆狋 狌狓 犉 犖 狓 犼 犆 犼 犉 犆狋 犪 犆狋 狌犼 犉 犪 犆狋 狌狓 犉 犖 狓 犼 犼 狀 为 布 尔 变 量 赋 值 的 一 位 跳 变 局 部 搜 索 算 法 如 下 算 法 狅 狀 犲 犳 犾犻 狆 犝 犆 犪 狌犽 犚 犪 狀 犱 犜 犉 犽 狀 存 在狌犼 使 犆 犼 犜 犆 犼 犉 犪 狌犼 犪 狌 犼 犪 犝 算 法 中 犚 犪 狀 犱 犜 犉 表 示 随 机 选 择 犜 或 犉 的 函 数 算 法 的 循 环 中 执 行 一 次 语 句 的 变 量 赋 值 取 反 操 作 则犆 犼 犉 中 的 项 由 不 满 足 变 为 满 足 犆 犼 犜 中 的 项 由 满 足 变 为 不 满 足 满 足 的 项 数 目 至 少 增 加 因犆中 只 有犿个 项 能 被 满 足 所 以 算 法 循 环 一 定 能 够 结 束 对 于 每 个 布 尔 变 量 计 算犆 犜 和犆 犉 的 时 间 复 杂 性 为犗 犿 所 以 算 法 在 循 环 中 找 到 一 个狌 犼满 足 犆 犼 犜 犆 犼 犉 的 时 间 复 杂 性 为犗 犿 狀 每 循 环 一 次 被 满 足 的 项 数 目 至 少 增 加 所 以 算 法 时 间 复 杂 性 为 犗 犿 狀 下 面 分 析 算 法 的 性 能 引 理 算 法 结 束 时 得 到 布 尔 变 量 赋 值 犪 犝 对 于 每 个狌犼 犼 狀 总 有 犆 犼 犜 犆 犼 犉 证 明 若 存 在狌 犼 满 足 犆 犼 犜 犆 犼 犉 由 循 环 的 条 件 可 知 算 法 循 环 不 会 结 束 证 毕 引 理 设 算 法 结 束 时 被犪 犝 满 足 的 项 集 合 为犛 犪 则 犛 犪 狀 犼 犆 犼 犜 证 明 设犆 狋 狓 狋 狓 狋 狓 狋 犛 犪 狓 狋 犼 狌 狌狀 狌 狌 狀 犼 若犆 狋中 至 少 有 两 个 布 尔 变 量 字 母 取 值 为犜 则 狓 狋 狓 狋 狓 狋 中 每 个 字 母 赋 值 取 反 犆狋仍 然 满 足 其 它 字 母 赋 值 取 反 不 影 响犆 狋的 可 满 足 性 所 以 由犆 犼 犜 的 定 义 可 知 犆 狋 犆 犼 犜 犼 狀 若犆 狋中 只 有 一 个 布 尔 变 量 字 母 取 值 为犜 不 妨 设犪 狓 狋 犜 则 仅 当狓 狋 赋 值 取 反 时 犆 狋由 满 足 变 为 不 满 足 设狓 狋 狌 犼 狌 犼 则犆 狋 犆 犼 犜 但 对 于狓 犼 犆狋 犆 狓 犜 即犆狋最 多 出 现 在 一 个犆 犼 犜 中 所 以 犛 犪 狀 犼 犆 犼 犜 证 毕 引 理 设 算 法 结 束 时 不 被犪 犝 满 足 的 项 集 合 为犖 犛 犪 则 狀 犼 犆 犼 犉 犖 犛 犪 证 明 我 们 证 明犖 犛 犪 中 的 每 个 项 在 犆 犉 犆 狀 犉 中 至 少 出 现 次 即 任 意犆狋 犖 犛 犪 存 在 至 少 个 正 整 数犼 犼 犼 使犆狋 犆 犼 犉 犆狋 犆 犼 犉 犆狋 犆 犼 犉 设犆 狋 狓 狋 狓 狋 狓 狋 犖 犛 犪 犪 狓 狋 犉 犪 狓 狋 犉 犪 狓 狋 犉 狓 狋 或狓 狋 或狓 狋 赋 值 取 反 犆狋会 由 不 满 足 变 为 满 足 犪 犆 狋 狓 狋 犪 犆 狋 狓 狋 犪 犆狋 狓 狋 犜 设狓 狋 狌犼 狌 犼 狓 狋 狌 犼 狌 犼 狓 狋 狌犼 狌 犼 则犆 狋 犆 犼 犉 犆狋 犆 犼 犉 犆狋 犆 犼 犉 所 以 狀 犼 犆 犼 犉 犖 犛 犪 证 毕 定 理 设 算 法 结 束 时 被犪 犝 满 足 的 项 集 合 为犛 犪 则 犛 犪 犆 证 明 由 引 理 引 理 和 引 理 得 犛 犪 狀 犼 犆 犼 犜 狀 犼 犆 犼 犉 犖 犛 犪 所 以 犆 犛 犪 犖 犛 犪 犛 犪 即 犛 犪 犆 证 毕 由 定 理 可 知 算 法狅 狀 犲 犳 犾犻 狆 解 答 问 题 的 近 似 性 能 比 不 大 于 例 犝 狌 狌 狌 犆 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 当犪 狌 犪 狌 犪 狌 犉时 算 法 狅 狀 犲 犳 犾犻 狆 得 到 一 个 局 部 最 优 解 犆 不 能 被犪 犝 满 足 犆 犆 犆 均 被 满 足 算 法 解 答 这 个 实 例 的 近 似 性 能 比 恰 为 若 实 例 中 某 些 项 含 有 多 于 个 布 尔 变 量 字 母 算 法狅 狀 犲 犳 犾犻 狆 并 不 需 要 任 何 改 计 算 机 学 报 年 变 即 可 解 答 这 样 的 实 例 近 似 性 能 比 仍 为 一 位 跳 变 加 全 体 跳 变 近 似 局 部 搜 索 算 法 一 个 项犆 狋被 满 足 其 中 的 个 布 尔 变 量 字 母 可 能 有 个 字 母 赋 值 为犜 或 有 两 个 字 母 赋 值 为犜 或 有 个 字 母 赋 值 为犜 还 可 观 察 到 前 面 定 义 的 犆 犼 犜 犼 狀 中 仅 含 有 一 个 字 母 赋 值 为犜而 被犪 犝 满 足 的 项 为 更 准 确 地 度 量 被 满 足 的 项 数 目 我 们 根 据 一 个 项 中 含 有 的 被 赋 值 为 犜 的 字 母 数 目 进 一 步 将 项 分 类 定 义 给 定 实 例犝 犆 设 犪 犝 犜 犉 为 布 尔 变 量 赋 值 犆狋 犆为 任 意 含 有 犽狋 个 字 母 的 项 对 于犼 犼 犽狋 若犆狋中 有犼 个 布 尔 变 量 字 母 赋 值 为犜 另 外 字 母 赋 值 为犉 则 称 犆狋关 于犪 犝 是犼 满 足 的 一 个 项 是 满 足 即 这 个 项 不 被 满 足 一 个 项 是 犼 满 足 的 则 这 个 项 肯 定 被 满 足 若 一 个 项 含 有 的 所 有 布 尔 变 量 字 母 均 被 赋 值 为犜 则 称 这 个 项 为 全 满 足 的 若 一 个 项 被 满 足 但 不 是 全 满 足 的 则 称 这 个 项 为 半 满 足 的 利 用 全 满 足 和 不 满 足 的 项 可 以 因 布 尔 变 量 赋 值 全 体 跳 变 而 相 互 转 化 可 给 出 解 答 问 题 性 能 更 好 的 算 法 下 面 仍 然 假 设 每 个 项 总 含 有 个 布 尔 变 量 字 母 设犪 犝 为犝的 赋 值 仍 然 设犛 犪 和犖 犛 犪 分 别 表 示 被犪 犝 满 足 和 不 被犪 犝 满 足 的 项 集 合 其 中 设犛 犪 犛 犪 犛 犪 分 别 表 示 关 于犪 犝 是 满 足 满 足 和 满 足 的 项 集 合 显 然犛 犪 犛 犪 犛 犪 犛 犪 引 理 任 给 布 尔 变 量 赋 值犪 犝 犪 犝 是 犪 犝 中 每 个 布 尔 变 量 赋 值 均 取 反 得 到 的 布 尔 变 量 赋 值 则犛 犪 犛 犪 犛 犪 犛 犪 犛 犪 犖 犛 犪 犖 犛 犪 犛 犪 证 明 考 察犆 狋 狓 狋 狓 狋 狓 狋 若犆 狋 犛 犪 不 妨 设犪 犆 狋 狓 狋 犜 则 犪 犆狋 狓 狋 犉 犪 犆狋 狓 狋 犉 将犝中 布 尔 变 量 赋 值 全 部 取 反 得 到犪 犆 狋 狓 狋 犉 犪 犆 狋 狓 狋 犜 犪 犆 狋 狓 狋 犜 所 以犆 狋关 于犪 犝 是 满 足 的 每 个 关 于犪 犝 为 满 足 的 项 均 可 由 关 于犪 犝 为 满 足 的 项 其 布 尔 变 量 赋 值 取 反 得 到 所 以犛 犪 犛 犪 同 理 可 证 犛 犪 犛 犪 犛 犪 犖 犛 犪 犖 犛 犪 犛 犪 证 毕 推 论 任 给 布 尔 变 量 赋 值犪 犝 则 必 有 犛 犪 犖 犛 犪 或 犛 犪 犖 犛 犪 证 明 若 犛 犪 犖 犛 犪 则 结 论 成 立 否 则 由 引 理 的 结 论 立 即 得 到 犛 犪 犖 犛 犪 犛 犪 犖 犛 犪 证 毕 由 引 理 和 推 论 可 以 在 一 位 跳 变 局 部 搜 索 结 束 后 利 用 所 有 布 尔 变 量 赋 值 全 部 取 反 进 一 步 改 善 算 法 性 能 算 法 犪 犾犾 犳 犾犻 狆 犝 犆 调 用狅 狀 犲 犳 犾犻 狆 犝 犆 得 到 布 尔 变 量 赋 值犪 犝 犛 犪 犖 犛 犪 犫 犝 犪 犝 犫 犝 犪 犝 犫 犝 因 为 算 法狅 狀 犲 犳 犾犻 狆 一 定 结 束 所 以 该 算 法 也 必 定 结 束 调 用狅 狀 犲 犳 犾犻 狆 得 到 布 尔 变 量 赋 值 犪 犝 计 算犛 犪 犛 犪 犛 犪 犖 犛 犪 的 时 间 复 杂 性 为犗 犿 所 以 执 行 算 法 步 的 时 间 复 杂 性 为犗 犿 所 以 算 法 时 间 复 杂 性 与狅 狀 犲 犳 犾犻 狆 的 时 间 复 杂 性 相 同 为犗 犿 狀 犿 狀分 别 为 实 例 中 项 数 目 和 布 尔 变 量 数 目 下 面 分 析 算 法犪 犾犾 犳 犾犻 狆 的 性 能 引 理 设 算 法犪 犾犾 犳 犾犻 狆 得 到 的 布 尔 变 量 赋 值 为犫 犝 则 犛 犫 犛 犫 犖 犛 犫 证 明 设 调 用 算 法狅 狀 犲 犳 犾犻 狆 得 到 的 布 尔 变 量 赋 值 为犪 犝 由犆 犼 犜 的 定 义 可 知 对 于 任 意 犼 犼 狀 有犛 犪 犆 犼 犜 且犛 犪 犆 犼 犜 犛 犪 中 的 每 个 项 包 含 在 一 个 且 仅 一 个犆 犼 犜 中 所 以 引 理 的 结 论 可 更 确 切 地 表 示 为 犛 犪 狀 犼 犆 犼 犜 即 犛 犪 犛 犪 狀 犼 犆 犼 犜 因 此 由 定 理 的 证 明 可 得 到 犛 犪 犛 犪 犖 犛 犪 由 引 理 和 推 论 知 犛 犫 犛 犫 犛 犪 犛 犪 犖 犛 犪 犖 犛 犫 所 以 犛 犫 犛 犫 犖 犛 犫 证 毕 定 理 设 算 法犪 犾犾 犳 犾犻 狆 得 到 的 布 尔 变 量 赋 值 为犫 犝 犛 犫 和犖 犛 犫 为 被犫 犝 满 足 和 不 被 犫 犝 满 足 的 项 集 合 则 犛 犫 犆 期朱 大 铭 等 合 取 范 式 可 满 足 问 题 的 局 部 搜 索 近 似 算 法 证 明 由 算 法 步 的 条 件 语 句 和 推 论 可 知 犛 犫 犖 犛 犫 由 引 理 犛 犫 犛 犫 犖 犛 犫 所 以 犛 犫 犛 犫 犛 犫 犛 犫 犖 犛 犫 所 以 犛 犫 犆 证 毕 由 定 理 可 知 算 法犪 犾犾 犳 犾犻 狆 的 近 似 性 能 比 为 例 犝 狌 狌 狌 犆 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 当犪 狌 犪 狌 犪 狌 犉时 算 法犪 犾犾 犳 犾犻 狆 得 到 一 个 局 部 最 优 解 犆 不 被犪 犝 满 足 犆 犆 犆 和犆 均 被犪 犝 满 足 算 法 解 答 这 个 实 例 的 近 似 性 能 比 恰 为 若 实 例 中 存 在 含 有 多 于 个 字 母 的 项 则 在 算 法犪 犾犾 犳 犾犻 狆 中 应 比 较 全 满 足 与 不 满 足 的 项 数 目 决 定 是 否 将 所 有 布 尔 变 量 赋 值 取 反 所 有 布 尔 变 量 赋 值 有 条 件 取 反 的 步 骤 使 得 全 满 足 项 的 数 目 不 少 于 不 满 足 项 的 数 目 且 不 改 变 半 满 足 项 的 数 目 半 满 足 的 项 数 目 仍 然 不 少 于 不 满 足 项 数 目 的 倍 所 以 算 法 解 答 这 种 实 例 的 近 似 性 能 比 仍 不 大 于 一 位 跳 变 加 全 体 跳 变 近 似 局 部 搜 索 算 法 前 面 算 法 考 虑 的 布 尔 变 量 赋 值 所 满 足 的 项 仍 然 未 能 包 括 满 足 的 项 下 面 假 设 每 个 项 均 含 有 个 布 尔 变 量 字 母 我 们 利 用 一 位 跳 变 最 大 化 满 足 和 满 足 项 集 合 的 局 部 搜 索 方 法 改 善 算 法 性 能 给 定 布 尔 变 量 赋 值犪 犝 选 择 任 意 一 个 布 尔 变 量 赋 值 取 反 任 意 项犆 狋的 可 满 足 性 变 化 有 如 下 性 质 若犆 狋 犖 犛 犪 则犆 狋仍 为 不 满 足 或 变 为 满 足 不 可 能 变 为 满 足 或 满 足 若犆 狋 犛 犪 则犆 狋仍 为 满 足 或 变 为 满 足 或 不 满 足 不 可 能 变 为 满 足 若犆 狋 犛 犪 则犆 狋仍 为 满 足 或 变 为 满 足 或 满 足 不 可 能 变 为 不 满 足 若犆 狋 犛 犪 则犆 狋仍 为 满 足 或 变 为 满 足 不 可 能 变 为 满 足 或 不 满 足 由 此 设犆 犼 表 示 将犪 狌 犼 取 反 由 不 满 足 变 为 满 足 的 项 集 合 犆 犼 表 示 将犪 狌 犼 取 反 由 满 足 变 为 不 满 足 的 项 集 合 犆 犼 表 示 将犪 狌犼 取 反 由 满 足 变 为 满 足 的 项 集 合 犆 犼 表 示 将犪 狌 犼 取 反 由 满 足 变 为 满 足 的 项 集 合 即 犆 犼 犆狋 犆狋 犖 犛 犪 犪 犆狋 狌犼 犉 犆 犼 犆狋 犆狋 犛 犪 犪 犆狋 狌犼 犜 犆 犼 犆狋 犆狋 犛 犪 犪 犆狋 狌犼 犉 犆 犼 犆狋 犆狋 犛 犪 犪 犆狋 狌犼 犜 其 中 犼 狀 一 个 布 尔 变 量 赋 值 取 反 跳 变 最 大 化 满 足 和 满 足 项 集 合 的 算 法 如 下 算 法 狅 狀 犲 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 犝 犆 犪 狌犽 犚 犪 狀 犱 犜 犉 犽 狀 存 在狌犼 使 犆 犼 犆 犼 犆 犼 犆 犼 犪 狌犼 犪 狌 犼 犪 犝 算 法 的 循 环 中 执 行 一 次 语 句 的 变 量 赋 值 取 反 操 作 则犆 犼 中 的 项 由 不 满 足 变 为 满 足 犆 犼 中 的 项 由 满 足 变 为 满 足 犆 犼 中 的 项 由 满 足 变 为 不 满 足 犆 犼 中 的 项 由 满 足 变 为 满 足 满 足 与 满 足 的 项 数 目 之 和 至 少 增 加 因犆中 只 有犿个 项 所 以 算 法 循 环 一 定 能 够 结 束 对 于 每 个 布 尔 变 量 计 算 犆 犼 的 时 间 复 杂 性 为犗 犿 所 以 算 法 在 循 环 中 找 到 一 个狌 犼满 足 犆 犼 犆 犼 犆 犼 犆 犼 的 时 间 复 杂 性 为犗 犿 狀 每 循 环 一 次 满 足 和 满 足 的 项 数 目 至 少 增 加 所 以 算 法 时 间 复 杂 性 为犗 犿 狀 下 面 再 分 析 算 法 的 性 能 引 理 设 算 法狅 狀 犲 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 犝 犆 得 到 布 尔 变 量 赋 值犪 犝 则 对 于 任 意狌 犼 有 犆 犼 犆 犼 犆 犼 犆 犼 证 明 若 存 在狌 犼 满 足 犆 犼 犆 犼 犆 犼 犆 犼 由 算 法 的 循 环 条 件 可 知 循 环 不 会 结 束 证 毕 引 理 设 算 法 结 束 时 得 到 布 尔 变 量 赋 值 犪 犝 则 犛 犪 犛 犪 狀 犼 犆 犼 狀 犼 犆 犼 证 明 设犆 狋 狓 狋 狓 狋 狓 狋 狓 狋 犼 狌 狌狀 狌 狌 狀 犼 若犆 狋 犛 犪 不 失 一 般 性 设犪 狓 狋 犜 犪 狓 狋 犪 狓 狋 犉 当 且 仅 当狓 狋 赋 值 取 反 时 犆狋变 为 不 满 足 其 它 布 尔 变 量 赋 值 取 反 犆 狋仍 为 满 足 或 计 算 机 学 报 年 变 为 满 足 设狓 狋 狌 犼 狌 犼 则犆 狋 犆 犼 但 对 于狓 犼 犆 狋 犆 狓 即犆 狋出 现 在 一 个 且 仅 一 个犆 犼 中 所 以 犛 犪 狀 犼 犆 犼 同 理 可 证 犛 犪 狀 犼 犆 犼 即 有 犛 犪 犛 犪 狀 犼 犆 犼 狀 犼 犆 犼 证 毕 引 理 设 算 法 结 束 时 得 到 布 尔 变 量 赋 值 犪 犝 则 犛 犪 犖 犛 犪 狀 犼 犆 犼 狀 犼 犆 犼 证 明 我 们 证 明 任 意犆 狋 犖 犛 犪 存 在 个 且 仅 个 正 整 数 犼 犼 犼 使犆 狋 犆 犼 犆 狋 犆 犼 犆狋 犆 犼 设犆 狋 狓 狋 狓 狋 狓 狋 犖 犛 犪 犪 狓 狋 犪 狓 狋 犪 狓 狋 犉 只 有 狓 狋 或狓 狋 或狓 狋 赋 值 取 反 犆狋会 由 不 满 足 变 为 满 足 即犪 犆 狋 狓 狋 犪 犆 狋 狓 狋 犪 犆狋 狓 狋 犜 设狓 狋 狌犼 狌 犼 狓 狋 狌 犼 狌 犼 狓 狋 狌 犼 狌 犼 则犆 狋 犆 犼 犆狋 犆 犼 犆狋 犆 犼 而 对 于 任 意狓 犼 犼 犼 有犪 犆 狋 狌狓 犪 犆 狋 狌 狓 犖 所 以犆 狋 犆 狓 所 以 狀 犼 犆 犼 犖 犛 犪 同 理 可 证 狀 犼 犆 犼 犛 犪 所 以 狀 犼 犆 犼 狀 犼 犆 犼 犖 犛 犪 犛 犪 证 毕 定 理 设 算 法 结 束 时 得 到 布 尔 变 量 赋 值 犪 犝 则 犛 犪 犛 犪 犖 犛 犪 犛 犪 证 明 由 引 理 引 理 和 引 理 得 犛 犪 犛 犪 狀 犼 犆 犼 狀 犼 犆 犼 狀 犼 犆 犼 狀 犼 犆 犼 犖 犛 犪 犛 犪 犖 犛 犪 犛 犪 定 理 得 证 证 毕 由 定 理 若 犛 犪 犖 犛 犪 则 算 法狅 狀 犲 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 得 到 的 解 犪 犝 使 满 足 与 满 足 的 项 数 目 之 和 至 少 为 不 满 足 项 数 目 的 倍 但 若 犛 犪 犖 犛 犪 如 犛 犪 则 算 法 得 到 的 解 只 能 保 证 满 足 和 满 足 的 项 数 目 不 少 于 不 满 足 项 数 目 的 倍 在 算 法 中 增 加 所 有 布 尔 变 量 赋 值 有 条 件 取 反 的 步 骤 可 使 算 法 的 近 似 性 能 比 达 到 算 法 犪 犾犾 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 犝 犆 调 用狅 狀 犲 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 犝 犆 得 到 布 尔 变 量 赋 值 犪 犝 犛 犪 犖 犛 犪 犫 犝 犪 犝 犫 犝 犪 犝 犫 犝 该 算 法 的 时 间 复 杂 性 仍 为犗 犿 狀 我 们 不 再 具 体 分 析 算 法 的 时 间 复 杂 性 引 理 设 算 法犪 犾犾 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 得 到 的 布 尔 变 量 赋 值 为犫 犝 则 犛 犫 犖 犛 犫 证 明 观 察 算 法犪 犾犾 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 的 步 由 引 理 和 推 论 即 得 犛 犫 犖 犛 犫 定 理 设 算 法犪 犾犾 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 得 到 的 布 尔 变 量 赋 值 为犫 犝 则 犛 犫 犆 证 明 设 调 用 算 法狅 狀 犲 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 得 到 的 布 尔 变 量 赋 值犪 犝 由 引 理 和 推 论 得 犛 犫 犛 犫 犛 犪 犛 犪 由 引 理 犖 犛 犫 犛 犫 犖 犛 犫 所 以 由 定 理 我 们 得 到 犛 犫 犛 犫 犛 犫 犛 犫 犛 犫 犖 犛 犫 犛 犫 犖 犛 犫 所 以 犛 犫 犆 证 毕 定 理 说 明 算 法犪 犾犾 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 的 近 似 性 能 比 为 例 设犝 狌 狌 狌 狌 狌 狌 犆 犆 犆 犆 犆 犆 犆 犆 犆 犆 犆 犆 犆 犆 犆 犆 犆 每 个 项 的 布 尔 变 量 字 母 集 表 示 如 下 犖 犛 犪 犆 狌 狌 狌 犆 狌 狌 狌 犛 犪 犆 狌 狌 狌 犆 狌 狌 狌 犛 犪 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犛 犪 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 犆 狌 狌 狌 当犪 狌 犪 狌 犪 狌 犪 狌 犪 狌 犪 狌 犉时 算 法 得 到 局 部 最 优 解 犖 犛 犪 犆 犆 犛 犪 犆 犆 犛 犪 犆 但 算 法 的 最 优 解 可 使 所 有 项 都 被 满 足 算 法 解 答 这 个 实 期朱 大 铭 等 合 取 范 式 可 满 足 问 题 的 局 部 搜 索 近 似 算 法 例 的 近 似 性 能 比 恰 为 若 实 例 中 存 在 含 有 多 于 个 字 母 的 项 则 在 算 法狅 狀 犲 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 中 应 利 用 一 位 跳 变 最 大 化 半 满 足 的 项 从 而 可 证 明 局 部 最 优 解 得 到 的 布 尔 变 量 赋 值 所 产 生 的 半 满 足 项 数 目 不 少 于 全 满 足 和 不 满 足 项 数 目 总 和 的 倍 因 此 在 算 法 犪 犾犾 犳 犾犻 狆 犿 犪 狓 狊 犪 狋 中 应 比 较 全 满 足 与 不 满 足 的 项 数 目 决 定 是 否 将 所 有 布 尔 变 量 赋 值 取 反 所 有 布 尔 变 量 赋 值 有 条 件 取 反 的 步 骤 使 得 全 满 足 项 的 数 目 不 少 于 不 满 足 项 的 数 目 且 不 改 变 半 满 足 的 项 数 目 因 此 半 满 足 项 与 全 满 足 项 数 目 之 和 不 少 于 不 满 足 项 数 目 的 倍 算 法 近 似 性 能 比 仍 不 大 于 犕 犪 狓 犽 犛 犪狋问 题 犽 犽 近 似 算 法 每 个 项 均 含 有 不 少 于犽个 布 尔 变 量 字 母 的 子 问 题 即 为 犽 问 题 不 难 推 知 算 法狅 狀 犲 犳 犾犻 狆 解 答 问 题 的 近 似 性 能 比 为 解 答 问 题 的 近 似 性 能 比 为 算 法犪 犾犾 犳 犾犻 狆 解 答 问 题 的 近 似 能 比 为 本 节 考 虑犽 的 情 况 利 用 类 似 于 解 答 问 题 的 局 部 搜 索 方 法 给 出 解 答 犽 问 题 的 一 位 跳 变 后 跟 全 体 跳 变 的 局 部 搜 索 算 法 使 其 近 似 性 能 比 达 到 犽 犽 下 面 总 假 设犽 且 假 设 犽 问 题 实 例 中 每 个 项 均 含 有犽个 布 尔 变 量 字 母 不 再 讨 论 实 例 中 存 在 含 有 多 于犽个 字 母 项 的 情 况 设犆 狋 狓 狋 狓 狋 狓 狋 犽 给 定 布 尔 变 量 赋 值犪 犝 延 用 前 面 项 关 于 被 布 尔 变 量 赋 值 犼 满 足 的 概 念 犼 犽 其 中 满 足 为 不 满 足 犽 满 足 为 全 满 足 犽 满 足 均 为 半 满 足 另 设 犛 犪 犼 为 关 于 布 尔 变 量 赋 值犪 犝 是犼 满 足 的 项 集 合 犛 犪 和犖 犛 犪 为 被犪 犝 满 足 和 不 被犪 犝 满 足 的 项 集 合 给 定 犽 问 题 实 例 的 布 尔 变 量 赋 值 犪 犝 一 个 布 尔 变 量 赋 值 取 反 任 意 项犆狋的 可 满 足 性 变 化 有 如 下 性 质 若犆 狋 犖 犛 犪 则犆 狋仍 为 不 满 足 或 变 为 满 足 不 可 能 变 为 犼 满 足 若犆 狋 犛 犪 犼 犼 犽 则犆 狋仍 为犼 满 足 或 变 为 犼 满 足 或 犼 满 足 不 可 能 变 为 犼 狓 满 足 或 犼 狔 满 足 狓 犽 犼 狔 犼 若犆 狋 犛 犪 犽 则犆 狋仍 为犽 满 足 或 变 为 犽 满 足 不 可 能 变 为 犽 狓 满 足 狓 犽 一 个 布 尔 变 量 赋 值 取 反 对 于 满 足 犼 犽 的 犼 犼 满 足 的 项 不 可 能 变 为 不 满 足 或 犽 满 足 不 满 足 或犽 满 足 的 项 也 不 可 能 变 为 犼 满 足 由 此 我 们 仍 然 假 设犆 犼 表 示 将犪 狌 犼 取 反 由 不 满 足 变 为 满 足 的 项 集 合 犆 犼 表 示 将犪 狌 犼 取 反 由 满 足 变 为 不 满 足 的 项 集 合 犆 犼 犽 表 示 将犪 狌 犼 取 反 由 犽 满 足 变 为犽 满 足 的 项 集 合 犆 犼 犽 表 示 将犪 狌 犼 取 反 由犽 满 足 变 为 犽 满 足 的 项 集 合 即 犆 犼 犆狋 犆狋 犖 犛 犪 犪 犆狋 狌犼 犉 犆 犼 犆狋 犆狋 犛 犪 犪 犆狋 狌犼 犜 犆 犼 犽 犆狋 犆狋 犛 犪 犽 犪 犆狋 狌犼 犉 犆 犼 犽 犆 狋 犆狋 犛 犪 犽 犪 犆 狋 狌犼 犜 其 中 犼 狀 下 面 给 出 一 个 布 尔 变 量 赋 值 取 反 跳 变 最 大 化 满 足 至 犽 满 足 的 项 集 合 然 后 所 有 布 尔 变 量 赋 值 有 条 件 取 反 的 算 法 算 法 犳 犾犻 狆 犿 犪 狓 犽 狊 犪 狋 犝 犆 犪 狌犽 犚 犪 狀 犱 犜 犉 犽 狀 存 在狌犼 使 犆 犼 犆 犼 犽 犆 犼 犆 犼 犽 犪 狌犼 犪 狌 犼 犛 犪 犽 犖 犛 犪 犫 犝 犪 犝 犫 犝 犪 犝 犫 犝 在 算 法 循 环 条 件 中 仅 比 较 了 满 足 转 化 为 不 满 足 和 犽 满 足 转 化 为犽 满 足 项 与 不 满 足 转 化 为 满 足 和犽 满 足 转 化 为 犽 满 足 项 的 数 目 这 是 因 为 满 足 至 犽 满 足 的 项 不 可 能 因 一 个 布 尔 变 量 赋 值 取 反 转 化 为 不 满 足 或犽 满 足 反 之 亦 然 算 法 的 循 环 中 执 行 一 次 语 句 的 变 量 赋 值 取 反 操 作 则犆 犼 中 的 项 由 不 满 足 变 为 满 足 犆 犼 犽 中 的 项 由犽 满 足 变 为 犽 满 足 犆 犼 中 的 项 由 满 足 变 为 不 满 足 犆 犼 犽 中 的 项 由 犽 满 足 变 为犽 满 足 犽 满 足 的 项 数 目 至 少 增 加 因犆中 只 有犿个 项 所 以 算 法 循 环 一 定 能 够 结 束 注 意 执 行 一 次 语 句 的 变 量 赋 值 取 反 操 作 满 足 和 犽 满 足 的 项 数 目 未 必 一 定 增 加 这 是 因 为 满 足 的 项 可 能 变 为 满 足 犽 满 足 的 项 可 能 变 为 犽 满 足 对 于 每 个 布 尔 变 量 计 算犆 犼 狓 的 时 间 复 杂 性 为 计 算 机 学 报 年 犗 犽 犿 犼 狀 狓 犽 犽 算 法 在 循 环 中 找 到 一 个狌 犼满 足 犆 犼 犆 犼 犽 犆 犼 犆 犼 犽 的 时 间 复 杂 性 为犗 犽 犿 狀 每 循 环 一 次 犽 满 足 的 项 数 目 至 少 增 加 所 以 算 法 时 间 复 杂 性 为犗 犽 犿 狀 下 面 分 析 算 法 的 近 似 性 能 比 引 理 设 算 法 犳 犾犻 狆 犿 犪 狓 犽 狊 犪 狋 犝 犆 步 的 循 环 结 束 时 得 到 布 尔 变 量 赋 值犪 犝 则 对 于 任 意狌 犼 犆 犼 犆 犼 犽 犆 犼 犆 犼 犽 证 明 若 存 在狌 犼 满 足 犆 犼 犆 犼 犽 犆 犼 犆 犼 犽 由 算 法 循 环 条 件 可 知 循 环 不 会 结 束 证 毕 引 理 给 定 布 尔 变 量 赋 值犪 犝 所 有 布 尔 变 量 赋 值 均 取 反 得 到犪 犝 则犛 犪 犛 犪 犽 犛 犪 犛 犪 犽 犖 犛 犪 犛 犪 犽 犖 犛 犪 犛 犪 犽 证 明 所 有 布 尔 变 量 赋 值 取 反 犼 满 足