Scippy

SCIP

Solving Constraint Integer Programs

reader_cnf.c
Go to the documentation of this file.
1 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
2 /* */
3 /* This file is part of the program and library */
4 /* SCIP --- Solving Constraint Integer Programs */
5 /* */
6 /* Copyright (C) 2002-2014 Konrad-Zuse-Zentrum */
7 /* fuer Informationstechnik Berlin */
8 /* */
9 /* SCIP is distributed under the terms of the ZIB Academic License. */
10 /* */
11 /* You should have received a copy of the ZIB Academic License */
12 /* along with SCIP; see the file COPYING. If not email to scip@zib.de. */
13 /* */
14 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
15 
16 /**@file reader_cnf.c
17  * @brief CNF file reader
18  * @author Thorsten Koch
19  * @author Tobias Achterberg
20  *
21  * The DIMACS CNF (conjunctive normal form) is a file format used for example for SAT problems. For a detailed description of
22  * this format see http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html .
23  */
24 
25 /*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
26 
27 #include <assert.h>
28 #include <string.h>
29 
30 #include "scip/reader_cnf.h"
31 #include "scip/cons_linear.h"
32 #include "scip/cons_logicor.h"
33 #include "scip/cons_setppc.h"
34 #include "scip/pub_misc.h"
35 
36 
37 #define READER_NAME "cnfreader"
38 #define READER_DESC "file reader for SAT problems in conjunctive normal form"
39 #define READER_EXTENSION "cnf"
40 
41 #define MAXLINELEN 65536
42 
43 
44 /*
45  * cnf reader internal methods
46  */
47 
48 static
49 void readError(
50  SCIP* scip, /**< SCIP data structure */
51  int linecount, /**< line number of error */
52  const char* errormsg /**< error message */
53  )
54 {
55  SCIPerrorMessage("read error in line <%d>: %s\n", linecount, errormsg);
56 }
57 
58 static
59 void readWarning(
60  SCIP* scip, /**< SCIP data structure */
61  int linecount, /**< line number of error */
62  const char* warningmsg /**< warning message */
63  )
64 {
65  SCIPwarningMessage(scip, "Line <%d>: %s\n", linecount, warningmsg);
66 }
67 
68 /** reads the next non-empty non-comment line of a cnf file */
69 static
70 SCIP_RETCODE readCnfLine(
71  SCIP* scip, /**< SCIP data structure */
72  SCIP_FILE* file, /**< input file */
73  char* buffer, /**< buffer for storing the input line */
74  int size, /**< size of the buffer */
75  int* linecount /**< pointer to the line number counter */
76  )
77 {
78  char* line;
79  int linelen;
80 
81  assert(file != NULL);
82  assert(buffer != NULL);
83  assert(size >= 2);
84  assert(linecount != NULL);
85 
86  do
87  {
88  (*linecount)++;
89  line = SCIPfgets(buffer, size, file);
90  if( line != NULL )
91  {
92  linelen = (int)strlen(line);
93  if( linelen == size-1 )
94  {
95  char s[SCIP_MAXSTRLEN];
96  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "line too long (exceeds %d characters)", size-2);
97  readError(scip, *linecount, s);
98  return SCIP_READERROR;
99  }
100  }
101  else
102  linelen = 0;
103  }
104  while( line != NULL && (*line == 'c' || *line == '\n') );
105 
106  if( line != NULL && linelen >= 2 && line[linelen-2] == '\n' )
107  line[linelen-2] = '\0';
108  else if( linelen == 0 )
109  *buffer = '\0';
110 
111  assert((line == NULL) == (*buffer == '\0'));
112 
113  return SCIP_OKAY;
114 }
115 
116 /* Read SAT formula in "CNF File Format".
117  *
118  * The specification is taken from the
119  *
120  * Satisfiability Suggested Format
121  *
122  * Online available at http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/Benchmarks/SAT/satformat.ps
123  *
124  * The method reads all files of CNF format. Other formats (SAT, SATX, SATE) are not supported.
125  */
126 static
127 SCIP_RETCODE readCnf(
128  SCIP* scip, /**< SCIP data structure */
129  SCIP_FILE* file /**< input file */
130  )
131 {
132  SCIP_RETCODE retcode;
133  SCIP_VAR** vars;
134  SCIP_VAR** clausevars;
135  SCIP_CONS* cons;
136  int* varsign;
137  char* tok;
138  char* nexttok;
139  char line[MAXLINELEN];
140  char format[SCIP_MAXSTRLEN];
141  char varname[SCIP_MAXSTRLEN];
142  char s[SCIP_MAXSTRLEN];
143  SCIP_Bool initialconss;
144  SCIP_Bool dynamicconss;
145  SCIP_Bool dynamiccols;
146  SCIP_Bool dynamicrows;
147  SCIP_Bool useobj;
148  int linecount;
149  int clauselen;
150  int clausenum;
151  int nvars;
152  int nclauses;
153  int varnum;
154  int v;
155 
156  assert(scip != NULL);
157  assert(file != NULL);
158 
159  retcode = SCIP_OKAY;
160 
161  linecount = 0;
162 
163  /* read header */
164  SCIP_CALL( readCnfLine(scip, file, line, (int) sizeof(line), &linecount) );
165  if( *line != 'p' )
166  {
167  readError(scip, linecount, "problem declaration line expected");
168  return SCIP_READERROR;
169  }
170  if( sscanf(line, "p %8s %d %d", format, &nvars, &nclauses) != 3 )
171  {
172  readError(scip, linecount, "invalid problem declaration (must be 'p cnf <nvars> <nclauses>')");
173  return SCIP_READERROR;
174  }
175  if( strcmp(format, "cnf") != 0 )
176  {
177  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid format tag <%s> (must be 'cnf')", format);
178  readError(scip, linecount, s);
179  return SCIP_READERROR;
180  }
181  if( nvars <= 0 )
182  {
183  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid number of variables <%d> (must be positive)", nvars);
184  readError(scip, linecount, s);
185  return SCIP_READERROR;
186  }
187  if( nclauses <= 0 )
188  {
189  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid number of clauses <%d> (must be positive)", nclauses);
190  readError(scip, linecount, s);
191  return SCIP_READERROR;
192  }
193 
194  /* get parameter values */
195  SCIP_CALL( SCIPgetBoolParam(scip, "reading/initialconss", &initialconss) );
196  SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamicconss", &dynamicconss) );
197  SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamiccols", &dynamiccols) );
198  SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamicrows", &dynamicrows) );
199  SCIP_CALL( SCIPgetBoolParam(scip, "reading/cnfreader/useobj", &useobj) );
200 
201  /* get temporary memory */
202  SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
203  SCIP_CALL( SCIPallocBufferArray(scip, &clausevars, nvars) );
204  SCIP_CALL( SCIPallocBufferArray(scip, &varsign, nvars) );
205 
206  /* create the variables */
207  for( v = 0; v < nvars; ++v )
208  {
209  (void) SCIPsnprintf(varname, SCIP_MAXSTRLEN, "x%d", v+1);
210  SCIP_CALL( SCIPcreateVar(scip, &vars[v], varname, 0.0, 1.0, 0.0, SCIP_VARTYPE_BINARY, !dynamiccols, dynamiccols,
211  NULL, NULL, NULL, NULL, NULL) );
212  SCIP_CALL( SCIPaddVar(scip, vars[v]) );
213  varsign[v] = 0;
214  }
215 
216  /* read clauses */
217  clausenum = 0;
218  clauselen = 0;
219  do
220  {
221  retcode = readCnfLine(scip, file, line, (int) sizeof(line), &linecount);
222  if( retcode != SCIP_OKAY )
223  goto TERMINATE;
224 
225  if( *line != '\0' && *line != '%' )
226  {
227  tok = SCIPstrtok(line, " \f\n\r\t", &nexttok);
228  while( tok != NULL )
229  {
230  /* parse literal and check for errors */
231  if( sscanf(tok, "%d", &v) != 1 )
232  {
233  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid literal <%s>", tok);
234  readError(scip, linecount, s);
235  retcode = SCIP_READERROR;
236  goto TERMINATE;
237  }
238 
239  /* interpret literal number: v == 0: end of clause, v < 0: negated literal, v > 0: positive literal */
240  if( v == 0 )
241  {
242  /* end of clause: construct clause and add it to SCIP */
243  if( clauselen == 0 )
244  readWarning(scip, linecount, "empty clause detected in line -- problem infeasible");
245 
246  clausenum++;
247  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "c%d", clausenum);
248 
249  if( SCIPfindConshdlr(scip, "logicor") != NULL )
250  {
251  /* if the constraint handler logicor exit create a logicor constraint */
252  SCIP_CALL( SCIPcreateConsLogicor(scip, &cons, s, clauselen, clausevars,
253  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
254  }
255  else if( SCIPfindConshdlr(scip, "setppc") != NULL )
256  {
257  /* if the constraint handler logicor does not exit but constraint
258  * handler setppc create a setppc constraint */
259  SCIP_CALL( SCIPcreateConsSetcover(scip, &cons, s, clauselen, clausevars,
260  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
261  }
262  else
263  {
264  /* if none of the previous constraint handler exits create a linear
265  * constraint */
266  SCIP_Real* vals;
267  int i;
268 
269  SCIP_CALL( SCIPallocBufferArray(scip, &vals, clauselen) );
270 
271  for( i = 0; i < clauselen; ++i )
272  vals[i] = 1.0;
273 
274  SCIP_CALL( SCIPcreateConsLinear(scip, &cons, s, clauselen, clausevars, vals, 1.0, SCIPinfinity(scip),
275  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
276 
277  SCIPfreeBufferArray(scip, &vals);
278  }
279 
280  SCIP_CALL( SCIPaddCons(scip, cons) );
281  SCIP_CALL( SCIPreleaseCons(scip, &cons) );
282  clauselen = 0;
283  }
284  else if( v >= -nvars && v <= nvars )
285  {
286  if( clauselen >= nvars )
287  {
288  readError(scip, linecount, "too many literals in clause");
289  retcode = SCIP_READERROR;
290  goto TERMINATE;
291  }
292 
293  /* add literal to clause */
294  varnum = ABS(v)-1;
295  if( v < 0 )
296  {
297  SCIP_CALL( SCIPgetNegatedVar(scip, vars[varnum], &clausevars[clauselen]) );
298  varsign[varnum]--;
299  }
300  else
301  {
302  clausevars[clauselen] = vars[varnum];
303  varsign[varnum]++;
304  }
305  clauselen++;
306  }
307  else
308  {
309  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid variable number <%d>", ABS(v));
310  readError(scip, linecount, s);
311  retcode = SCIP_READERROR;
312  goto TERMINATE;
313  }
314 
315  /* get next token */
316  tok = SCIPstrtok(NULL, " \f\n\r\t", &nexttok);
317  }
318  }
319  }
320  while( *line != '\0' && *line != '%' );
321 
322  /* check for additional literals */
323  if( clauselen > 0 )
324  {
325  SCIPwarningMessage(scip, "found %d additional literals after last clause\n", clauselen);
326  }
327 
328  /* check number of clauses */
329  if( clausenum != nclauses )
330  {
331  SCIPwarningMessage(scip, "expected %d clauses, but found %d\n", nclauses, clausenum);
332  }
333 
334  TERMINATE:
335  /* change objective values and release variables */
336  SCIP_CALL( SCIPsetObjsense(scip, SCIP_OBJSENSE_MAXIMIZE) );
337  for( v = 0; v < nvars; ++v )
338  {
339  if( useobj )
340  {
341  SCIP_CALL( SCIPchgVarObj(scip, vars[v], (SCIP_Real)varsign[v]) );
342  }
343  SCIP_CALL( SCIPreleaseVar(scip, &vars[v]) );
344  }
345 
346  /* free temporary memory */
347  SCIPfreeBufferArray(scip, &varsign);
348  SCIPfreeBufferArray(scip, &clausevars);
349  SCIPfreeBufferArray(scip, &vars);
350 
351  return retcode;
352 }
353 
354 
355 /*
356  * Callback methods
357  */
358 
359 /** copy method for reader plugins (called when SCIP copies plugins) */
360 static
361 SCIP_DECL_READERCOPY(readerCopyCnf)
362 { /*lint --e{715}*/
363  assert(scip != NULL);
364  assert(reader != NULL);
365  assert(strcmp(SCIPreaderGetName(reader), READER_NAME) == 0);
366 
367  /* call inclusion method of reader */
368  SCIP_CALL( SCIPincludeReaderCnf(scip) );
369 
370  return SCIP_OKAY;
371 }
372 
373 
374 /** problem reading method of reader */
375 static
376 SCIP_DECL_READERREAD(readerReadCnf)
377 { /*lint --e{715}*/
378  SCIP_FILE* f;
379  SCIP_RETCODE retcode;
380 
381  assert(reader != NULL);
382  assert(strcmp(SCIPreaderGetName(reader), READER_NAME) == 0);
383  assert(filename != NULL);
384  assert(result != NULL);
385 
386  /* open file */
387  f = SCIPfopen(filename, "r");
388  if( f == NULL )
389  {
390  SCIPerrorMessage("cannot open file <%s> for reading\n", filename);
391  SCIPprintSysError(filename);
392  return SCIP_NOFILE;
393  }
394 
395  /* create problem */
396  SCIP_CALL( SCIPcreateProb(scip, filename, NULL, NULL, NULL, NULL, NULL, NULL, NULL) );
397 
398  /* read cnf file */
399  retcode = readCnf(scip, f);
400 
401  /* close file */
402  SCIPfclose(f);
403 
404  *result = SCIP_SUCCESS;
405 
406  return retcode;
407 }
408 
409 
410 /*
411  * cnf file reader specific interface methods
412  */
413 
414 /** includes the cnf file reader in SCIP */
415 SCIP_RETCODE SCIPincludeReaderCnf(
416  SCIP* scip /**< SCIP data structure */
417  )
418 {
419  SCIP_READERDATA* readerdata;
420  SCIP_READER* reader;
421 
422  /* create reader data */
423  readerdata = NULL;
424 
425  /* include reader */
426  SCIP_CALL( SCIPincludeReaderBasic(scip, &reader, READER_NAME, READER_DESC, READER_EXTENSION, readerdata) );
427 
428  /* set non fundamental callbacks via setter functions */
429  SCIP_CALL( SCIPsetReaderCopy(scip, reader, readerCopyCnf) );
430  SCIP_CALL( SCIPsetReaderRead(scip, reader, readerReadCnf) );
431 
432  /* add cnf reader parameters */
433  SCIP_CALL( SCIPaddBoolParam(scip,
434  "reading/cnfreader/useobj", "should an artificial objective, depending on the number of clauses a variable appears in, be used?",
435  NULL, FALSE, FALSE, NULL, NULL) );
436 
437  return SCIP_OKAY;
438 }
439 
440