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