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-2018 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 visit 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 "blockmemshell/memory.h"
28 #include "scip/cons_linear.h"
29 #include "scip/cons_logicor.h"
30 #include "scip/cons_setppc.h"
31 #include "scip/pub_fileio.h"
32 #include "scip/pub_message.h"
33 #include "scip/pub_misc.h"
34 #include "scip/pub_reader.h"
35 #include "scip/reader_cnf.h"
36 #include "scip/scip_cons.h"
37 #include "scip/scip_mem.h"
38 #include "scip/scip_message.h"
39 #include "scip/scip_numerics.h"
40 #include "scip/scip_param.h"
41 #include "scip/scip_prob.h"
42 #include "scip/scip_reader.h"
43 #include "scip/scip_var.h"
44 #include <string.h>
45 
46 #define READER_NAME "cnfreader"
47 #define READER_DESC "file reader for SAT problems in conjunctive normal form"
48 #define READER_EXTENSION "cnf"
49 
50 #define MAXLINELEN 65536
51 
52 
53 /*
54  * cnf reader internal methods
55  */
56 
57 static
58 void readError(
59  SCIP* scip, /**< SCIP data structure */
60  int linecount, /**< line number of error */
61  const char* errormsg /**< error message */
62  )
63 {
64  SCIPerrorMessage("read error in line <%d>: %s\n", linecount, errormsg);
65 }
66 
67 static
69  SCIP* scip, /**< SCIP data structure */
70  int linecount, /**< line number of error */
71  const char* warningmsg /**< warning message */
72  )
73 {
74  SCIPwarningMessage(scip, "Line <%d>: %s\n", linecount, warningmsg);
75 }
76 
77 /** reads the next non-empty non-comment line of a cnf file */
78 static
80  SCIP* scip, /**< SCIP data structure */
81  SCIP_FILE* file, /**< input file */
82  char* buffer, /**< buffer for storing the input line */
83  int size, /**< size of the buffer */
84  int* linecount /**< pointer to the line number counter */
85  )
86 {
87  char* line;
88  int linelen;
89 
90  assert(file != NULL);
91  assert(buffer != NULL);
92  assert(size >= 2);
93  assert(linecount != NULL);
94 
95  do
96  {
97  (*linecount)++;
98  line = SCIPfgets(buffer, size, file);
99  if( line != NULL )
100  {
101  linelen = (int)strlen(line);
102  if( linelen == size-1 )
103  {
104  char s[SCIP_MAXSTRLEN];
105  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "line too long (exceeds %d characters)", size-2);
106  readError(scip, *linecount, s);
107  return SCIP_READERROR;
108  }
109  }
110  else
111  linelen = 0;
112  }
113  while( line != NULL && (*line == 'c' || *line == '\n') );
114 
115  if( line != NULL && linelen >= 2 && line[linelen-2] == '\n' )
116  line[linelen-2] = '\0';
117  else if( linelen == 0 )
118  *buffer = '\0';
119 
120  assert((line == NULL) == (*buffer == '\0'));
121 
122  return SCIP_OKAY;
123 }
124 
125 /* Read SAT formula in "CNF File Format".
126  *
127  * The specification is taken from the
128  *
129  * Satisfiability Suggested Format
130  *
131  * Online available at http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/Benchmarks/SAT/satformat.ps
132  *
133  * The method reads all files of CNF format. Other formats (SAT, SATX, SATE) are not supported.
134  */
135 static
137  SCIP* scip, /**< SCIP data structure */
138  SCIP_FILE* file /**< input file */
139  )
140 {
141  SCIP_RETCODE retcode;
142  SCIP_VAR** vars;
143  SCIP_VAR** clausevars;
144  SCIP_CONS* cons;
145  int* varsign;
146  char* tok;
147  char* nexttok;
148  char line[MAXLINELEN];
149  char format[SCIP_MAXSTRLEN];
150  char varname[SCIP_MAXSTRLEN];
151  char s[SCIP_MAXSTRLEN];
152  SCIP_Bool initialconss;
153  SCIP_Bool dynamicconss;
154  SCIP_Bool dynamiccols;
155  SCIP_Bool dynamicrows;
156  SCIP_Bool useobj;
157  int linecount;
158  int clauselen;
159  int clausenum;
160  int nvars;
161  int nclauses;
162  int varnum;
163  int v;
164 
165  assert(scip != NULL);
166  assert(file != NULL);
167 
168  linecount = 0;
169 
170  /* read header */
171  SCIP_CALL( readCnfLine(scip, file, line, (int) sizeof(line), &linecount) );
172  if( *line != 'p' )
173  {
174  readError(scip, linecount, "problem declaration line expected");
175  return SCIP_READERROR;
176  }
177  /* cppcheck-suppress invalidScanfFormatWidth_smaller */
178  if( sscanf(line, "p %8s %d %d", format, &nvars, &nclauses) != 3 )
179  {
180  readError(scip, linecount, "invalid problem declaration (must be 'p cnf <nvars> <nclauses>')");
181  return SCIP_READERROR;
182  }
183  if( strcmp(format, "cnf") != 0 )
184  {
185  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid format tag <%s> (must be 'cnf')", format);
186  readError(scip, linecount, s);
187  return SCIP_READERROR;
188  }
189  if( nvars <= 0 )
190  {
191  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid number of variables <%d> (must be positive)", nvars);
192  readError(scip, linecount, s);
193  return SCIP_READERROR;
194  }
195  if( nclauses <= 0 )
196  {
197  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid number of clauses <%d> (must be positive)", nclauses);
198  readError(scip, linecount, s);
199  return SCIP_READERROR;
200  }
201 
202  /* get parameter values */
203  SCIP_CALL( SCIPgetBoolParam(scip, "reading/initialconss", &initialconss) );
204  SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamicconss", &dynamicconss) );
205  SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamiccols", &dynamiccols) );
206  SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamicrows", &dynamicrows) );
207  SCIP_CALL( SCIPgetBoolParam(scip, "reading/cnfreader/useobj", &useobj) );
208 
209  /* get temporary memory */
210  SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
211  SCIP_CALL( SCIPallocBufferArray(scip, &clausevars, nvars) );
212  SCIP_CALL( SCIPallocBufferArray(scip, &varsign, nvars) );
213 
214  /* create the variables */
215  for( v = 0; v < nvars; ++v )
216  {
217  (void) SCIPsnprintf(varname, SCIP_MAXSTRLEN, "x%d", v+1);
218  SCIP_CALL( SCIPcreateVar(scip, &vars[v], varname, 0.0, 1.0, 0.0, SCIP_VARTYPE_BINARY, !dynamiccols, dynamiccols,
219  NULL, NULL, NULL, NULL, NULL) );
220  SCIP_CALL( SCIPaddVar(scip, vars[v]) );
221  varsign[v] = 0;
222  }
223 
224  /* read clauses */
225  clausenum = 0;
226  clauselen = 0;
227  do
228  {
229  retcode = readCnfLine(scip, file, line, (int) sizeof(line), &linecount);
230  if( retcode != SCIP_OKAY )
231  goto TERMINATE;
232 
233  if( *line != '\0' && *line != '%' )
234  {
235  tok = SCIPstrtok(line, " \f\n\r\t", &nexttok);
236  while( tok != NULL )
237  {
238  /* parse literal and check for errors */
239  if( sscanf(tok, "%d", &v) != 1 )
240  {
241  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid literal <%s>", tok);
242  readError(scip, linecount, s);
243  retcode = SCIP_READERROR;
244  goto TERMINATE;
245  }
246 
247  /* interpret literal number: v == 0: end of clause, v < 0: negated literal, v > 0: positive literal */
248  if( v == 0 )
249  {
250  /* end of clause: construct clause and add it to SCIP */
251  if( clauselen == 0 )
252  readWarning(scip, linecount, "empty clause detected in line -- problem infeasible");
253 
254  clausenum++;
255  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "c%d", clausenum);
256 
257  if( SCIPfindConshdlr(scip, "logicor") != NULL )
258  {
259  /* if the constraint handler logicor exit create a logicor constraint */
260  SCIP_CALL( SCIPcreateConsLogicor(scip, &cons, s, clauselen, clausevars,
261  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
262  }
263  else if( SCIPfindConshdlr(scip, "setppc") != NULL )
264  {
265  /* if the constraint handler logicor does not exit but constraint
266  * handler setppc create a setppc constraint */
267  SCIP_CALL( SCIPcreateConsSetcover(scip, &cons, s, clauselen, clausevars,
268  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
269  }
270  else
271  {
272  /* if none of the previous constraint handler exits create a linear
273  * constraint */
274  SCIP_Real* vals;
275  int i;
276 
277  SCIP_CALL( SCIPallocBufferArray(scip, &vals, clauselen) );
278 
279  for( i = 0; i < clauselen; ++i )
280  vals[i] = 1.0;
281 
282  SCIP_CALL( SCIPcreateConsLinear(scip, &cons, s, clauselen, clausevars, vals, 1.0, SCIPinfinity(scip),
283  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
284 
285  SCIPfreeBufferArray(scip, &vals);
286  }
287 
288  SCIP_CALL( SCIPaddCons(scip, cons) );
289  SCIP_CALL( SCIPreleaseCons(scip, &cons) );
290  clauselen = 0;
291  }
292  else if( v >= -nvars && v <= nvars )
293  {
294  if( clauselen >= nvars )
295  {
296  readError(scip, linecount, "too many literals in clause");
297  retcode = SCIP_READERROR;
298  goto TERMINATE;
299  }
300 
301  /* add literal to clause */
302  varnum = ABS(v)-1;
303  if( v < 0 )
304  {
305  SCIP_CALL( SCIPgetNegatedVar(scip, vars[varnum], &clausevars[clauselen]) );
306  varsign[varnum]--;
307  }
308  else
309  {
310  clausevars[clauselen] = vars[varnum];
311  varsign[varnum]++;
312  }
313  clauselen++;
314  }
315  else
316  {
317  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid variable number <%d>", ABS(v));
318  readError(scip, linecount, s);
319  retcode = SCIP_READERROR;
320  goto TERMINATE;
321  }
322 
323  /* get next token */
324  tok = SCIPstrtok(NULL, " \f\n\r\t", &nexttok);
325  }
326  }
327  }
328  while( *line != '\0' && *line != '%' );
329 
330  /* check for additional literals */
331  if( clauselen > 0 )
332  {
333  SCIPwarningMessage(scip, "found %d additional literals after last clause\n", clauselen);
334  }
335 
336  /* check number of clauses */
337  if( clausenum != nclauses )
338  {
339  SCIPwarningMessage(scip, "expected %d clauses, but found %d\n", nclauses, clausenum);
340  }
341 
342  TERMINATE:
343  /* change objective values and release variables */
345  for( v = 0; v < nvars; ++v )
346  {
347  if( useobj )
348  {
349  SCIP_CALL( SCIPchgVarObj(scip, vars[v], (SCIP_Real)varsign[v]) );
350  }
351  SCIP_CALL( SCIPreleaseVar(scip, &vars[v]) );
352  }
353 
354  /* free temporary memory */
355  SCIPfreeBufferArray(scip, &varsign);
356  SCIPfreeBufferArray(scip, &clausevars);
357  SCIPfreeBufferArray(scip, &vars);
358 
359  return retcode;
360 }
361 
362 
363 /*
364  * Callback methods
365  */
366 
367 /** copy method for reader plugins (called when SCIP copies plugins) */
368 static
369 SCIP_DECL_READERCOPY(readerCopyCnf)
370 { /*lint --e{715}*/
371  assert(scip != NULL);
372  assert(reader != NULL);
373  assert(strcmp(SCIPreaderGetName(reader), READER_NAME) == 0);
374 
375  /* call inclusion method of reader */
377 
378  return SCIP_OKAY;
379 }
380 
381 
382 /** problem reading method of reader */
383 static
384 SCIP_DECL_READERREAD(readerReadCnf)
385 { /*lint --e{715}*/
386  SCIP_FILE* f;
387  SCIP_RETCODE retcode;
388 
389  assert(reader != NULL);
390  assert(strcmp(SCIPreaderGetName(reader), READER_NAME) == 0);
391  assert(filename != NULL);
392  assert(result != NULL);
393 
394  /* open file */
395  f = SCIPfopen(filename, "r");
396  if( f == NULL )
397  {
398  SCIPerrorMessage("cannot open file <%s> for reading\n", filename);
399  SCIPprintSysError(filename);
400  return SCIP_NOFILE;
401  }
402 
403  /* create problem */
404  SCIP_CALL( SCIPcreateProb(scip, filename, NULL, NULL, NULL, NULL, NULL, NULL, NULL) );
405 
406  /* read cnf file */
407  retcode = readCnf(scip, f);
408 
409  /* close file */
410  SCIPfclose(f);
411 
412  *result = SCIP_SUCCESS;
413 
414  return retcode;
415 }
416 
417 
418 /*
419  * cnf file reader specific interface methods
420  */
421 
422 /** includes the cnf file reader in SCIP */
424  SCIP* scip /**< SCIP data structure */
425  )
426 {
427  SCIP_READER* reader;
428 
429  /* include reader */
431 
432  /* set non fundamental callbacks via setter functions */
433  SCIP_CALL( SCIPsetReaderCopy(scip, reader, readerCopyCnf) );
434  SCIP_CALL( SCIPsetReaderRead(scip, reader, readerReadCnf) );
435 
436  /* add cnf reader parameters */
438  "reading/cnfreader/useobj", "should an artificial objective, depending on the number of clauses a variable appears in, be used?",
439  NULL, FALSE, FALSE, NULL, NULL) );
440 
441  return SCIP_OKAY;
442 }
443 
#define NULL
Definition: def.h:239
static void readWarning(SCIP *scip, int linecount, const char *warningmsg)
Definition: reader_cnf.c:68
public methods for SCIP parameter handling
public methods for memory management
SCIP_CONSHDLR * SCIPfindConshdlr(SCIP *scip, const char *name)
Definition: scip_cons.c:954
CNF file reader.
static SCIP_DECL_READERCOPY(readerCopyCnf)
Definition: reader_cnf.c:369
#define SCIP_MAXSTRLEN
Definition: def.h:260
SCIP_RETCODE SCIPcreateProb(SCIP *scip, const char *name, SCIP_DECL_PROBDELORIG((*probdelorig)), SCIP_DECL_PROBTRANS((*probtrans)), SCIP_DECL_PROBDELTRANS((*probdeltrans)), SCIP_DECL_PROBINITSOL((*probinitsol)), SCIP_DECL_PROBEXITSOL((*probexitsol)), SCIP_DECL_PROBCOPY((*probcopy)), SCIP_PROBDATA *probdata)
Definition: scip_prob.c:162
static SCIP_RETCODE readCnfLine(SCIP *scip, SCIP_FILE *file, char *buffer, int size, int *linecount)
Definition: reader_cnf.c:79
SCIP_RETCODE SCIPcreateConsSetcover(SCIP *scip, SCIP_CONS **cons, const char *name, int nvars, SCIP_VAR **vars, SCIP_Bool initial, SCIP_Bool separate, SCIP_Bool enforce, SCIP_Bool check, SCIP_Bool propagate, SCIP_Bool local, SCIP_Bool modifiable, SCIP_Bool dynamic, SCIP_Bool removable, SCIP_Bool stickingatnode)
Definition: cons_setppc.c:9172
const char * SCIPreaderGetName(SCIP_READER *reader)
Definition: reader.c:547
SCIP_RETCODE SCIPreleaseVar(SCIP *scip, SCIP_VAR **var)
Definition: scip_var.c:1251
#define FALSE
Definition: def.h:65
SCIP_Real SCIPinfinity(SCIP *scip)
int SCIPsnprintf(char *t, int len, const char *s,...)
Definition: misc.c:10017
#define TRUE
Definition: def.h:64
enum SCIP_Retcode SCIP_RETCODE
Definition: type_retcode.h:53
static SCIP_RETCODE readCnf(SCIP *scip, SCIP_FILE *file)
Definition: reader_cnf.c:136
#define SCIPfreeBufferArray(scip, ptr)
Definition: scip_mem.h:142
Constraint handler for the set partitioning / packing / covering constraints .
public methods for SCIP variables
void SCIPwarningMessage(SCIP *scip, const char *formatstr,...)
Definition: scip_message.c:203
public methods for numerical tolerances
SCIP_FILE * SCIPfopen(const char *path, const char *mode)
Definition: fileio.c:140
SCIP_RETCODE SCIPsetObjsense(SCIP *scip, SCIP_OBJSENSE objsense)
Definition: scip_prob.c:1298
#define SCIPerrorMessage
Definition: pub_message.h:45
SCIP_RETCODE SCIPaddCons(SCIP *scip, SCIP_CONS *cons)
Definition: scip_prob.c:2822
Constraint handler for logicor constraints (equivalent to set covering, but algorithms are suited fo...
struct SCIP_File SCIP_FILE
Definition: pub_fileio.h:34
char * SCIPfgets(char *s, int size, SCIP_FILE *stream)
Definition: fileio.c:187
#define READER_DESC
Definition: reader_cnf.c:47
SCIP_RETCODE SCIPgetBoolParam(SCIP *scip, const char *name, SCIP_Bool *value)
Definition: scip_param.c:322
#define SCIP_CALL(x)
Definition: def.h:351
#define READER_EXTENSION
Definition: reader_cnf.c:48
public methods for constraint handler plugins and constraints
wrapper functions to map file i/o to standard or zlib file i/o
SCIP_RETCODE SCIPchgVarObj(SCIP *scip, SCIP_VAR *var, SCIP_Real newobj)
Definition: scip_var.c:4450
SCIP_RETCODE SCIPincludeReaderCnf(SCIP *scip)
Definition: reader_cnf.c:423
#define SCIPallocBufferArray(scip, ptr, num)
Definition: scip_mem.h:130
public data structures and miscellaneous methods
#define READER_NAME
Definition: reader_cnf.c:46
#define SCIP_Bool
Definition: def.h:62
SCIP_RETCODE SCIPincludeReaderBasic(SCIP *scip, SCIP_READER **readerptr, const char *name, const char *desc, const char *extension, SCIP_READERDATA *readerdata)
Definition: scip_reader.c:180
void SCIPprintSysError(const char *message)
Definition: misc.c:9926
SCIP_RETCODE SCIPcreateVar(SCIP *scip, SCIP_VAR **var, const char *name, SCIP_Real lb, SCIP_Real ub, SCIP_Real obj, SCIP_VARTYPE vartype, SCIP_Bool initial, SCIP_Bool removable, SCIP_DECL_VARDELORIG((*vardelorig)), SCIP_DECL_VARTRANS((*vartrans)), SCIP_DECL_VARDELTRANS((*vardeltrans)), SCIP_DECL_VARCOPY((*varcopy)), SCIP_VARDATA *vardata)
Definition: scip_var.c:104
Constraint handler for linear constraints in their most general form, .
SCIP_RETCODE SCIPcreateConsLogicor(SCIP *scip, SCIP_CONS **cons, const char *name, int nvars, SCIP_VAR **vars, SCIP_Bool initial, SCIP_Bool separate, SCIP_Bool enforce, SCIP_Bool check, SCIP_Bool propagate, SCIP_Bool local, SCIP_Bool modifiable, SCIP_Bool dynamic, SCIP_Bool removable, SCIP_Bool stickingatnode)
SCIP_RETCODE SCIPsetReaderCopy(SCIP *scip, SCIP_READER *reader, SCIP_DECL_READERCOPY((*readercopy)))
Definition: scip_reader.c:218
SCIP_RETCODE SCIPcreateConsLinear(SCIP *scip, SCIP_CONS **cons, const char *name, int nvars, SCIP_VAR **vars, SCIP_Real *vals, SCIP_Real lhs, SCIP_Real rhs, SCIP_Bool initial, SCIP_Bool separate, SCIP_Bool enforce, SCIP_Bool check, SCIP_Bool propagate, SCIP_Bool local, SCIP_Bool modifiable, SCIP_Bool dynamic, SCIP_Bool removable, SCIP_Bool stickingatnode)
static SCIP_DECL_READERREAD(readerReadCnf)
Definition: reader_cnf.c:384
SCIP_RETCODE SCIPaddVar(SCIP *scip, SCIP_VAR *var)
Definition: scip_prob.c:1724
SCIP_RETCODE SCIPreleaseCons(SCIP *scip, SCIP_CONS **cons)
Definition: scip_cons.c:1187
public methods for message output
#define MAXLINELEN
Definition: reader_cnf.c:50
#define SCIP_Real
Definition: def.h:150
public methods for input file readers
static void readError(SCIP *scip, int linecount, const char *errormsg)
Definition: reader_cnf.c:58
public methods for message handling
SCIP_RETCODE SCIPsetReaderRead(SCIP *scip, SCIP_READER *reader, SCIP_DECL_READERREAD((*readerread)))
Definition: scip_reader.c:266
int SCIPfclose(SCIP_FILE *fp)
Definition: fileio.c:219
public methods for reader plugins
public methods for global and local (sub)problems
char * SCIPstrtok(char *s, const char *delim, char **ptrptr)
Definition: misc.c:9975
#define ABS(x)
Definition: def.h:204
SCIP_RETCODE SCIPgetNegatedVar(SCIP *scip, SCIP_VAR *var, SCIP_VAR **negvar)
Definition: scip_var.c:1530
SCIP_RETCODE SCIPaddBoolParam(SCIP *scip, const char *name, const char *desc, SCIP_Bool *valueptr, SCIP_Bool isadvanced, SCIP_Bool defaultvalue, SCIP_DECL_PARAMCHGD((*paramchgd)), SCIP_PARAMDATA *paramdata)
Definition: scip_param.c:129
memory allocation routines