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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
#ifndef _checker_hpp_INCLUDED
#define _checker_hpp_INCLUDED
#include "tracer.hpp" // Alphabetically after 'checker'.
#include <cstdint>
namespace CaDiCaL {
/*------------------------------------------------------------------------*/
// This checker implements an online forward DRUP proof checker enabled by
// 'opts.checkproof' (requires 'opts.check' also to be enabled). This is
// useful for model basted testing (and delta-debugging), where we can not
// rely on an external proof checker such as 'drat-trim'. We also do not
// have yet a flow for offline incremental proof checking, while this
// checker here can also be used in an incremental setting.
//
// In essence the checker implements is a simple propagation online SAT
// solver with an additional hash table to find clauses fast for
// 'delete_clause'. It requires its own data structure for clauses
// ('CheckerClause') and watches ('CheckerWatch').
//
// In our experiments the checker slows down overall SAT solving time by a
// factor of 3, which we contribute to its slightly less efficient
// implementation.
/*------------------------------------------------------------------------*/
struct CheckerClause {
CheckerClause *next; // collision chain link for hash table
uint64_t hash; // previously computed full 64-bit hash
unsigned size; // zero if this is a garbage clause
int literals[2]; // otherwise 'literals' of length 'size'
};
struct CheckerWatch {
int blit;
unsigned size;
CheckerClause *clause;
CheckerWatch () {}
CheckerWatch (int b, CheckerClause *c)
: blit (b), size (c->size), clause (c) {}
};
typedef std::vector<CheckerWatch> CheckerWatcher;
/*------------------------------------------------------------------------*/
class Checker : public StatTracer {
Internal *internal;
// Capacity of variable values.
//
int64_t size_vars;
// For the assignment we want to have an as fast access as possible and
// thus we use an array which can also be indexed by negative literals and
// is actually valid in the range [-size_vars+1, ..., size_vars-1].
//
signed char *vals;
// The 'watchers' and 'marks' data structures are not that time critical
// and thus we access them by first mapping a literal to 'unsigned'.
//
static unsigned l2u (int lit);
std::vector<CheckerWatcher> watchers; // watchers of literals
std::vector<signed char> marks; // mark bits of literals
signed char &mark (int lit);
CheckerWatcher &watcher (int lit);
bool inconsistent; // found or added empty clause
uint64_t num_clauses; // number of clauses in hash table
uint64_t num_garbage; // number of garbage clauses
uint64_t size_clauses; // size of clause hash table
CheckerClause **clauses; // hash table of clauses
CheckerClause *garbage; // linked list of garbage clauses
std::vector<int> unsimplified; // original clause for reporting
std::vector<int> simplified; // clause for sorting
std::vector<int> trail; // for propagation
unsigned next_to_propagate; // next to propagate on trail
void enlarge_vars (int64_t idx);
void import_literal (int lit);
void import_clause (const std::vector<int> &);
bool tautological ();
static const unsigned num_nonces = 4;
uint64_t nonces[num_nonces]; // random numbers for hashing
uint64_t last_hash; // last computed hash value of clause
int64_t last_id;
uint64_t compute_hash (); // compute and save hash value of clause
// Reduce hash value to the actual size.
//
static uint64_t reduce_hash (uint64_t hash, uint64_t size);
void enlarge_clauses (); // enlarge hash table for clauses
void insert (); // insert clause in hash table
CheckerClause **find (); // find clause position in hash table
void add_clause (const char *type);
void collect_garbage_clauses ();
CheckerClause *new_clause ();
void delete_clause (CheckerClause *);
signed char val (int lit); // returns '-1', '0' or '1'
bool clause_satisfied (CheckerClause *);
void assign (int lit); // assign a literal to true
void assume (int lit); // assume a literal
bool propagate (); // propagate and check for conflicts
void backtrack (unsigned); // prepare for next clause
bool check (); // check simplified clause is implied
bool check_blocked (); // check if clause is blocked
struct {
int64_t added; // number of added clauses
int64_t original; // number of added original clauses
int64_t derived; // number of added derived clauses
int64_t deleted; // number of deleted clauses
int64_t assumptions; // number of assumed literals
int64_t propagations; // number of propagated literals
int64_t insertions; // number of clauses added to hash table
int64_t collisions; // number of hash collisions in 'find'
int64_t searches; // number of searched clauses in 'find'
int64_t checks; // number of implication checks
int64_t collections; // garbage collections
int64_t units;
} stats;
public:
Checker (Internal *);
virtual ~Checker ();
void connect_internal (Internal *i) override;
void add_original_clause (int64_t, bool, const std::vector<int> &,
bool = false) override;
void add_derived_clause (int64_t, bool, int, const std::vector<int> &,
const std::vector<int64_t> &) override;
void delete_clause (int64_t, bool, const std::vector<int> &) override;
void finalize_clause (int64_t, const std::vector<int> &) override {
} // skip
void report_status (int, int64_t) override {} // skip
void begin_proof (int64_t) override {} // skip
void add_assumption_clause (int64_t, const std::vector<int> &,
const std::vector<int64_t> &) override;
void print_stats () override;
void dump (); // for debugging purposes only
};
} // namespace CaDiCaL
#endif