/* Copyright (C) 2001  Dale Schuurmans, Finnegan Southey                     */
/* This work is licensed under the Gnu General Public License (see gpl.txt). */

/* Transforms SAT instance to an ILP instance (in LP format)        *
 * simply by encoding a zero objective and encoding the constraints */

#include <stdlib.h>
#include <stdio.h>
#include <string.h>

int main(int argc, char **argv)
{
   int n, m, x, c, k, lit;

   FILE *in, *out;
   char ch;
	 int fnum;
	 char outname[10000];
	 char *outputDir;
	 char* lastslash;

	 if (argc < 3) {
		 printf("Incorrect number of arguments.\n");
		 printf("Usage: cnf2lp <output dir> <cnf file> [cnf file] ...\n");
		 exit(1);
	 }

	 outputDir = argv[1];

	 for (fnum = 2; fnum < argc; fnum++) {

		 in = fopen(argv[fnum], "r");
		 if (in == NULL) {
			 printf("Error opening input file: %s\n", argv[fnum]);
			 exit(1);
		 }

	 		strcpy(outname, outputDir);
			if (outputDir[strlen(outputDir)-1] != '/')
				strcat(outname, "/");
			lastslash = strrchr(argv[fnum], '/');
			if (lastslash == NULL)
	 	    strcat(outname, argv[fnum]);
			else
	 	    strcat(outname, lastslash + 1);
			strcpy(strrchr(outname, '.'), ".lp");

		 out = fopen(outname, "w");
		 if (out == NULL) {
			 printf("Error opening output file: %s\n", outname);
			 exit(1);
		 }

		 ch = fgetc(in);
	   while (ch == 'c' || ch == '#') {
	      while (fgetc(in) != '\n');
	      ch = fgetc(in);
	   }
	
	   fscanf(in, " cnf %d %d", &n, &m);
	
	   fprintf(out, "max\n");
	   fprintf(out, "\n");
	   for (x = 1; x <= 2*n-1; x++) fprintf(out, "0x%d + ", x);
	   fprintf(out, "0x%d\n", 2*n);
	   fprintf(out, "\n");
	
	   fprintf(out, "st\n");
	   fprintf(out, "\n");
	   
	   for (x = 1; x <= 2*n; x++) fprintf(out, "x%d  >= 0\nx%d  <= 1\n", x, x);
	   for (x = 1; x <= n; x++) fprintf(out, "x%d + x%d = 1\n", x, n+x);
	   
	   for (c = 0; c < m; c++) {
	      k = 0;
	      fscanf(in, "%d", &lit);
	      if (lit) {
	         k++;
	         fprintf(out, "x%d ", abs(lit) + (lit > 0 ? 0 : n));
	      } else
	         continue;
	      for (fscanf(in, "%d", &lit); lit; fscanf(in, "%d", &lit)) {
	         k++;
	         fprintf(out, "+ x%d ", abs(lit) + (lit > 0 ? 0 : n));
	      }
	      fprintf(out, " >= 1\n");
	   }
	   fprintf(out, "\n");
	
	   fprintf(out, "binary\n");
	   fprintf(out, "\n");
	   
	   for (x = 1; x <= 2*n; x++) {
			 fprintf(out, "x%d ", x);
			 if (x % 10 == 0)
		   	 fprintf(out, "\n");  /* Need these line breaks or CPLEX complains. */
		 }

	   fprintf(out, "\n");
	   fprintf(out, "\n");
	   
	   fprintf(out, "end\n");
	   fclose(out);
	   fclose(in);
	 }

	 return 0;
}