DPLL

1. 数据结构部分：

• 定义了一个名为 _list_iterator 的 C++ 模板类，它表示一个双向链表的迭代器。
• 定义了一个名为 Doubly_Linked_List 的 C++ 模板类，它表示一个双向链表的数据结构

2. 测试时间
3. basic和optimize的两个solution函数

• 单子句传播，找L，有，删除所在子句，有非L，删除文字
• 分类策略 1.选出现次数最多的 2.MOM
• 都满足时-> 子句集为空，返回true
• 含有空子句，返回false
• 都不满足，将分类策略出来的文字并入原子句集，递归，还不行，非文字，递归

Suduku

数独约束条件

1. 每个单元格只能填入1～9之间唯一一个数字，称之为“格约束”

-111 -121 0             前两格不同时为1
-111 -131 0             第1与第3格不同时为1
-111 -141 0             第1与第4格不同时为1
......

code：

// 格约束
for (int i = 0; i < 61; ++i)
{
    //当前格可以填写1-9
    for (int k = 1; k <= 9; ++k)
    {
        outFile << i * 9 + k << " ";
    }
    outFile << "0" << endl;

    //任意两个数字都不能同时成立
    for (int k1 = 1; k1 <= 9; ++k1)
    {
        for (int k2 = k1 + 1; k2 <= 9; ++k2)
        {
            outFile << -(i * 9 + k1) << " " << -(i * 9 + k2) << " 0" << endl;
        }
    }
}

2. 必填数字，例如第一行必填5，利用switch case调试

112 122 132 212 222 232 312 322 332 0   包含2

code:

// 必填数字
for (int i = 5; i <= 5; ++i)
{
    for (const auto position : positions)
    {
        int literal = position * 10 + i; //语义编码的位置
        literal = Natural_Sequence_Encoding(literal); //自然编码
        outFile << literal << " ";
    }
    outFile << "0" << endl;
}

3. 选填数字

311 321 331 341 351 361 371 318 328 338 348 358 368 378 0 --> 1或者8
312 322 332 342 352 362 372 318 328 338 348 358 368 378 0 --> 2或者8
312 322 332 342 352 362 372 319 329 339 349 359 369 379 0 --> 2或者9

code：

// 选填数字
for (int i = rows_length + 1; i <= 9; ++i)
{
    for (int j = i - rows_length; j <= 9 - rows_length; ++j)
    {
        for (const auto position : positions)
        {
            int literal = position * 10 + i;
            literal = Natural_Sequence_Encoding(literal);
            outFile << literal << " ";
        }

        for (const auto position : positions)
        {
            int literal = position * 10 + j;
            literal = Natural_Sequence_Encoding(literal);
            outFile << literal << " ";
        }

        outFile << "0" << endl;
    }
}

4. 任意两个格子不能填写相同数字

-111 -121 0
-111 -131 0
-111 -141 0
-111 -151 0
......

code：

 // 任意两个格子不可以填写相同的数字
 for (int i = 1; i <= 9; ++i)
 {
     for (int index1 = 0; index1 < rows_length; ++index1)
     {
         for (int index2 = index1 + 1; index2 < rows_length; ++index2)
         {
             int literal1 = positions[index1] * 10 + i;
             int literal2 = positions[index2] * 10 + i;
             literal1 = Natural_Sequence_Encoding(literal1);
             literal2 = Natural_Sequence_Encoding(literal2);
             outFile << -literal1 << " " << -literal2 << " 0" << endl;
         }
     }
 }

语义编码转化成自然编码

自然顺序编码：ijn → row_start[i - 1] * 9+(j-1)*9+n
int Natural_Sequence_Encoding(int literal)
{
    int variable = 0;
    int x = literal % 10;

    variable += x;

    literal = literal / 10;
    x = literal % 10;

    variable += (x - 1) * 9;

    x = literal / 10;

    variable += row_start[x - 1] * 9;

    return variable;
}

数度优化

• 分裂策略：优先选择所有子句中最短子句中出现次数较多的（以其正负值相乘作为衡量标准）

• 单子句传播的时候可以一次性读所有单子句，存在数组里

• setting直接引用，不传入数组

• 去掉一个clause副本

优化率：

文件名	基础求解	优化求解	优化率
S\problem3-100.cnf	20096	277	98.6%
basic_eg\performance\sud00009.cnf	172472	275	99.8%
M\bart17.shuffled-231.cnf	null	124	100%
M\problem12-200.cnf	null	7115	100%
M\sud00001.cnf	null	2642	100%
M\sud00009.cnf	null	266	100%
M\sud00079.cnf	550659	4437	99.2%
M\sud00082.cnf	39853	1483	96.3%
M\sud00861.cnf	3839	700	81.7%
S\problem3-100.cnf	19372	308	98.4%
S\problem2-50.cnf	201	0	100%
S\problem8-50.cnf	124	3	97.6%
S\problem11-100.cnf	3639	166	95.4%

问题

1. 自定义数据结构（不用vector）故不能使用find函数（std::find函数要求迭代器具有适当的iterator_category）

2. //如果相反形式不存在
    if(!parser.IsLiteral(*it_clause, -*it_literal)) {
    	pure_literals.insert(abs_literal);
   } //漏了“！”

3. 对空子句的出现不透彻，对分支回溯return false条件不对---导致无解出现有解，不会产生分支

   if ((*it_clause).literals.empty()) {
   	it_clause = clauses.remove_node(it_clause); // 移除整个子句
       continue;
   }

4. int* counter = new int[2 * (bool_num) + 1] {0};//数组变长两倍，但从二维变一维