-
Notifications
You must be signed in to change notification settings - Fork 0
/
Trail.cs
99 lines (79 loc) · 2.95 KB
/
Trail.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
using System;
using System.Collections;
using System.Collections.Generic;
using System.Linq;
using System.Text;
namespace SAT_Solver {
public class Trail : IEnumerable<TrailNode> {
private List<TrailNode> list = new List<TrailNode>();
private Dictionary<int, TrailNode> map = new Dictionary<int, TrailNode>();
public string DebugMessage { get; private set; }
public int Count => list.Count;
public TrailNode this[int key] {
get => list[key];
set => list[key] = value;
}
public void Add(TrailNode node) {
list.Add(node);
map.Add(node.Literal.index, node);
}
public void Remove(int index) {
var node = list[index];
list.RemoveAt(index);
map.Remove(node.Literal.index);
}
public TrailNode Find(Literal literal) => map.ContainsKey(literal.index) ? map[literal.index] : null;
public TrailNode FindLatestMatch(Clause clause) {
var set = clause.ToHashSet();
for (int i = list.Count - 1; i >= 0; i--) {
if (set.Contains(this[i].Literal)) {
return this[i];
}
}
throw new Exception("Match not found");
}
public Clause GetUIP(Clause source, out int level) {
DebugMessage = $"Conflict nodes: {string.Join(" ", source.Select(x => Find(x)))}";
var clause = new Clause(source);
int currentLevel = list[Count - 1].Level;
for (int i = Count - 1; i >= 0; i--) {
if (list[i].IsDecision)
break;
if (!HasMultipleTops(clause))
break;
if (clause.Contains(list[i].Literal)) {
clause.Resolution(list[i].Clause);
}
}
level = FindBacktrackLevel(clause);
return clause;
}
public bool HasMultipleTops(Clause clause) {
int count = 0;
foreach (var literal in clause) {
if (map[literal.index].Level == list[Count - 1].Level) {
if (count > 0)
return true;
count++;
}
}
return false;
}
public int FindBacktrackLevel(Clause clause) {
int highest = 0;
int second = 0;
foreach (var literal in clause) {
var node = map[literal.index];
if (node.Level > highest) {
second = highest;
highest = node.Level;
} else if (node.Level > second && node.Level != highest) {
second = node.Level;
}
}
return second;
}
public IEnumerator<TrailNode> GetEnumerator() => list.GetEnumerator();
IEnumerator IEnumerable.GetEnumerator() => GetEnumerator();
}
}