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