Sfoglia il codice sorgente

use a thread to increase the stack size

(yes, i know this is a hack.  but we can solve the hole6 problem now,
without having to think further. :)
Lucas Stadler 10 anni fa
parent
commit
78b1496b22
2 ha cambiato i file con 155 aggiunte e 4 eliminazioni
  1. 148 0
      rust/solve/examples/external-03-hole6.cnf
  2. 7 4
      rust/solve/src/main.rs

+ 148 - 0
rust/solve/examples/external-03-hole6.cnf

@ -0,0 +1,148 @@
1
c http://people.sc.fsu.edu/~jburkardt/data/cnf/hole6.cnf
2
3
c File:  hole6.cnf
4
c
5
c SOURCE: John Hooker (jh38+@andrew.cmu.edu)
6
c
7
c DESCRIPTION: Pigeon hole problem of placing n (for file holen) pigeons
8
c              in n+1 holes without placing 2 pigeons in the same hole
9
c
10
c NOTE: Part of the collection at the Forschungsinstitut fuer 
11
c       anwendungsorientierte Wissensverarbeitung in Ulm Germany.
12
c
13
c NOTE: Not satisfiable
14
c
15
p cnf 42 133
16
-1     -7    0
17
-1     -13   0
18
-1     -19   0
19
-1     -25   0
20
-1     -31   0
21
-1     -37   0
22
-7     -13   0
23
-7     -19   0
24
-7     -25   0
25
-7     -31   0
26
-7     -37   0
27
-13    -19   0
28
-13    -25   0
29
-13    -31   0
30
-13    -37   0
31
-19    -25   0
32
-19    -31   0
33
-19    -37   0
34
-25    -31   0
35
-25    -37   0
36
-31    -37   0
37
-2     -8    0
38
-2     -14   0
39
-2     -20   0
40
-2     -26   0
41
-2     -32   0
42
-2     -38   0
43
-8     -14   0
44
-8     -20   0
45
-8     -26   0
46
-8     -32   0
47
-8     -38   0
48
-14    -20   0
49
-14    -26   0
50
-14    -32   0
51
-14    -38   0
52
-20    -26   0
53
-20    -32   0
54
-20    -38   0
55
-26    -32   0
56
-26    -38   0
57
-32    -38   0
58
-3     -9    0
59
-3     -15   0
60
-3     -21   0
61
-3     -27   0
62
-3     -33   0
63
-3     -39   0
64
-9     -15   0
65
-9     -21   0
66
-9     -27   0
67
-9     -33   0
68
-9     -39   0
69
-15    -21   0
70
-15    -27   0
71
-15    -33   0
72
-15    -39   0
73
-21    -27   0
74
-21    -33   0
75
-21    -39   0
76
-27    -33   0
77
-27    -39   0
78
-33    -39   0
79
-4     -10   0
80
-4     -16   0
81
-4     -22   0
82
-4     -28   0
83
-4     -34   0
84
-4     -40   0
85
-10    -16   0
86
-10    -22   0
87
-10    -28   0
88
-10    -34   0
89
-10    -40   0
90
-16    -22   0
91
-16    -28   0
92
-16    -34   0
93
-16    -40   0
94
-22    -28   0
95
-22    -34   0
96
-22    -40   0
97
-28    -34   0
98
-28    -40   0
99
-34    -40   0
100
-5     -11   0
101
-5     -17   0
102
-5     -23   0
103
-5     -29   0
104
-5     -35   0
105
-5     -41   0
106
-11    -17   0
107
-11    -23   0
108
-11    -29   0
109
-11    -35   0
110
-11    -41   0
111
-17    -23   0
112
-17    -29   0
113
-17    -35   0
114
-17    -41   0
115
-23    -29   0
116
-23    -35   0
117
-23    -41   0
118
-29    -35   0
119
-29    -41   0
120
-35    -41   0
121
-6     -12   0
122
-6     -18   0
123
-6     -24   0
124
-6     -30   0
125
-6     -36   0
126
-6     -42   0
127
-12    -18   0
128
-12    -24   0
129
-12    -30   0
130
-12    -36   0
131
-12    -42   0
132
-18    -24   0
133
-18    -30   0
134
-18    -36   0
135
-18    -42   0
136
-24    -30   0
137
-24    -36   0
138
-24    -42   0
139
-30    -36   0
140
-30    -42   0
141
-36    -42   0
142
 6      5      4      3      2      1    0
143
 12     11     10     9      8      7    0
144
 18     17     16     15     14     13   0
145
 24     23     22     21     20     19   0
146
 30     29     28     27     26     25   0
147
 36     35     34     33     32     31   0
148
 42     41     40     39     38     37   0

+ 7 - 4
rust/solve/src/main.rs

@ -12,6 +12,7 @@ extern crate solve;
12 12
13 13
use std::io;
14 14
use std::io::Read;
15
use std::thread;
15 16
16 17
use solve::cnf;
17 18
use solve::dpll;
@ -26,10 +27,12 @@ fn main() {
26 27
		    println!("{:?}", clause);
27 28
		}
28 29
29
                match dpll::dpll(cnf.clauses) {
30
                    Some(bindings) => println!("satisfiable: {:?}", bindings),
31
                    None => println!("not satisfiable")
32
                }
30
                thread::Builder::new().name("solver".to_string()).stack_size(100 * 1024 * 1024).spawn(move || {
31
                    match dpll::dpll(cnf.clauses) {
32
                        Some(bindings) => println!("satisfiable: {:?}", bindings),
33
                        None => println!("not satisfiable")
34
                    }
35
                }).unwrap().join();
33 36
	    }
34 37
	    Err(e) => { println!("Error: {}", e) }
35 38
	},