sat.rs 11.5 KB
Newer Older
Ranadeep Biswas's avatar
Ranadeep Biswas committed
1
use hashbrown::{HashMap, HashSet};
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
2
3
use std::fs::{File, OpenOptions};

4
5
use std::default::Default;

Ranadeep Biswas's avatar
Ranadeep Biswas committed
6
7
8
use std::process::{Command, Stdio};

use std::path::PathBuf;
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
9
10
11
12
13
14
15
16
17
18
19
20
21

use std::io::BufRead;
use std::io::BufReader;

use std::io::Write;

#[derive(Hash, Ord, PartialOrd, Eq, PartialEq, Clone, Copy, Debug)]
pub enum Edge {
    CO,
    VI,
    WW(usize),
}

22
#[derive(Debug)]
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
23
struct CNF {
24
    clauses: Vec<Vec<(bool, usize)>>,
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
25
26
27
    n_variable: usize,
}

28
29
30
31
32
33
34
35
36
impl Default for CNF {
    fn default() -> Self {
        CNF {
            clauses: vec![Vec::new()],
            n_variable: 0,
        }
    }
}

Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
37
38
39
impl CNF {
    fn add_variable(&mut self, var: usize, sign: bool) {
        self.n_variable = std::cmp::max(self.n_variable, var);
40
        self.clauses.last_mut().unwrap().push((sign, var));
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
41
42
43
    }

    fn finish_clause(&mut self) {
44
        self.clauses.push(Vec::new());
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
45
46
    }

Ranadeep Biswas's avatar
Ranadeep Biswas committed
47
    fn write_to_file(&self, path: &PathBuf) {
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
48
49
50
        let mut file = OpenOptions::new()
            .write(true)
            .create(true)
Ranadeep Biswas's avatar
Ranadeep Biswas committed
51
            .truncate(true)
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
52
53
54
            .open(path)
            .expect("couldn't create");

55
        writeln!(file, "p cnf {} {}", self.n_variable, self.clauses.len())
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
56
            .expect("failed to write parameters");
57
58
59
60
61
62
63
64
65
66
        for clause in self.clauses.iter().rev().skip(1) {
            for (sign, literal) in clause {
                if *sign {
                    write!(file, "{} ", literal).expect("failed to write cnf to file");
                } else {
                    write!(file, "-{} ", literal).expect("failed to write cnf to file");
                }
            }
            writeln!(file, "0").expect("failed to write cnf to file");
        }
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
67
68
69
70
71
72
73
74
75
76
77
78
79
80
    }
}

#[derive(Debug)]
pub struct Sat {
    cnf: CNF,
    edge_variable: HashMap<(Edge, (usize, usize), (usize, usize)), usize>,
    write_variable: HashMap<usize, HashMap<(usize, usize), HashSet<(usize, usize)>>>,
    n_sizes: Vec<usize>,
    transactions: Vec<(usize, usize)>,
}

impl Sat {
    pub fn new(
Ranadeep Biswas's avatar
Ranadeep Biswas committed
81
        n_sizes: &[usize],
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
82
83
        txns_info: &HashMap<(usize, usize), (HashMap<usize, (usize, usize)>, HashSet<usize>)>,
    ) -> Self {
Ranadeep Biswas's avatar
Ranadeep Biswas committed
84
85
        let mut write_variable: HashMap<usize, HashMap<(usize, usize), HashSet<(usize, usize)>>> =
            HashMap::new();
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
86
87
88
89
90
91
92
93
94
95
96
97
98

        for (&transaction1, (ref read_info, write_info)) in txns_info.iter() {
            for &x in write_info.iter() {
                let entry = write_variable.entry(x).or_insert_with(Default::default);
                entry.entry(transaction1).or_insert_with(Default::default);
            }
            for (&x, &transaction2) in read_info.iter() {
                let entry1 = write_variable.entry(x).or_insert_with(Default::default);
                let entry2 = entry1.entry(transaction2).or_insert_with(Default::default);
                entry2.insert(transaction1);
            }
        }

Ranadeep Biswas's avatar
Ranadeep Biswas committed
99
        for (_, mut wr_map) in write_variable.iter_mut() {
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
100
101
102
103
104
105
106
107
108
109
110
111
112
113
            wr_map.entry((0, 0)).or_insert_with(Default::default);
        }

        let mut transactions = vec![(0, 0)];

        for (i_node, &n_transaction) in n_sizes.iter().enumerate() {
            for i_transaction in 0..n_transaction {
                transactions.push((i_node + 1, i_transaction));
            }
        }

        Sat {
            cnf: Default::default(),
            edge_variable: HashMap::new(),
Ranadeep Biswas's avatar
Ranadeep Biswas committed
114
115
116
            write_variable,
            n_sizes: n_sizes.to_owned(),
            transactions,
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
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
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
        }
    }

    pub fn session(&mut self) {
        let mut clauses = Vec::new();
        for (i_node, &n_transaction) in self.n_sizes.iter().enumerate() {
            for i_transaction in 1..n_transaction {
                // session orders
                clauses.push(vec![(
                    Edge::VI,
                    (i_node + 1, i_transaction - 1),
                    (i_node + 1, i_transaction),
                    true,
                )])
            }
            clauses.push(vec![(Edge::VI, (0, 0), (i_node + 1, 0), true)]);
        }

        self.add_clauses(&clauses);
    }

    pub fn pre_vis_co(&mut self) {
        let mut clauses = Vec::new();

        for &t1 in self.transactions.iter() {
            for &t2 in self.transactions.iter() {
                if t1 != t2 {
                    // VIS <= CO
                    clauses.push(vec![(Edge::VI, t1, t2, false), (Edge::CO, t1, t2, true)]);

                    // CO total
                    // no cycle
                    clauses.push(vec![(Edge::CO, t1, t2, false), (Edge::CO, t2, t1, false)]);
                    // total
                    clauses.push(vec![(Edge::CO, t1, t2, true), (Edge::CO, t2, t1, true)]);

                    for &t3 in self.transactions.iter() {
                        if t2 != t3 {
                            // CO transitive / CO;CO => CO
                            clauses.push(vec![
                                (Edge::CO, t1, t2, false),
                                (Edge::CO, t2, t3, false),
                                (Edge::CO, t1, t3, true),
                            ]);
                        }
                    }
                }
            }
        }
        self.add_clauses(&clauses);
    }

    pub fn ser(&mut self) {
        let mut clauses = Vec::new();

        for &t1 in self.transactions.iter() {
            for &t2 in self.transactions.iter() {
                if t1 != t2 {
                    // CO <= VIS
                    clauses.push(vec![(Edge::CO, t1, t2, false), (Edge::VI, t1, t2, true)]);
                }
            }
        }
        self.add_clauses(&clauses);
    }

    pub fn vis_transitive(&mut self) {
        let mut clauses = Vec::new();

        for &t1 in self.transactions.iter() {
            for &t2 in self.transactions.iter() {
                if t1 != t2 {
                    for &t3 in self.transactions.iter() {
                        if t2 != t3 {
                            // VI transitive / VI;VI => VI
                            clauses.push(vec![
                                (Edge::VI, t1, t2, false),
                                (Edge::VI, t2, t3, false),
                                (Edge::VI, t1, t3, true),
                            ]);
                        }
                    }
                }
            }
        }
        self.add_clauses(&clauses);
    }

205
    pub fn wr_ww(&mut self) {
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
206
207
208
209
210
        let mut clauses = Vec::new();

        for (&x, ref wr_map) in self.write_variable.iter() {
            for (&u1, ref vs) in wr_map.iter() {
                for &v in vs.iter() {
Ranadeep Biswas's avatar
Ranadeep Biswas committed
211
                    // clauses.push(vec![(Edge::WR(x), u1, v, true)]);
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
                    clauses.push(vec![(Edge::VI, u1, v, true)]);
                }
                for (&u2, _) in wr_map.iter() {
                    if u1 != u2 {
                        clauses.push(vec![(Edge::WW(x), u1, u2, false), (Edge::CO, u1, u2, true)]);
                        clauses.push(vec![
                            (Edge::WW(x), u1, u2, true),
                            (Edge::WW(x), u2, u1, true),
                        ]);
                    }
                }
            }
        }

        self.add_clauses(&clauses);
    }

Ranadeep Biswas's avatar
Ranadeep Biswas committed
229
    pub fn read_atomic(&mut self) {
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
230
231
232
233
234
235
236
237
        let mut clauses = Vec::new();

        for (&x, ref wr_map) in self.write_variable.iter() {
            for (&u, ref vs) in wr_map.iter() {
                for &v in vs.iter() {
                    for (&u1, _) in wr_map.iter() {
                        if u1 != u {
                            clauses
238
                                .push(vec![(Edge::VI, u1, v, false), (Edge::WW(x), u1, u, true)]);
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
                        }
                    }
                }
            }
        }

        self.add_clauses(&clauses);
    }

    pub fn prefix(&mut self) {
        let mut clauses = Vec::new();

        for &t1 in self.transactions.iter() {
            for &t2 in self.transactions.iter() {
                if t1 != t2 {
                    for &t3 in self.transactions.iter() {
                        if t2 != t3 {
                            // CO;VI => VI
                            clauses.push(vec![
                                (Edge::CO, t1, t2, false),
                                (Edge::VI, t2, t3, false),
                                (Edge::VI, t1, t3, true),
                            ]);
                        }
                    }
                }
            }
        }
        self.add_clauses(&clauses);
    }

    pub fn conflict(&mut self) {
        let mut clauses = Vec::new();
        for (&x, ref wr_map) in self.write_variable.iter() {
            for (&u1, _) in wr_map.iter() {
                for (&u2, _) in wr_map.iter() {
                    if u1 != u2 {
                        clauses.push(vec![(Edge::WW(x), u1, u2, false), (Edge::VI, u1, u2, true)]);
                    }
                }
            }
        }
        self.add_clauses(&clauses);
    }

Ranadeep Biswas's avatar
Ranadeep Biswas committed
284
    pub fn solve(&self, path: &PathBuf) -> bool {
Ranadeep Biswas's avatar
Ranadeep Biswas committed
285
286
287
        let inp_cnf = path.join("history.cnf");
        let out_cnf = path.join("result.cnf");
        self.cnf.write_to_file(&inp_cnf);
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
288

Ranadeep Biswas's avatar
Ranadeep Biswas committed
289
        if let Ok(mut child) = Command::new("minisat")
Ranadeep Biswas's avatar
Ranadeep Biswas committed
290
291
            .arg(&inp_cnf)
            .arg(&out_cnf)
Ranadeep Biswas's avatar
Ranadeep Biswas committed
292
293
294
295
296
297
298
            .stdout(Stdio::null())
            .spawn()
        {
            child.wait().expect("failed to execute process");
        } else {
            panic!("failed to execute process")
        }
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
299
300
301
302
303

        // println!("status: {}", output.status);
        // println!("stdout: {}", String::from_utf8_lossy(&output.stdout));
        // println!("stderr: {}", String::from_utf8_lossy(&output.stderr));

Ranadeep Biswas's avatar
Ranadeep Biswas committed
304
        let result = File::open(&out_cnf).expect("file couldn't open");
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337

        let reader = BufReader::new(&result);

        let mut lines = reader.lines().map(|l| l.unwrap());

        let mut assignments = HashMap::new();

        match lines.next() {
            Some(ref e) if e.as_str() == "SAT" => {
                for line in lines {
                    for var_st in line.split_whitespace() {
                        let var: isize = var_st.parse().unwrap();
                        if var != 0 {
                            assignments.insert(var.abs() as usize, var > 0);
                        }
                    }
                }
            }
            Some(ref e) if e.as_str() == "UNSAT" => {
                // println!("{:?}", e);
                // for line in lines {
                //     println!("{}", line);
                // }
            }
            _ => {
                unreachable!();
            }
        }

        if !assignments.is_empty() {
            let mut edges: Vec<_> = self
                .edge_variable
                .iter()
Ranadeep Biswas's avatar
Ranadeep Biswas committed
338
                .filter(|(_, &v)| assignments[&v])
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
339
340
341
342
343
                .map(|(&k, _)| k)
                .collect();

            edges.sort_unstable();

Ranadeep Biswas's avatar
Ranadeep Biswas committed
344
345
346
347
348
            for e in &edges {
                if e.0 == Edge::CO {
                    println!("{:?}", e);
                }
            }
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
349
350
351
352
353
354
355

            true
        } else {
            false
        }
    }

Ranadeep Biswas's avatar
Ranadeep Biswas committed
356
    pub fn add_clause(&mut self, edges: &[(Edge, (usize, usize), (usize, usize), bool)]) {
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
357
        for edge in edges.iter() {
Ranadeep Biswas's avatar
Ranadeep Biswas committed
358
359
            let variable = self.get_variable(edge.0, edge.1, edge.2);
            self.cnf.add_variable(variable, edge.3);
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
360
361
362
363
        }
        self.cnf.finish_clause();
    }

Ranadeep Biswas's avatar
Ranadeep Biswas committed
364
    pub fn add_clauses(&mut self, clauses: &[Vec<(Edge, (usize, usize), (usize, usize), bool)>]) {
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
365
366
367
368
369
        for clause in clauses.iter() {
            self.add_clause(clause);
        }
    }

Ranadeep Biswas's avatar
Ranadeep Biswas committed
370
    pub fn get_variable(&mut self, edge: Edge, u: (usize, usize), v: (usize, usize)) -> usize {
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
371
        let usable = self.edge_variable.len() + 1;
Ranadeep Biswas's avatar
Ranadeep Biswas committed
372
        *self.edge_variable.entry((edge, u, v)).or_insert(usable)
Ranadeep Biswas's avatar
update    
Ranadeep Biswas committed
373
374
    }
}