1 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
2 /* */
3 /* This file is part of the program and library */
4 /* SCIP --- Solving Constraint Integer Programs */
5 /* */
6 /* Copyright (C) 2002-2021 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
readError(SCIP * scip,int linecount,const char * errormsg)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
readWarning(SCIP * scip,int linecount,const char * warningmsg)70 void readWarning(
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
readCnfLine(SCIP * scip,SCIP_FILE * file,char * buffer,int size,int * linecount)81 SCIP_RETCODE readCnfLine(
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
readCnf(SCIP * scip,SCIP_FILE * file)138 SCIP_RETCODE readCnf(
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 */
347 SCIP_CALL( SCIPsetObjsense(scip, SCIP_OBJSENSE_MAXIMIZE) );
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
SCIP_DECL_READERCOPY(readerCopyCnf)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 */
379 SCIP_CALL( SCIPincludeReaderCnf(scip) );
380
381 return SCIP_OKAY;
382 }
383
384
385 /** problem reading method of reader */
386 static
SCIP_DECL_READERREAD(readerReadCnf)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 */
SCIPincludeReaderCnf(SCIP * scip)432 SCIP_RETCODE SCIPincludeReaderCnf(
433 SCIP* scip /**< SCIP data structure */
434 )
435 {
436 SCIP_READER* reader;
437
438 /* include reader */
439 SCIP_CALL( SCIPincludeReaderBasic(scip, &reader, READER_NAME, READER_DESC, READER_EXTENSION, NULL) );
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 */
446 SCIP_CALL( SCIPaddBoolParam(scip,
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
453