SemOpt  $Revision:72+[d9d7a33b5c20+]$
prefSAT.cpp
Go to the documentation of this file.
1 
9 #include "semopt.h"
10 
11 string sep = " ";
12 string nl = "\n";
13 string endcl = sep + "0";
14 string endclnl = endcl + nl;
15 
35 int PiGreek(SATFormulae *sat, AF* af, int encoding)
36 {
37  OrClause noempty_clause = OrClause();
39  for (int i = 0; i < (int)af->numArgs(); i++)
40  {
41  noempty_clause.appendVariable(af->getArgumentByNumber(i)->InVar());
42 
43  SetArguments *pred = new SetArguments();
44  af->getPredecessors(af->getArgumentByNumber(i), pred);
45 
46  if (debug)
47  {
48  cout << "predecessors of " << af->getArgumentByNumber(i)->getName() << ": ";
49 
50  for (it = pred->begin(); it != pred->end(); it++)
51  cout << (*it)->getName() << " ";
52  cout << endl;
53  }
54 
55  if (pred->empty())
56  {
57  //c2
58  (*sat).appendOrClause(
59  OrClause(1, af->getArgumentByNumber(i)->InVar()));
60 
61  (*sat).appendOrClause(af->getArgumentByNumber(i)->NotOutVar());
62 
63  (*sat).appendOrClause(af->getArgumentByNumber(i)->NotUndecVar());
64  }
65  else
66  {
67  OrClause c1_last_clause = OrClause();
68  OrClause c2_last_clause = OrClause();
69  OrClause c3_or_undec_clause = OrClause();
70  OrClause c3_bigor_clause = OrClause();
71  //c1
72  if (encoding == 0 || encoding == 1 || encoding == 2 || encoding == 3
73  || encoding == 4 || encoding == 5)
74  {
75  (*sat).appendOrClause(
76  OrClause(3, af->getArgumentByNumber(i)->InVar(),
77  af->getArgumentByNumber(i)->OutVar(),
78  af->getArgumentByNumber(i)->UndecVar()));
79 
80  (*sat).appendOrClause(
82  af->getArgumentByNumber(i)->NotOutVar()));
83 
84  (*sat).appendOrClause(
86  af->getArgumentByNumber(i)->NotUndecVar()));
87 
88  (*sat).appendOrClause(
90  af->getArgumentByNumber(i)->NotUndecVar()));
91  }
92 
93  for (it = pred->begin(); it != pred->end(); it++)
94  {
95  //c3
96  if (encoding == 0 || encoding == 1 || encoding == 3
97  || encoding == 5)
98  {
99  (*sat).appendOrClause(
101  (*it)->OutVar()));
102  }
103 
104  if (encoding == 0 || encoding == 2 || encoding == 3
105  || encoding == 5 )
106  {
107  c1_last_clause.appendVariable((*it)->NotOutVar());
108  }
109 
110  //c4
111  if (encoding == 0 || encoding == 2 || encoding == 3
112  || encoding == 4 )
113  {
114  (*sat).appendOrClause(
115  OrClause(2,
116  (*it)->NotInVar(),
117  af->getArgumentByNumber(i)->OutVar()));
118  }
119 
120  if (encoding == 0 || encoding == 1 || encoding == 3
121  || encoding == 4 )
122  {
123  c2_last_clause.appendVariable((*it)->InVar());
124  }
125 
126  //c5
127  if (encoding == 0 || encoding == 1 || encoding == 4
128  || encoding == 5 )
129  {
130  (*sat).appendOrClause(
131  OrClause(2,
133  (*it)->NotInVar()));
134 
135  c3_or_undec_clause.appendVariable((*it)->UndecVar());
136  }
137 
138  if (encoding == 0 || encoding == 2 || encoding == 4
139  || encoding == 5 )
140  {
141  c3_bigor_clause.appendVariable((*it)->InVar());
142  }
143  }
144 
145  //c3-end
146  if (encoding == 0 || encoding == 2 || encoding == 3 || encoding == 5
147  )
148  {
149  c1_last_clause.appendVariable(af->getArgumentByNumber(i)->InVar());
150  (*sat).appendOrClause(c1_last_clause);
151  }
152 
153  //c4-end
154  if (encoding == 0 || encoding == 1 || encoding == 3 || encoding == 4
155  )
156  {
157  c2_last_clause.addHeadVariable(
158  af->getArgumentByNumber(i)->NotOutVar());
159  (*sat).appendOrClause(c2_last_clause);
160  }
161 
162  //c5-end
163  if (encoding == 0 || encoding == 1 || encoding == 4 || encoding == 5
164  )
165  {
166  c3_or_undec_clause.addHeadVariable(
167  af->getArgumentByNumber(i)->NotUndecVar());
168  (*sat).appendOrClause(c3_or_undec_clause);
169  }
170 
171  if (encoding == 0 || encoding == 2 || encoding == 4 || encoding == 5
172  )
173  {
174  for (it = pred->begin(); it != pred->end(); it++)
175  {
176  OrClause to_add = OrClause();
177  c3_bigor_clause.clone(&to_add);
178  to_add.appendVariable((*it)->NotUndecVar());
179  to_add.appendVariable(af->getArgumentByNumber(i)->UndecVar());
180  (*sat).appendOrClause(to_add);
181  }
182  }
183 
184  }
185  }
186  (*sat).appendOrClause(noempty_clause);
187 
188  return (*sat).size();
189 }
190 
204 void aSolution(vector<int> *res, dArray *vals, AF *af)
205 {
206  for (int i = 0; i < (int) (*vals).size(); i++)
207  {
208  if (count(res->begin(), res->end(), af->getArgumentByNumber(i)->InVar())
209  == 1)
210  (*vals)[i] = 1;
211  else
212  (*vals)[i] = 0;
213  }
214 }
215 
230 void INARGS(vector<int> *assign, vector<Argument *> *toarg, vector<Argument *> *closeworld, AF *af)
231 {
232  for (int i = 0; i < af->numArgs(); i++)
233  {
234  if (assign->at(i) > 0)
235  {
236  toarg->push_back(af->getArgumentByNumber(i));
237  }
238  else
239  {
240  closeworld->push_back(af->getArgumentByNumber(i));
241  }
242  }
243 }
244 
288 int PrefSat(dMatrix *preferred_extensions, AF *af, int encoding, int (*SatSolver)(stringstream *, int, int, vector<int> *))
289 {
290 
291  vector<vector<int> > intres_temp = vector<vector<int> >();
292 
293 
294  SATFormulae cnf = SATFormulae();
295  int numcl = PiGreek(&cnf, af, encoding);
296 
297  if (debug)
298  {
299  cout << cnf;
300  ofstream f("/tmp/debugcnf");
301  f << "p cnf " << 3 * af->numArgs() << " " << numcl << "\n"
302  << cnf;
303  f.flush();
304  f.close();
305  }
306 
307 
308  if (SatSolver == NULL)
309  {
310  ofstream f(inputfile.append(".CNF").c_str());
311  f << "p cnf " << 3 * af->numArgs() << " " << numcl << "\n"
312  << cnf;
313  f.flush();
314  f.close();
315  return 1;
316  }
317 
318  do
319  {
320  vector<int> prefcand = vector<int>();
321 
322  SATFormulae cnfdf = SATFormulae();
323  cnf.clone(&cnfdf);
324 
325  if (debug)
326  {
327  cout << "Cloned\n";
328  cout << cnfdf;
329  }
330 
331  while (true)
332  {
333  stringstream cnf_string(stringstream::in | stringstream::out);
334  cnfdf.toSS(&cnf_string);
335 
336  if (debug)
337  {
338  cout << "Preparing the satsolver" << "\n";
339  cout << cnf_string.str();
340  }
341 
342  vector<int> lastcompfound = vector<int>();
343  int retsat = (*SatSolver)(&cnf_string, 3 * af->numArgs(), cnfdf.size(), &lastcompfound);
344 
345  if (debug)
346  cout << retsat;
347 
348  if (retsat == 20)
349  {
350  break;
351  }
352 
353  prefcand = vector<int>();
354  for (int i = 0; i < af->numArgs(); i++)
355  prefcand.push_back(lastcompfound.at(i));
356 
357  vector<Argument *> in_args = vector<Argument *>();
358  vector<Argument *> in_args_closure = vector<Argument *>();
359  INARGS(&lastcompfound, &in_args, &in_args_closure, af);
360 
361  if (debug)
362  {
363  cout << "{";
364  for (int i = 0; i < (int)in_args.size(); i++)
365  {
366  cout << in_args.at(i)->getName() << " ";
367  }
368  cout << "}\n";
369  }
370 
371  if ((int)in_args.size() == af->numArgs())
372  break;
373 
374  OrClause remove_complete_from_cnf = OrClause();
375  for (int i = 0; i < (int)in_args.size(); i++)
376  {
377  cnfdf.appendOrClause(OrClause(1,in_args.at(i)->InVar()));
378  remove_complete_from_cnf.appendVariable(in_args.at(i)->NotInVar());
379  }
380  cnf.appendOrClause(remove_complete_from_cnf);
381 
382  OrClause remaining = OrClause();
383  for (int i = 0; i < (int)in_args_closure.size(); i++)
384  {
385  remaining.appendVariable(in_args_closure.at(i)->InVar());
386  }
387  cnfdf.appendOrClause(remaining);
388  }
389 
390  if (prefcand.empty())
391  break;
392 
393  dArray vals = dArray(af->numArgs());
394  aSolution(&prefcand, &vals, af);
395  (*preferred_extensions).push_back(vals);
396 
397  vector<Argument *> in_pref = vector<Argument *>();
398  vector<Argument *> in_pref_closure = vector<Argument *>();
399  INARGS(&prefcand, &in_pref, &in_pref_closure, af);
400 
401  OrClause oppsolution = OrClause();
402  for (int i = 0; i < (int)in_pref_closure.size(); i++)
403  {
404  oppsolution.appendVariable(in_pref_closure.at(i)->InVar());
405  }
406  cnf.appendOrClause(oppsolution);
407 
408  } while (true);
409 
410  if ((*preferred_extensions).empty())
411  {
412  dArray emptyset = dArray(af->numArgs());
413  for (int i = 0; i < (int) emptyset.size(); i++)
414  emptyset[i] = 0;
415  (*preferred_extensions).push_back(emptyset);
416  }
417 
418  return 0;
419 }