实验2：命题逻辑与 SAT 求解

任务 1：DIMACS 读写与结果解释#

规则编号	逻辑公式	DIMACS 子句
1	$S \vee L$	`1 2 0`
2	$S \rightarrow D$	`-1 3 0`
3	$L \rightarrow F$	`-2 4 0`
4	$D \rightarrow P$	`-3 5 0`
5	$F \rightarrow P$	`-4 5 0`
6	$P \rightarrow (D \vee F)$	`-5 3 4 0`
7	$\lnot (D \land F)$	`-3 -4 0`
8	$P$	`5 0`

base.cnf 文件内容如下：

1
c S=1, L=2, D=3, F=4, P=5
2
p cnf 5 8
3
1 2 0
4
-1 3 0
5
-2 4 0
6
-3 5 0
7
-4 5 0
8
-5 3 4 0
9
-3 -4 0
10
5 0

MiniSAT 终端输出如下：

1
❯ minisat base.cnf base_result.txt
2
WARNING: for repeatability, setting FPU to use double precision
3
============================[ Problem Statistics ]=============================
4
|                                                                             |
5
|  Number of variables:             5                                         |
6
|  Number of clauses:               7                                         |
7
|  Parse time:                   0.00 s                                       |
8
|  Eliminated vars:                 4                                           |
9
|  Vars set       :                 1                                           |
10
|  Eliminated clauses:           0.00 Mb                                      |
11
|  Simplification time:          0.00 s                                       |
12
|                                                                             |
13
============================[ Search Statistics ]==============================
14
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
15
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
16
===============================================================================
17
===============================================================================
18
restarts              : 1
19
conflicts             : 0              (-nan /sec)
20
decisions             : 1              (0.00 % random) (inf /sec)
21
propagations          : 1              (inf /sec)
22
conflict literals     : 0              (-nan % deleted)
23
Memory used           : 11.75 MB
24
CPU time              : 0 s
25

26
SATISFIABLE

结果文件如下：

1
SAT
2
1 -2 3 -4 5 0

求解状态表示 SAT 可满足，其中一种可满足的模型为：S, D, P 为真；L, F 为假。

模型中正变量编号代表该变量为真，负变量编号代表该变量为假。

对应的软件配置为：启用服务器模式、数据库后端、持久化功能，不启用本地模式、文件储存后端。

检查八条业务规则：

满足：服务器模式已启用
满足：服务器模式已启用且数据库后端已启用
满足：本地模式未启用
满足：数据库后端已启用且持久化功能已启用
满足：文件存储后端未启用
满足：持久化功能已启用且数据库后端已启用
满足：数据库后端已启用且文件存储后端未启用
满足：持久化功能已启用

server_only.cnf 文件内容如下：

1
c S=1, L=2, D=3, F=4, P=5
2
p cnf 5 9
3
1 2 0
4
-1 3 0
5
-2 4 0
6
-3 5 0
7
-4 5 0
8
-5 3 4 0
9
-3 -4 0
10
5 0
11
1 0

MiniSAT 终端输出如下：

1
❯ minisat server_only.cnf server_only_result.txt
2
WARNING: for repeatability, setting FPU to use double precision
3
============================[ Problem Statistics ]=============================
4
|                                                                             |
5
|  Number of variables:             5                                         |
6
|  Number of clauses:               7                                         |
7
|  Parse time:                   0.00 s                                       |
8
|  Simplification time:          0.00 s                                       |
9
|                                                                             |
10
============================[ Search Statistics ]==============================
11
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
12
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
13
===============================================================================
14
===============================================================================
15
restarts              : 1
16
conflicts             : 0              (-nan /sec)
17
decisions             : 1              (0.00 % random) (inf /sec)
18
propagations          : 5              (inf /sec)
19
conflict literals     : 0              (-nan % deleted)
20
Memory used           : 11.75 MB
21
CPU time              : 0 s
22

23
SATISFIABLE

结果文件如下：

1
SAT
2
1 -2 3 -4 5 0

no_persistence.cnf 文件内容如下：

1
c S=1, L=2, D=3, F=4, P=5
2
p cnf 5 8
3
1 2 0
4
-1 3 0
5
-2 4 0
6
-3 5 0
7
-4 5 0
8
-5 3 4 0
9
-3 -4 0
10
-5 0

MiniSAT 终端输出如下：

1
❯ minisat no_persistence.cnf no_persistence_result.txt
2
WARNING: for repeatability, setting FPU to use double precision
3
============================[ Problem Statistics ]=============================
4
|                                                                             |
5
|  Number of variables:             5                                         |
6
|  Number of clauses:               7                                         |
7
|  Parse time:                   0.00 s                                       |
8
|  Simplification time:          0.00 s                                       |
9
|                                                                             |
10
===============================================================================
11
Solved by simplification
12
restarts              : 0
13
conflicts             : 0              (0 /sec)
14
decisions             : 0              (-nan % random) (0 /sec)
15
propagations          : 4              (4635 /sec)
16
conflict literals     : 0              (-nan % deleted)
17
Memory used           : 11.75 MB
18
CPU time              : 0.000863 s
19

20
UNSATISFIABLE

结果文件如下：

1
UNSAT

版本	求解状态	模型
`base.cnf`	SAT	`1 -2 3 -4 5 0`
`server_only.cnf`	SAT	`1 -2 3 -4 5 0`
`no_persistence.cnf`	UNSAT	/

$\lnot P, D \rightarrow P \vdash \lnot D \\ \lnot P, F \rightarrow P \vdash \lnot F \\ \lnot D, S \rightarrow D \vdash \lnot S \\ \lnot F, L \rightarrow F \vdash \lnot L \\ \lnot S, \lnot L, S \vee L \vdash False \\$
实际使用的规则包括修改后的规则 8 ( $\lnot P$ ), 规则 4 ( $D \rightarrow P$ ), 规则 5 ( $F \rightarrow P$ ), 规则 2 ( $S \rightarrow D$ ), 规则 3 ( $L \rightarrow F$ ), 规则 1 ( $S \vee L$ )
在解决实际软件工程问题中，我们将具体问题建模为对应的 SAT 问题求解，故求解结果需要结合变量语义和约束关系解释，还原为原有的实际问题并加以分析。

任务 2：诚实者与说谎者建模#

变量表：

变量	编号	为真时的含义
A	1	Alice 是诚实者
B	2	Bob 是诚实者
C	3	Carol 是诚实者
D	4	David 是诚实者
E	5	Eve 是诚实者

陈述人	陈述内容	逻辑公式
Alice	Bob 与 David 身份不同	$A \leftrightarrow (B \oplus D)$
Bob	Alice 或 David 中至少一人诚实	$B \leftrightarrow (A \vee D)$
Carol	Alice 是说谎者	$C \leftrightarrow \lnot A$
David	Alice 或 Bob 中至少一人诚实	$D \leftrightarrow (A \vee B)$
Eve	Carol 是诚实者	$E \leftrightarrow C$
/	至少两名诚实者	$(A \vee B \vee C \vee D) \land \\ (A \vee B \vee C \vee E) \land \\ (A \vee B \vee D \vee E) \land \\ (A \vee C \vee D \vee E) \land \\ (B \vee C \vee D \vee E)$
/	至少两名说谎者	$(\lnot A \vee \lnot B \vee \lnot C \vee \lnot D) \land \\ (\lnot A \vee \lnot B \vee \lnot C \vee \lnot E) \land \\ (\lnot A \vee \lnot B \vee \lnot D \vee \lnot E) \land \\ (\lnot A \vee \lnot C \vee \lnot D \vee \lnot E) \land \\ (\lnot B \vee \lnot C \vee \lnot D \vee \lnot E)$

对应的 CNF 为：

1
c A=1, B=2, C=3, D=4, E=5
2
p cnf 5 24
3

4
c Alice
5
-1 2 4 0
6
-1 -2 -4 0
7
1 -2 4 0
33 collapsed lines
8
1 2 -4 0
9

10
c Bob
11
-2 1 4 0
12
2 -1 0
13
2 -4 0
14

15
c Carol
16
-3 -1 0
17
1 3 0
18

19
c David
20
-4 1 2 0
21
4 -1 0
22
4 -2 0
23

24
c Eve
25
-5 3 0
26
-3 5 0
27

28
c 2True
29
1 2 3 4 0
30
1 2 3 5 0
31
1 2 4 5 0
32
1 3 4 5 0
33
2 3 4 5 0
34

35
c 2False
36
-1 -2 -3 -4 0
37
-1 -2 -3 -5 0
38
-1 -2 -4 -5 0
39
-1 -3 -4 -5 0
40
-2 -3 -4 -5 0

输出为

1
❯ minisat task2.cnf task2_result.txt
2
WARNING: for repeatability, setting FPU to use double precision
3
============================[ Problem Statistics ]=============================
4
|                                                                             |
5
|  Number of variables:             5                                         |
6
|  Number of clauses:              24                                         |
7
|  Parse time:                   0.00 s                                       |
8
|  Simplification time:          0.00 s                                       |
9
|                                                                             |
10
============================[ Search Statistics ]==============================
11
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
12
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
13
===============================================================================
14
===============================================================================
15
restarts              : 1
16
conflicts             : 0              (0 /sec)
17
decisions             : 1              (0.00 % random) (788 /sec)
18
propagations          : 5              (3940 /sec)
19
conflict literals     : 0              (-nan % deleted)
20
Memory used           : 11.75 MB
21
CPU time              : 0.001269 s
22

23
SATISFIABLE

运行结果为

1
SAT
2
-1 -2 3 -4 5 0

说明“Carol 与 Eve 是诚实者”为满足要求的一组解。

添加阻塞语句 1 2 -3 4 -5 0 ，再次运行，输出为

1
❯ minisat task2.cnf task2_result.txt
2
WARNING: for repeatability, setting FPU to use double precision
3
============================[ Problem Statistics ]=============================
4
|                                                                             |
5
|  Number of variables:             5                                         |
6
|  Number of clauses:              25                                         |
7
|  Parse time:                   0.00 s                                       |
8
|  Simplification time:          0.00 s                                       |
9
|                                                                             |
10
===============================================================================
11
Solved by simplification
12
restarts              : 0
13
conflicts             : 0              (0 /sec)
14
decisions             : 0              (-nan % random) (0 /sec)
15
propagations          : 4              (4813 /sec)
16
conflict literals     : 0              (-nan % deleted)
17
Memory used           : 11.75 MB
18
CPU time              : 0.000831 s
19

20
UNSATISFIABLE

结果为 UNSAT ，说明解唯一，该问题仅存在一组解。

任务 3：自选场景的 SAT 建模#

以下为 LLM 生成的候选模型与候选方案，尚未由本人独立核验，也未运行 MiniSAT。

1. 本次 LLM 使用记录#

本次实际提供给 LLM 的请求原文为：

1
完成任务3中需要LLM参与的部分，不要进行需要我完成的部分

同时提供了现有报告 2.md 和任务书 实验2_命题逻辑与SAT求解_实验任务.pdf 作为上下文。任务书中任务 3 的生成要求为：从软件配置、测试用例选择、课程冲突或资源分配中选择一个场景；不少于 10 个有业务含义的布尔变量和 15 个 CNF 子句；至少包含依赖、互斥、至少一个、至多一个和条件组合中的三类关系；需求至少允许一个合法方案；生成场景说明、变量含义、编号需求、对应 CNF 和一份候选方案。

以上记录区分了实际提问和附件中的要求，没有将另拟的提示词记为已实际发送的提示词。

2. LLM 生成的场景说明#

选择场景：团队协作平台的软件部署配置。

某团队协作平台支持云端托管和本地部署两种模式，数据库可以选择 PostgreSQL 或 SQLite，并可选配账号认证、单点登录、HTTPS、自动备份、附件上传、病毒扫描、Redis 缓存和后台任务。本模型只考虑这些功能是否启用；数据库选型、功能依赖和安全策略均按下述产品规则约束。

产品约定：内置自动备份仅支持 PostgreSQL，并通过后台任务执行；附件上传必须启用异步病毒扫描，病毒扫描也通过后台任务执行；后台任务使用 Redis 作为队列与缓存服务，而本产品的 Redis 组件不支持与 SQLite 搭配。云端部署上传附件时，还必须启用自动备份。

3. 候选变量表#

变量	编号	为真时的业务含义
$C$	1	采用云端托管模式
$L$	2	采用本地部署模式
$P$	3	使用 PostgreSQL 数据库
$Q$	4	使用 SQLite 数据库
$A$	5	启用账号认证
$S$	6	启用单点登录（SSO）
$T$	7	启用 HTTPS
$B$	8	启用内置自动备份
$U$	9	启用附件上传
$V$	10	启用附件病毒扫描
$R$	11	启用 Redis 队列与缓存服务
$J$	12	启用后台任务

变量为假表示对应模式、数据库或功能未启用。全部 12 个变量均直接具有业务含义，不引入辅助变量。

4. 编号需求与候选 CNF 子句#

用 $C_1,\ldots,C_{16}$ 标记子句；表中的整数按上述变量编号表示文字，末尾的 0 表示子句结束。

需求编号	自然语言需求	命题逻辑公式	对应 CNF 子句	整数编码
R1	云端托管与本地部署必须恰好选择一种。	$(C\vee L)\land(\lnot C\vee\lnot L)$	$C_1=C\vee L$ ； $C_2=\lnot C\vee\lnot L$	`1 2 0`；`-1 -2 0`
R2	PostgreSQL 与 SQLite 必须恰好选择一种。	$(P\vee Q)\land(\lnot P\vee\lnot Q)$	$C_3=P\vee Q$ ； $C_4=\lnot P\vee\lnot Q$	`3 4 0`；`-3 -4 0`
R3	云端托管必须使用 PostgreSQL。	$C\rightarrow P$	$C_5=\lnot C\vee P$	`-1 3 0`
R4	云端托管必须启用 HTTPS。	$C\rightarrow T$	$C_6=\lnot C\vee T$	`-1 7 0`
R5	云端托管必须启用账号认证。	$C\rightarrow A$	$C_7=\lnot C\vee A$	`-1 5 0`
R6	单点登录依赖账号认证。	$S\rightarrow A$	$C_8=\lnot S\vee A$	`-6 5 0`
R7	单点登录必须通过 HTTPS 使用。	$S\rightarrow T$	$C_9=\lnot S\vee T$	`-6 7 0`
R8	内置自动备份要求使用 PostgreSQL。	$B\rightarrow P$	$C_{10}=\lnot B\vee P$	`-8 3 0`
R9	内置自动备份要求启用后台任务。	$B\rightarrow J$	$C_{11}=\lnot B\vee J$	`-8 12 0`
R10	后台任务要求启用 Redis 队列与缓存服务。	$J\rightarrow R$	$C_{12}=\lnot J\vee R$	`-12 11 0`
R11	Redis 队列与缓存服务和 SQLite 不能同时启用。	$\lnot(R\land Q)$	$C_{13}=\lnot R\vee\lnot Q$	`-11 -4 0`
R12	附件上传要求启用病毒扫描。	$U\rightarrow V$	$C_{14}=\lnot U\vee V$	`-9 10 0`
R13	病毒扫描要求启用后台任务。	$V\rightarrow J$	$C_{15}=\lnot V\vee J$	`-10 12 0`
R14	同时采用云端托管并启用附件上传时，必须启用内置自动备份。	$(C\land U)\rightarrow B$	$C_{16}=\lnot C\vee\lnot U\vee B$	`-1 -9 8 0`

候选 CNF 为 $F=\bigwedge_{i=1}^{16}C_i$ ，共 12 个业务变量、14 条自然语言需求、16 个子句。关系类型包括：R1、R2 中的至少一个与至多一个；R11 中的互斥；R3—R10、R12、R13 中的依赖；R14 中的条件组合。

5. LLM 给出的候选方案#

候选业务方案：采用云端托管和 PostgreSQL，启用账号认证、HTTPS、内置自动备份、附件上传、病毒扫描、Redis 队列与缓存服务及后台任务；不采用本地部署或 SQLite，不启用单点登录。

变量	$C$	$L$	$P$	$Q$	$A$	$S$	$T$	$B$	$U$	$V$	$R$	$J$
候选赋值	1	0	1	0	1	0	1	1	1	1	1	1

按变量编号表示的完整候选赋值为：

1
1 -2 3 -4 5 -6 7 8 9 10 11 12 0

这份赋值由 LLM 提供，不是 MiniSAT 的运行输出。

本人仍需完成：整理和独立检查候选模型、必要的修正、候选方案对每条需求与 CNF 的代入检查、最终 DIMACS 文件、MiniSAT 求解及模型的业务解释与需求检查、关键截图，以及自行撰写的编码准确性结论。

LLM 生成内容核对无误，以下为人工部分：

DIMACS 文件：

1
c C=1, L=2, P=3, Q=4, A=5, S=6, T=7, B=8, U=9, V=10, R=11, J=12
2
p cnf 12 16
3

4
1 2 0
5
-1 -2 0
6
3 4 0
7
-3 -4 0
8
-1 3 0
9
-1 7 0
10
-1 5 0
11
-6 5 0
12
-6 7 0
13
-8 3 0
14
-8 12 0
15
-12 11 0
16
-11 -4 0
17
-9 10 0
18
-10 12 0
19
-1 -9 8 0

输出：

1
❯ minisat task3.cnf task3_result.txt
2
WARNING: for repeatability, setting FPU to use double precision
3
============================[ Problem Statistics ]=============================
4
|                                                                             |
5
|  Number of variables:            12                                         |
6
|  Number of clauses:              16                                         |
7
|  Parse time:                   0.00 s                                       |
8
|  Eliminated vars:                12                                           |
9
|  Vars set       :                 0                                           |
10
|  Eliminated clauses:           0.00 Mb                                      |
11
|  Simplification time:          0.00 s                                       |
12
|                                                                             |
13
============================[ Search Statistics ]==============================
14
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
15
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
16
===============================================================================
17
===============================================================================
18
restarts              : 1
19
conflicts             : 0              (-nan /sec)
20
decisions             : 1              (0.00 % random) (inf /sec)
21
propagations          : 0              (-nan /sec)
22
conflict literals     : 0              (-nan % deleted)
23
Memory used           : 11.73 MB
24
CPU time              : 0 s
25

26
SATISFIABLE

运行结果为：

1
SAT
2
-1 2 -3 4 5 -6 7 -8 -9 -10 -11 -12 0

其含义为：采用本地部署模式，使用SQLite数据库，启用账号认证，启用 HTTPS。

CNF 准确表达了需求

任务 4（编程题）：实现 CNF 赋值检查器#

代码补全如下：

1
#include <vector>
2
bool satisfiesCnf(
3
  int variableCount,
4
  const std::vector<std::vector<int>>& clauses,
5
  const std::vector<int>& assignment) {
6
    for(const std::vector<int>& clause : clauses) {
7
      bool sat = false;
8
      for(int i : clause) {
9
        bool sign = (i < 0);
10
        int index = (sign ? -i : i) - 1;
11
        sat |= (assignment[index] ^ sign);
12
        if(sat) break;
13
      }
14
      if(!sat) return false;
15
    }
16
    return true;
17
}

测试代码如下：

1
#include <iostream>
2
#include <vector>
3

4
bool satisfiesCnf(
5
  int variableCount,
6
  const std::vector<std::vector<int>>& clauses,
7
  const std::vector<int>& assignment);
8

9
int main() {
10
  int variableCount, clauseCount;
11
  std::cin >> variableCount >> clauseCount;
12
  std::vector<std::vector<int>> clauses(clauseCount);
13
  std::vector<int> assignment(variableCount);
14
  for(int i = 0; i < clauseCount; i++) {
15
    int var;
16
    while(true) {
17
        std :: cin >> var;
18
        if(var == 0) break;
19
        clauses[i].push_back(var);
20
    }
21
  }
22
  for(int i = 0; i < variableCount; i++) {
23
    std::cin >> assignment[i];
24
  }
25
  std::cout << (
26
    satisfiesCnf(variableCount, clauses, assignment) ? "AC" : "WA"
27
  ) << std::endl;
28
  return 0;
29
}

测试用例如下：

测试点编号	`variableCount`	`clauses`	`assignment`	预期解	返回结果
1	1	`{}`	`x1=true`	AC	AC
2	1	`{{1}}`	`x1=true`	AC	AC
3	1	`{{1}, {-1}}`	`x1=true`	WA	WA
4	2	`{{1, 2}, {-1, -2}}`	`x1=true, x2=true`	WA	WA
5	2	`{{1, 2}, {-1, -2}}`	`x1=true, x2=false`	AC	AC
6	3	`{{-1, 2}, {-2, 3}, {-3, 1}}`	`x1=true, x2=true, x3=true`	AC	AC

使用固定CNF {{1, 2}, {-1, 3}, {-2, -3}} 和赋值 x1=true, x2=false, x3=true 测试结果如下：

1
❯ ./test_lab2
2
3 3
3
1 2 0
4
-1 3 0
5
-2 -3 0
6
1 0 1
7
AC

故返回值为 true，将 x3 改为 false 后测试结果如下：

1
❯ ./test_lab2
2
3 3
3
1 2 0
4
-1 3 0
5
-2 -3 0
6
1 0 0
7
WA

此时cnf子句 -1 3 0 不满足。

CNF中“所有子句均满足”的含义是“对给定的同一组完整赋值，每个子句都至少有一个文字为真时，整个 CNF 才为真；只要有一个子句中的文字全部为假，整个 CNF 就为假。”

任务 5：使用阻塞子句寻找多个解#

方案编号	CNF运行结果	测试策略	加入的阻塞语句	`satisfiesCnf` 检测结果
1	`1 -2 -3 -4 0`	执行单元测试	`-1 2 3 4 0`	AC
2	`-1 2 -3 -4 0`	执行集成测试	`1 -2 3 4 0`	AC
3	`1 2 -3 -4 0`	执行单元测试和集成测试	`-1 -2 3 4 0`	AC
4	`1 2 3 -4 0`	执行单元测试，集成测试和静态分析	`-1 -2 -3 4 0`	AC
5	`1 -2 3 -4 0`	执行单元测试和静态分析	`-1 2 -3 4 0`	AC
6	`-1 2 -3 4 0`	执行集成测试，并收集覆盖率	`1 -2 3 -4 0`	AC
7	`1 2 -3 4 0`	执行单元测试和集成测试，并收集覆盖率	`-1 -2 3 -4 0`	AC
/	`UNSAT`	无测试策略	/	/

若存在其他完整合法赋值，则该组赋值可通过原始CNF，并不会被任何一条阻塞语句排除，最后输出UNSAT则说明不存在这样的赋值组合。

增加业务规则“必须执行静态分析”后，初始cnf如下：

1
c U=1, I=2, S=3, C=4
2
p cnf 4 5
3
1 2 0
4
-3 1 0
5
-4 2 0
6
-3 -4 0
7
3 0

原方案编号	CNF运行结果	测试策略	加入的阻塞语句	`satisfiesCnf` 检测结果
5	`1 -2 3 -4 0`	执行单元测试和静态分析	`-1 2 -3 4 0`	AC
4	`1 2 3 -4 0`	执行单元测试，集成测试和静态分析	`-1 -2 -3 4 0`	AC
/	`UNSAT`	无测试策略	/	/

方案数由修改前的7降为2，原方案1, 2, 3, 6, 7被排除，即所有包含-3的方案被排除。

单个阻塞语句由被阻塞赋值逐项取反得到，这使得其具有针对性：排除这一种赋值组合并不影响其他赋值组合的判断。

任务 6：检查两份 CNF 是否等价#

需求编号	逻辑公式
1	$A \vee W$
2	$A \leftrightarrow D$
3	$W \rightarrow C$
4	$C \rightarrow D$
5	$D \rightarrow L$
6	$M \leftrightarrow L$

运行 encoding_a.cnf 输出如下：

1
❯ minisat encoding_a.cnf encoding_a.txt
2
WARNING: for repeatability, setting FPU to use double precision
3
============================[ Problem Statistics ]=============================
4
|                                                                             |
5
|  Number of variables:             6                                         |
6
|  Number of clauses:               8                                         |
7
|  Parse time:                   0.00 s                                       |
8
|  Eliminated vars:                 4                                           |
9
|  Vars set       :                 2                                           |
10
|  Eliminated clauses:           0.00 Mb                                      |
11
|  Simplification time:          0.00 s                                       |
12
|                                                                             |
13
============================[ Search Statistics ]==============================
14
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
15
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
16
===============================================================================
17
===============================================================================
18
restarts              : 1
19
conflicts             : 0              (0 /sec)
20
decisions             : 1              (0.00 % random) (740 /sec)
21
propagations          : 2              (1480 /sec)
22
conflict literals     : 0              (-nan % deleted)
23
Memory used           : 11.73 MB
24
CPU time              : 0.001351 s
25

26
SATISFIABLE

结果如下：

1
SAT
2
1 -2 3 -4 5 6 0

运行 encoding_b.cnf 输出如下：

1
❯ minisat encoding_b.cnf encoding_b.txt
2
WARNING: for repeatability, setting FPU to use double precision
3
============================[ Problem Statistics ]=============================
4
|                                                                             |
5
|  Number of variables:             6                                         |
6
|  Number of clauses:              12                                         |
7
|  Parse time:                   0.00 s                                       |
8
|  Eliminated vars:                 4                                           |
9
|  Vars set       :                 2                                           |
10
|  Eliminated clauses:           0.00 Mb                                      |
11
|  Simplification time:          0.00 s                                       |
12
|                                                                             |
13
============================[ Search Statistics ]==============================
14
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
15
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
16
===============================================================================
17
===============================================================================
18
restarts              : 1
19
conflicts             : 0              (0 /sec)
20
decisions             : 1              (0.00 % random) (912 /sec)
21
propagations          : 2              (1825 /sec)
22
conflict literals     : 0              (-nan % deleted)
23
Memory used           : 11.73 MB
24
CPU time              : 0.001096 s
25

26
SATISFIABLE

结果如下：

1
SAT
2
1 -2 3 -4 5 6 0

检查函数如下：

1
std::vector<int> check() {
2
  int variableCount = 6;
3
  std::vector<std::vector<int>> encoding_a = {
8 collapsed lines
4
    {1, 2},
5
    {-1, 3},
6
    {-3, 1},
7
    {-2, 4},
8
    {-4, 3},
9
    {-3, 5},
10
    {-6, 5},
11
    {-5, 6}
12
  };
13

14
  std::vector<std::vector<int>> encoding_b = {
12 collapsed lines
15
    {-4, 3},
16
    {-3, 5},
17
    {-6, 5},
18
    {-5, 6},
19
    {1, 2, 4},
20
    {1, 2, -4},
21
    {-1, 3, 6},
22
    {-1, 3, -6},
23
    {-3, 1, 2},
24
    {-3, 1, -2},
25
    {-2, 4, 5},
26
    {-2, 4, -5},
27
  };
28

29
  std::vector<int> assignment(variableCount), diff;
30
  for(int i = 0; i < 64; i ++) {
31
    for(int j = 0; j < variableCount; j++) {
32
      assignment[j] = (i >> j) & 1;
33
    }
34
    if(
35
      satisfiesCnf(variableCount, encoding_a, assignment) !=
36
      satisfiesCnf(variableCount, encoding_b, assignment)
37
    ) diff.push_back(i);
38
  }
39
  return diff;
40
}

运行后返回的 diff 为空，故 encoding_a 与 encoding_b 等价

1
(K OR x) AND (K OR NOT x)
2
≡ K OR (x AND NOT x) (分配律)
3
≡ K OR FALSE (矛盾律)
4
≡ K (恒等律)

删除 B 中 1 2 4 0 子句，并删除检查函数中变量 encoding_b 中元素 {1, 2, 4} ，再次运行检查函数，返回 diff 为 {0, 48}，得到如下结果：

`diff` 内的元素	赋值组合	服务配置	`encoding_a` 中不满足的子句	不满足的需求编号
0	A=false, W=false, D=false, C=false, L=false, M=false	不启用任何业务	`1 2 0`	1
48	A=false, W=false, D=false, C=false, L=true, M=true	启用日志与监控	`1 2 0`	1

语法形式不同的cnf可能在命题逻辑等价性上属于同一等价类，故仍可能表达相同模型集合。