1 #include "sat/sat_local_search.h"
2 #include "sat/sat_solver.h"
3 #include "util/cancel_eh.h"
4 #include "util/scoped_ctrl_c.h"
5 #include "util/scoped_timer.h"
6
build_instance(char const * filename,sat::solver & s,sat::local_search & local_search)7 static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
8 {
9 char line[16383];
10 // for temporary storage
11
12 std::ifstream infile(filename);
13 //if (infile == NULL) //linux
14 if (!infile) {
15 std::cout << "File not found " << filename << "\n";
16 return false;
17 }
18 infile.getline(line, 16383);
19 #ifdef _WINDOWS
20 int cur_term;
21 int num_vars = 0, num_constraints = 0;
22 sscanf_s(line, "%d %d", &num_vars, &num_constraints);
23 //std::cout << "number of variables: " << num_vars << '\n';
24 //std::cout << "number of constraints: " << num_constraints << '\n';
25
26
27 unsigned_vector coefficients;
28 sat::literal_vector lits;
29
30 // process objective function:
31 // read coefficients
32 infile >> cur_term;
33 while (cur_term != 0) {
34 coefficients.push_back(cur_term);
35 infile >> cur_term;
36 }
37
38 // read variables
39 infile >> cur_term;
40 while (cur_term != 0) {
41 lits.push_back(sat::literal(abs(cur_term), cur_term < 0));
42 infile >> cur_term;
43 }
44
45 if (lits.size() != coefficients.size()) {
46 std::cout << "Objective function format error. They have different lengths.\n";
47 return false;
48 }
49
50 // read the constraints, one at a time
51 int k;
52 for (int c = 0; c < num_constraints; ++c) {
53 lits.reset();
54 infile >> cur_term;
55 while (cur_term != 0) {
56 lits.push_back(sat::literal(abs(cur_term), cur_term > 0));
57 infile >> cur_term;
58 }
59 infile >> k;
60 //local_search.add_cardinality(lits.size(), lits.c_ptr(), static_cast<unsigned>(lits.size() - k));
61 local_search.add_cardinality(lits.size(), lits.data(), static_cast<unsigned>(k));
62 }
63
64 infile.close();
65 return true;
66 #else
67 return false;
68 #endif
69 }
70
tst_sat_local_search(char ** argv,int argc,int & i)71 void tst_sat_local_search(char ** argv, int argc, int& i) {
72 if (argc < i + 2) {
73 std::cout << "require dimacs file name\n";
74 return;
75 }
76 reslimit limit;
77 params_ref params;
78 sat::solver solver(params, limit);
79 sat::local_search local_search;
80
81 local_search.import(solver, true);
82 char const* file_name = argv[i + 1];
83 ++i;
84
85 int cutoff_time = 1;
86
87 int v;
88 while (i + 1 < argc) {
89 std::cout << argv[i + 1] << "\n";
90 // set other ad hoc parameters.
91 if (argv[i + 1][0] == '-' && i + 2 < argc) {
92 switch (argv[i + 1][1]) {
93 case 's': // seed
94 v = atoi(argv[i + 2]);
95 local_search.config().set_random_seed(v);
96 break;
97 case 't': // cutoff_time
98 v = atoi(argv[i + 2]);
99 cutoff_time = v;
100 break;
101 case 'b': // best_known_value
102 v = atoi(argv[i + 2]);
103 local_search.config().set_best_known_value(v);
104 break;
105 default:
106 ++i;
107 v = -1;
108 break;
109 }
110 }
111 ++i;
112 }
113
114 if (!build_instance(file_name, solver, local_search)) {
115 return;
116 }
117
118 //std::cout << "local instance built\n";
119
120
121 // set up cancellation/timeout environment.
122
123 cancel_eh<reslimit> eh(local_search.rlimit());
124 scoped_ctrl_c ctrlc(eh, false, true);
125 scoped_timer timer(cutoff_time*1000, &eh);
126 local_search.check(0, nullptr, nullptr);
127
128 }
129