reader_cnf.c

Go to the documentation of this file.

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/*                                                                           */
/*                  This file is part of the program and library             */
/*         SCIP --- Solving Constraint Integer Programs                      */
/*                                                                           */
/*  Copyright (c) 2002-2024 Zuse Institute Berlin (ZIB)                      */
/*                                                                           */
/*  Licensed under the Apache License, Version 2.0 (the "License");          */
/*  you may not use this file except in compliance with the License.         */
/*  You may obtain a copy of the License at                                  */
/*                                                                           */
/*      http://www.apache.org/licenses/LICENSE-2.0                           */
/*                                                                           */
/*  Unless required by applicable law or agreed to in writing, software      */
/*  distributed under the License is distributed on an "AS IS" BASIS,        */
/*  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. */
/*  See the License for the specific language governing permissions and      */
/*  limitations under the License.                                           */
/*                                                                           */
/*  You should have received a copy of the Apache-2.0 license                */
/*  along with SCIP; see the file LICENSE. If not visit scipopt.org.         */
/*                                                                           */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
 
/**@file   reader_cnf.c
 * @ingroup DEFPLUGINS_READER
 * @brief  CNF file reader
 * @author Thorsten Koch
 * @author Tobias Achterberg
 *
 * The DIMACS CNF (conjunctive normal form) is a file format used for example for SAT problems. For a detailed description of
 * this format see http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html .
 */
 
/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
 
#include "blockmemshell/memory.h"
#include "scip/cons_linear.h"
#include "scip/cons_logicor.h"
#include "scip/cons_setppc.h"
#include "scip/pub_fileio.h"
#include "scip/pub_message.h"
#include "scip/pub_misc.h"
#include "scip/pub_reader.h"
#include "scip/reader_cnf.h"
#include "scip/scip_cons.h"
#include "scip/scip_mem.h"
#include "scip/scip_message.h"
#include "scip/scip_numerics.h"
#include "scip/scip_param.h"
#include "scip/scip_prob.h"
#include "scip/scip_reader.h"
#include "scip/scip_var.h"
#include <string.h>
 
#define READER_NAME             "cnfreader"
#define READER_DESC             "file reader for SAT problems in conjunctive normal form"
#define READER_EXTENSION        "cnf"
 
#define MAXLINELEN       65536
 
 
/*
 * cnf reader internal methods
 */
 
static
void readError(
   SCIP*                 scip,               /**< SCIP data structure */
   int                   linecount,          /**< line number of error */
   const char*           errormsg            /**< error message */
   )
{
   assert( scip != NULL );
   SCIPerrorMessage("read error in line <%d>: %s\n", linecount, errormsg);
}
 
static
void readWarning(
   SCIP*                 scip,               /**< SCIP data structure */
   int                   linecount,          /**< line number of error */
   const char*           warningmsg          /**< warning message */
   )
{
   SCIPwarningMessage(scip, "Line <%d>: %s\n", linecount, warningmsg);
}
 
/** reads the next non-empty non-comment line of a cnf file */
static
SCIP_RETCODE readCnfLine(
   SCIP*                 scip,               /**< SCIP data structure */
   SCIP_FILE*            file,               /**< input file */
   char*                 buffer,             /**< buffer for storing the input line */
   int                   size,               /**< size of the buffer */
   int*                  linecount           /**< pointer to the line number counter */
   )
{
   char* line;
   int linelen;
 
   assert(file != NULL);
   assert(buffer != NULL);
   assert(size >= 2);
   assert(linecount != NULL);
 
   do
   {
      (*linecount)++;
      line = SCIPfgets(buffer, size, file);
      if( line != NULL )
      {
         linelen = (int)strlen(line);
         if( linelen == size-1 )
         {
            char s[SCIP_MAXSTRLEN];
            (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "line too long (exceeds %d characters)", size-2);
            readError(scip, *linecount, s);
            return SCIP_READERROR;
         }
      }
      else
         linelen = 0;
   }
   while( line != NULL && (*line == 'c' || *line == '\n') );
 
   if( line != NULL && linelen >= 2 && line[linelen-2] == '\n' )
      line[linelen-2] = '\0';
   else if( linelen == 0 )
      *buffer = '\0';
 
   assert((line == NULL) == (*buffer == '\0'));
 
   return SCIP_OKAY;
}
 
/* Read SAT formula in "CNF File Format".
 * 
 *  The specification is taken from the
 *
 *  Satisfiability Suggested Format
 *
 *  Online available at http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/Benchmarks/SAT/satformat.ps
 *
 *  The method reads all files of CNF format. Other formats (SAT, SATX, SATE) are not supported.
 */  
static
SCIP_RETCODE readCnf(
   SCIP*                 scip,               /**< SCIP data structure */   
   SCIP_FILE*            file                /**< input file */
   )
{
   SCIP_RETCODE retcode;
   SCIP_VAR** vars;
   SCIP_VAR** clausevars;
   SCIP_CONS* cons;
   int* varsign;
   char* tok;
   char* nexttok;
   char line[MAXLINELEN];
   char format[SCIP_MAXSTRLEN];
   char varname[SCIP_MAXSTRLEN];
   char s[SCIP_MAXSTRLEN];
   SCIP_Bool initialconss;
   SCIP_Bool dynamicconss;
   SCIP_Bool dynamiccols;
   SCIP_Bool dynamicrows;
   SCIP_Bool useobj;
   int linecount;
   int clauselen;
   int clausenum;
   int nvars;
   int nclauses;
   int varnum;
   int v;
 
   assert(scip != NULL);
   assert(file != NULL);
 
   linecount = 0;
 
   /* read header */
   SCIP_CALL( readCnfLine(scip, file, line, (int) sizeof(line), &linecount) );
   if( *line != 'p' )
   {
      readError(scip, linecount, "problem declaration line expected");
      return SCIP_READERROR;
   }
   /* cppcheck-suppress invalidScanfFormatWidth_smaller */
   if( sscanf(line, "p %8s %d %d", format, &nvars, &nclauses) != 3 )
   {
      readError(scip, linecount, "invalid problem declaration (must be 'p cnf <nvars> <nclauses>')");
      return SCIP_READERROR;
   }
   if( strcmp(format, "cnf") != 0 )
   {
      (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid format tag <%s> (must be 'cnf')", format);
      readError(scip, linecount, s);
      return SCIP_READERROR;
   }
   if( nvars <= 0 )
   {
      (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid number of variables <%d> (must be positive)", nvars);
      readError(scip, linecount, s);
      return SCIP_READERROR;
   }
   if( nclauses <= 0 )
   {
      (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid number of clauses <%d> (must be positive)", nclauses);
      readError(scip, linecount, s);
      return SCIP_READERROR;
   }
 
   /* get parameter values */
   SCIP_CALL( SCIPgetBoolParam(scip, "reading/initialconss", &initialconss) );
   SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamicconss", &dynamicconss) );
   SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamiccols", &dynamiccols) );
   SCIP_CALL( SCIPgetBoolParam(scip, "reading/dynamicrows", &dynamicrows) );
   SCIP_CALL( SCIPgetBoolParam(scip, "reading/cnfreader/useobj", &useobj) );
 
   /* get temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &clausevars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &varsign, nvars) );
 
   /* create the variables */
   for( v = 0; v < nvars; ++v )
   {
      (void) SCIPsnprintf(varname, SCIP_MAXSTRLEN, "x%d", v+1);
      SCIP_CALL( SCIPcreateVar(scip, &vars[v], varname, 0.0, 1.0, 0.0, SCIP_VARTYPE_BINARY, !dynamiccols, dynamiccols,
            NULL, NULL, NULL, NULL, NULL) );
      SCIP_CALL( SCIPaddVar(scip, vars[v]) );
      varsign[v] = 0;
   }
 
   /* read clauses */
   clausenum = 0;
   clauselen = 0;
   do
   {
      retcode = readCnfLine(scip, file, line, (int) sizeof(line), &linecount);
      if( retcode != SCIP_OKAY )
         goto TERMINATE;
 
      if( *line != '\0' && *line != '%' )
      {
         tok = SCIPstrtok(line, " \f\n\r\t", &nexttok);
         while( tok != NULL )
         {
            /* parse literal and check for errors */
            /* coverity[secure_coding] */
            if( sscanf(tok, "%d", &v) != 1 )
            {
               (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid literal <%s>", tok);
               readError(scip, linecount, s);
               retcode = SCIP_READERROR;
               goto TERMINATE;
            }
 
            /* interpret literal number: v == 0: end of clause, v < 0: negated literal, v > 0: positive literal */
            if( v == 0 )
            {
               /* end of clause: construct clause and add it to SCIP */
               if( clauselen == 0 )
                  readWarning(scip, linecount, "empty clause detected in line -- problem infeasible");
 
               clausenum++;
               (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "c%d", clausenum);
 
               if( SCIPfindConshdlr(scip, "logicor") != NULL )
               {
                  /* if the constraint handler logicor exit create a logicor constraint */
                  SCIP_CALL( SCIPcreateConsLogicor(scip, &cons, s, clauselen, clausevars,
                        initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
               }
               else if( SCIPfindConshdlr(scip, "setppc") != NULL )
               {
                  /* if the constraint handler logicor does not exit but constraint
                   *  handler setppc create a setppc constraint */
                  SCIP_CALL( SCIPcreateConsSetcover(scip, &cons, s, clauselen, clausevars,
                        initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
               }
               else
               {
                  /* if none of the previous constraint handler exits create a linear
                   * constraint */
                  SCIP_Real* vals;
                  int i;
 
                  SCIP_CALL( SCIPallocBufferArray(scip, &vals, clauselen) );
 
                  for( i = 0; i < clauselen; ++i )
                     vals[i] = 1.0;
 
                  SCIP_CALL( SCIPcreateConsLinear(scip, &cons, s, clauselen, clausevars, vals, 1.0, SCIPinfinity(scip),
                        initialconss, TRUE, TRUE, TRUE, TRUE, FALSE, FALSE, dynamicconss, dynamicrows, FALSE) );
 
                  SCIPfreeBufferArray(scip, &vals);
               }
 
               SCIP_CALL( SCIPaddCons(scip, cons) );
               SCIP_CALL( SCIPreleaseCons(scip, &cons) );
               clauselen = 0;
            }
            else if( v >= -nvars && v <= nvars )
            {
               if( clauselen >= nvars )
               {
                  readError(scip, linecount, "too many literals in clause");
                  retcode = SCIP_READERROR;
                  goto TERMINATE;
               }
 
               /* add literal to clause */
               varnum = ABS(v)-1;
               if( v < 0 )
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, vars[varnum], &clausevars[clauselen]) );
                  varsign[varnum]--;
               }
               else
               {
                  clausevars[clauselen] = vars[varnum];
                  varsign[varnum]++;
               }
               clauselen++;
            }
            else
            {
               (void) SCIPsnprintf(s, SCIP_MAXSTRLEN, "invalid variable number <%d>", ABS(v));
               readError(scip, linecount, s);
               retcode = SCIP_READERROR;
               goto TERMINATE;
            }
 
            /* get next token */
            tok = SCIPstrtok(NULL, " \f\n\r\t", &nexttok);
         }
      }
   }
   while( *line != '\0' && *line != '%' );
 
   /* check for additional literals */
   if( clauselen > 0 )
   {
      SCIPwarningMessage(scip, "found %d additional literals after last clause\n", clauselen);
   }
 
   /* check number of clauses */
   if( clausenum != nclauses )
   {
      SCIPwarningMessage(scip, "expected %d clauses, but found %d\n", nclauses, clausenum);
   }
 
 TERMINATE:
   /* change objective values and release variables */
   SCIP_CALL( SCIPsetObjsense(scip, SCIP_OBJSENSE_MAXIMIZE) );
   for( v = 0; v < nvars; ++v )
   {
      if( useobj )
      {
         SCIP_CALL( SCIPchgVarObj(scip, vars[v], (SCIP_Real)varsign[v]) );
      }
      SCIP_CALL( SCIPreleaseVar(scip, &vars[v]) );
   }
 
   /* free temporary memory */
   SCIPfreeBufferArray(scip, &varsign);
   SCIPfreeBufferArray(scip, &clausevars);
   SCIPfreeBufferArray(scip, &vars);
 
   return retcode;
}
 
 
/*
 * Callback methods
 */
 
/** copy method for reader plugins (called when SCIP copies plugins) */
static
SCIP_DECL_READERCOPY(readerCopyCnf)
{  /*lint --e{715}*/
   assert(scip != NULL);
   assert(reader != NULL);
   assert(strcmp(SCIPreaderGetName(reader), READER_NAME) == 0);
 
   /* call inclusion method of reader */
   SCIP_CALL( SCIPincludeReaderCnf(scip) );
 
   return SCIP_OKAY;
}
 
 
/** problem reading method of reader */
static
SCIP_DECL_READERREAD(readerReadCnf)
{  /*lint --e{715}*/
   SCIP_FILE* f;
   SCIP_RETCODE retcode;
 
   assert(reader != NULL);
   assert(strcmp(SCIPreaderGetName(reader), READER_NAME) == 0);
   assert(filename != NULL);
   assert(result != NULL);
 
   /* open file */
   f = SCIPfopen(filename, "r");
   if( f == NULL )
   {
      SCIPerrorMessage("cannot open file <%s> for reading\n", filename);
      SCIPprintSysError(filename);
      return SCIP_NOFILE;
   }
 
   /* create problem */
   retcode = SCIPcreateProb(scip, filename, NULL, NULL, NULL, NULL, NULL, NULL, NULL);
   if( retcode != SCIP_OKAY )
   {
      SCIPerrorMessage("Error creating problem for filename <%s>\n", filename);
      SCIPfclose(f);
      return retcode;
   }
 
   /* read cnf file */
   retcode = readCnf(scip, f);
 
   /* close file */
   SCIPfclose(f);
 
   *result = SCIP_SUCCESS;
 
   return retcode;
}
 
 
/*
 * cnf file reader specific interface methods
 */
 
/** includes the cnf file reader in SCIP */
SCIP_RETCODE SCIPincludeReaderCnf(
   SCIP*                 scip                /**< SCIP data structure */
   )
{
   SCIP_READER* reader;
 
   /* include reader */
   SCIP_CALL( SCIPincludeReaderBasic(scip, &reader, READER_NAME, READER_DESC, READER_EXTENSION, NULL) );
 
   /* set non fundamental callbacks via setter functions */
   SCIP_CALL( SCIPsetReaderCopy(scip, reader, readerCopyCnf) );
   SCIP_CALL( SCIPsetReaderRead(scip, reader, readerReadCnf) );
 
   /* add cnf reader parameters */
   SCIP_CALL( SCIPaddBoolParam(scip,
         "reading/cnfreader/useobj", "should an artificial objective, depending on the number of clauses a variable appears in, be used?",
         NULL, FALSE, FALSE, NULL, NULL) );
 
   return SCIP_OKAY;
}