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-2019 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  /* coverity[secure_coding] */
240  if( sscanf(tok, "%d", &v) != 1 )
241  {
242  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid literal <%s>", tok);
243  readError(scip, linecount, s);
244  retcode = SCIP_READERROR;
245  goto TERMINATE;
246  }
247 
248  /* interpret literal number: v == 0: end of clause, v < 0: negated literal, v > 0: positive literal */
249  if( v == 0 )
250  {
251  /* end of clause: construct clause and add it to SCIP */
252  if( clauselen == 0 )
253  readWarning(scip, linecount, "empty clause detected in line -- problem infeasible");
254 
255  clausenum++;
256  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "c%d", clausenum);
257 
258  if( SCIPfindConshdlr(scip, "logicor") != NULL )
259  {
260  /* if the constraint handler logicor exit create a logicor constraint */
261  SCIP_CALL( SCIPcreateConsLogicor(scip, &cons, s, clauselen, clausevars,
262  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
263  }
264  else if( SCIPfindConshdlr(scip, "setppc") != NULL )
265  {
266  /* if the constraint handler logicor does not exit but constraint
267  * handler setppc create a setppc constraint */
268  SCIP_CALL( SCIPcreateConsSetcover(scip, &cons, s, clauselen, clausevars,
269  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
270  }
271  else
272  {
273  /* if none of the previous constraint handler exits create a linear
274  * constraint */
275  SCIP_Real* vals;
276  int i;
277 
278  SCIP_CALL( SCIPallocBufferArray(scip, &vals, clauselen) );
279 
280  for( i = 0; i < clauselen; ++i )
281  vals[i] = 1.0;
282 
283  SCIP_CALL( SCIPcreateConsLinear(scip, &cons, s, clauselen, clausevars, vals, 1.0, SCIPinfinity(scip),
284  initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
285 
286  SCIPfreeBufferArray(scip, &vals);
287  }
288 
289  SCIP_CALL( SCIPaddCons(scip, cons) );
290  SCIP_CALL( SCIPreleaseCons(scip, &cons) );
291  clauselen = 0;
292  }
293  else if( v >= -nvars && v <= nvars )
294  {
295  if( clauselen >= nvars )
296  {
297  readError(scip, linecount, "too many literals in clause");
298  retcode = SCIP_READERROR;
299  goto TERMINATE;
300  }
301 
302  /* add literal to clause */
303  varnum = ABS(v)-1;
304  if( v < 0 )
305  {
306  SCIP_CALL( SCIPgetNegatedVar(scip, vars[varnum], &clausevars[clauselen]) );
307  varsign[varnum]--;
308  }
309  else
310  {
311  clausevars[clauselen] = vars[varnum];
312  varsign[varnum]++;
313  }
314  clauselen++;
315  }
316  else
317  {
318  (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid variable number <%d>", ABS(v));
319  readError(scip, linecount, s);
320  retcode = SCIP_READERROR;
321  goto TERMINATE;
322  }
323 
324  /* get next token */
325  tok = SCIPstrtok(NULL, " \f\n\r\t", &nexttok);
326  }
327  }
328  }
329  while( *line != '\0' && *line != '%' );
330 
331  /* check for additional literals */
332  if( clauselen > 0 )
333  {
334  SCIPwarningMessage(scip, "found %d additional literals after last clause\n", clauselen);
335  }
336 
337  /* check number of clauses */
338  if( clausenum != nclauses )
339  {
340  SCIPwarningMessage(scip, "expected %d clauses, but found %d\n", nclauses, clausenum);
341  }
342 
343  TERMINATE:
344  /* change objective values and release variables */
346  for( v = 0; v < nvars; ++v )
347  {
348  if( useobj )
349  {
350  SCIP_CALL( SCIPchgVarObj(scip, vars[v], (SCIP_Real)varsign[v]) );
351  }
352  SCIP_CALL( SCIPreleaseVar(scip, &vars[v]) );
353  }
354 
355  /* free temporary memory */
356  SCIPfreeBufferArray(scip, &varsign);
357  SCIPfreeBufferArray(scip, &clausevars);
358  SCIPfreeBufferArray(scip, &vars);
359 
360  return retcode;
361 }
362 
363 
364 /*
365  * Callback methods
366  */
367 
368 /** copy method for reader plugins (called when SCIP copies plugins) */
369 static
370 SCIP_DECL_READERCOPY(readerCopyCnf)
371 { /*lint --e{715}*/
372  assert(scip != NULL);
373  assert(reader != NULL);
374  assert(strcmp(SCIPreaderGetName(reader), READER_NAME) == 0);
375 
376  /* call inclusion method of reader */
378 
379  return SCIP_OKAY;
380 }
381 
382 
383 /** problem reading method of reader */
384 static
385 SCIP_DECL_READERREAD(readerReadCnf)
386 { /*lint --e{715}*/
387  SCIP_FILE* f;
388  SCIP_RETCODE retcode;
389 
390  assert(reader != NULL);
391  assert(strcmp(SCIPreaderGetName(reader), READER_NAME) == 0);
392  assert(filename != NULL);
393  assert(result != NULL);
394 
395  /* open file */
396  f = SCIPfopen(filename, "r");
397  if( f == NULL )
398  {
399  SCIPerrorMessage("cannot open file <%s> for reading\n", filename);
400  SCIPprintSysError(filename);
401  return SCIP_NOFILE;
402  }
403 
404  /* create problem */
405  SCIP_CALL( SCIPcreateProb(scip, filename, NULL, NULL, NULL, NULL, NULL, NULL, NULL) );
406 
407  /* read cnf file */
408  retcode = readCnf(scip, f);
409 
410  /* close file */
411  SCIPfclose(f);
412 
413  *result = SCIP_SUCCESS;
414 
415  return retcode;
416 }
417 
418 
419 /*
420  * cnf file reader specific interface methods
421  */
422 
423 /** includes the cnf file reader in SCIP */
425  SCIP* scip /**< SCIP data structure */
426  )
427 {
428  SCIP_READER* reader;
429 
430  /* include reader */
432 
433  /* set non fundamental callbacks via setter functions */
434  SCIP_CALL( SCIPsetReaderCopy(scip, reader, readerCopyCnf) );
435  SCIP_CALL( SCIPsetReaderRead(scip, reader, readerReadCnf) );
436 
437  /* add cnf reader parameters */
439  "reading/cnfreader/useobj", "should an artificial objective, depending on the number of clauses a variable appears in, be used?",
440  NULL, FALSE, FALSE, NULL, NULL) );
441 
442  return SCIP_OKAY;
443 }
444 
SCIP_EXPORT const char * SCIPreaderGetName(SCIP_READER *reader)
Definition: reader.c:547
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)
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)
#define NULL
Definition: def.h:253
static void readWarning(SCIP *scip, int linecount, const char *warningmsg)
Definition: reader_cnf.c:68
SCIP_CONSHDLR * SCIPfindConshdlr(SCIP *scip, const char *name)
Definition: scip_cons.c:876
public methods for SCIP parameter handling
public methods for memory management
SCIP_RETCODE SCIPincludeReaderCnf(SCIP *scip)
Definition: reader_cnf.c:424
CNF file reader.
static SCIP_DECL_READERCOPY(readerCopyCnf)
Definition: reader_cnf.c:370
#define SCIP_MAXSTRLEN
Definition: def.h:274
SCIP_RETCODE SCIPsetObjsense(SCIP *scip, SCIP_OBJSENSE objsense)
Definition: scip_prob.c:1241
void SCIPwarningMessage(SCIP *scip, const char *formatstr,...)
Definition: scip_message.c:122
static SCIP_RETCODE readCnfLine(SCIP *scip, SCIP_FILE *file, char *buffer, int size, int *linecount)
Definition: reader_cnf.c:79
SCIP_RETCODE SCIPgetBoolParam(SCIP *scip, const char *name, SCIP_Bool *value)
Definition: scip_param.c:240
SCIP_RETCODE SCIPsetReaderRead(SCIP *scip, SCIP_READER *reader, SCIP_DECL_READERREAD((*readerread)))
Definition: scip_reader.c:185
#define FALSE
Definition: def.h:73
SCIP_RETCODE SCIPsetReaderCopy(SCIP *scip, SCIP_READER *reader, SCIP_DECL_READERCOPY((*readercopy)))
Definition: scip_reader.c:137
#define TRUE
Definition: def.h:72
enum SCIP_Retcode SCIP_RETCODE
Definition: type_retcode.h:53
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:47
static SCIP_RETCODE readCnf(SCIP *scip, SCIP_FILE *file)
Definition: reader_cnf.c:136
char * SCIPstrtok(char *s, const char *delim, char **ptrptr)
Definition: misc.c:10221
#define SCIPfreeBufferArray(scip, ptr)
Definition: scip_mem.h:123
Constraint handler for the set partitioning / packing / covering constraints .
public methods for SCIP variables
public methods for numerical tolerances
SCIP_RETCODE SCIPgetNegatedVar(SCIP *scip, SCIP_VAR *var, SCIP_VAR **negvar)
Definition: scip_var.c:1530
SCIP_FILE * SCIPfopen(const char *path, const char *mode)
Definition: fileio.c:140
#define SCIPerrorMessage
Definition: pub_message.h:45
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
#define SCIP_CALL(x)
Definition: def.h:365
#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
#define SCIPallocBufferArray(scip, ptr, num)
Definition: scip_mem.h:111
SCIP_Real SCIPinfinity(SCIP *scip)
public data structures and miscellaneous methods
#define READER_NAME
Definition: reader_cnf.c:46
#define SCIP_Bool
Definition: def.h:70
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:9177
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
SCIP_RETCODE SCIPincludeReaderBasic(SCIP *scip, SCIP_READER **readerptr, const char *name, const char *desc, const char *extension, SCIP_READERDATA *readerdata)
Definition: scip_reader.c:99
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:105
Constraint handler for linear constraints in their most general form, .
SCIP_RETCODE SCIPaddVar(SCIP *scip, SCIP_VAR *var)
Definition: scip_prob.c:1667
static SCIP_DECL_READERREAD(readerReadCnf)
Definition: reader_cnf.c:385
SCIP_RETCODE SCIPchgVarObj(SCIP *scip, SCIP_VAR *var, SCIP_Real newobj)
Definition: scip_var.c:4451
public methods for message output
int SCIPsnprintf(char *t, int len, const char *s,...)
Definition: misc.c:10263
#define MAXLINELEN
Definition: reader_cnf.c:50
SCIP_RETCODE SCIPreleaseVar(SCIP *scip, SCIP_VAR **var)
Definition: scip_var.c:1251
#define SCIP_Real
Definition: def.h:164
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
void SCIPprintSysError(const char *message)
Definition: misc.c:10172
SCIP_RETCODE SCIPaddCons(SCIP *scip, SCIP_CONS *cons)
Definition: scip_prob.c:2765
int SCIPfclose(SCIP_FILE *fp)
Definition: fileio.c:219
SCIP_RETCODE SCIPreleaseCons(SCIP *scip, SCIP_CONS **cons)
Definition: scip_cons.c:1109
public methods for reader plugins
public methods for global and local (sub)problems
#define ABS(x)
Definition: def.h:218
memory allocation routines