Skip to content

Latest commit

 

History

History
232 lines (169 loc) · 5.7 KB

README.md

File metadata and controls

232 lines (169 loc) · 5.7 KB
Raw

DPLL

  1. 数据结构部分：
  • 定义了一个名为 _list_iterator 的 C++ 模板类，它表示一个双向链表的迭代器。
  • 定义了一个名为 Doubly_Linked_List 的 C++ 模板类，它表示一个双向链表的数据结构
  1. 测试时间
  2. 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;
        }
    }
}
  1. 必填数字，例如第一行必填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;
}
  1. 选填数字
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;
    }
}
  1. 任意两个格子不能填写相同数字
-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};//数组变长两倍，但从二维变一维