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