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