solve.c

利用空间表示的rcc8模型进行空间推理

/***************************************************************************/
/***                                                                     ***/
/***                   solve.c   (Version 2.0)                           ***/
/***                                                                     ***/
/***       Jochen Renz, Ronny Fehling, Bernhard Nebel  - July 1999       ***/
/***                                                                     ***/
/***         fehling, nebel, [e-mail]             ***/
/***                                                                     ***/
/***          http://www.informatik.uni-freiburg.de/~sppraum             ***/
/***                                                                     ***/
/***                      Institut fuer Informatik                       ***/
/***                     Albert-Ludwigs-Universitaet                     ***/
/***                           Am Flughafen 17                           ***/
/***                       79110 Freiburg, Germany                       ***/
/***                                                                     ***/
/***************************************************************************/

/*
solve [-bdefnpqrsv] [-w[v]] [-z[p]] [-m[f] number] [-g number] [-ctx file] [-o file [number]] [-h[a|A file] order] [-li <file>] [-le <file>] [file1 file2 ...]  
    solves RCC8 CSPs.
  solve [-bdefnpqrsvwz] [-m number] [-ctx file] [-o file [number]] [-h[a|A file] order] [file1 file2 ...]  
       solves RCC8 CSPs.

    options are:
    -b    return brief summary info on stdout (even if -q)
    -c <file> use the coverage info in file to split relations
    -d    give debugging info on stderr
    -e    use environment constrainedness to select next node (van Beek)
    -f    fixed ordering of variables 
    -g <number>  solve only instances larger than <number> 
    -h[a|A <file>]  <order>  use the orthogonal combination of the different 
                    heuristic methods. (a = always run all methods, the maximal
                    number of visited nodes of following methods is restricted
                    by the number required by the previously best method; 
                    A = run all methods and write output in <file>) 
                    <order> specifies the order of the methods. 
                    1=H^/dyn/loc, 2=H^/dyn/glo/, 3=H^/sta/loc, 4=H^/sta/glo, 
                    A=B^/dyn/loc, B=B^/dyn/glo/, C=B^/sta/loc, D=B^/sta/glo,
                    a=B/dyn/loc, b=B/dyn/glo/, c=B/sta/loc, d=B/sta/glo,
                    s=C/dyn/loc, t=C/dyn/glo/, u=C/sta/loc, v=C/sta/glo, 
		    S=Q/dyn/loc, T=Q/dyn/glo/, U=Q/sta/loc, V=Q/sta/glo,
                    i=I/dyn/loc, j=I/dyn/glo/, k=I/sta/loc, l=I/sta/glo,
                    <order>=2B4a means that the order is 2,B,4 and finally a.
                    NOTE: It is assumed that the files hornsplit, 
       	            closebasesplit, c8split, q8split and intersplit exist. 
                    This option overrides the options -c <file>, -f, and -e.  
    -li <file>   Include all headers of the logfile <file>
    -le <file>   Exclude all headers of the logfile <file>
                 NOTE: `-li <file>' must be given before `-le <file>'. 
    -m[f] <number> maximal number of nodes to visit (default NV_UPPER_LIMIT)
                   if -mf is set (f=factor), then the maximal number of nodes 
                   to visit is the instance size multiplicated by <number> 
    -n    restrict summary to negative (inconsistent) cases
    -o <file> <number> solve only those CSP that are tagged with [-1,0,1] 
                       (default -1) (should be a log-file)
    -p    restrict summary to positive (consistent) cases
    -q    return 0 if (last) CSP was consistent (suppresses -v) 
    -r    use random variable ordering 
    -s    return summary info on stdout (even if -q)
    -t <file> print return summary to file after typeid changes
    -v    give verbose output on stderr after solving a CSP
    -w[v] use weighted queue scheme for computing path-consistency 
          (v = van Beek)
    -x <file> print CSPs that could not been solved to file
    -z[p] compute path-consistency only (p=print path-consistent CSP to stdout)

    file[i] are CSP-input files. If none specified, solve uses stdin. 
    More than one CSP can be specified in each file (each must be 
    terminated by a point '.').

    Format of the CSP should be <node1> <node2> '(' <relations> ')'.
    First line of CSP should contain maximum node id and typeid (string).";
*/


const char *usagestring = "\
usage: solve [-bdefnpqrsv] [-w[v]] [-z[p]] [-m[f] number] [-g number] [-ctx file] [-o file [number]] [-h[a|A file] order] [-li <file>] [-le <file>] [file1 file2 ...]  
    solves RCC8 CSPs.

    options are:
    -b    return brief summary info on stdout (even if -q)
    -c <file> use the coverage info in file to split relations
    -d    give debugging info on stderr
    -e    use environment constrainedness to select next node (van Beek)
    -f    fixed ordering of variables 
    -g <number>  solve only instances larger than <number> 
    -h[a|A <file>]  <order>  use the orthogonal combination of the different 
                    heuristic methods. (a = always run all methods, the maximal
                    number of visited nodes of following methods is restricted
                    by the number required by the previously best method; 
                    A = run all methods and write output in <file>) 
                    <order> specifies the order of the methods. 
                    1=H^/dyn/loc, 2=H^/dyn/glo/, 3=H^/sta/loc, 4=H^/sta/glo, 
                    A=B^/dyn/loc, B=B^/dyn/glo/, C=B^/sta/loc, D=B^/sta/glo,
                    a=B/dyn/loc, b=B/dyn/glo/, c=B/sta/loc, d=B/sta/glo,
                    s=C/dyn/loc, t=C/dyn/glo/, u=C/sta/loc, v=C/sta/glo, 
		    S=Q/dyn/loc, T=Q/dyn/glo/, U=Q/sta/loc, V=Q/sta/glo,
                    i=I/dyn/loc, j=I/dyn/glo/, k=I/sta/loc, l=I/sta/glo,
                    <order>=2B4a means that the order is 2,B,4 and finally a.
                    NOTE: It is assumed that the files hornsplit, 
       	            closebasesplit, c8split, q8split and intersplit exist. 
                    This option overrides the options -c <file>, -f, and -e.  
    -li <file>   Include all headers of the logfile <file>
    -le <file>   Exclude all headers of the logfile <file> 
                 NOTE: `-li <file>' must be given before `-le <file>'. 
    -m[f] <number> maximal number of nodes to visit (default NV_UPPER_LIMIT)
                   if -mf is set (f=factor), then the maximal number of nodes 
                   to visit is the instance size multiplicated by <number> 
    -n    restrict summary to negative (inconsistent) cases
    -o <file> <number> solve only those CSP that are tagged with [-1,0,1] 
                       (default -1) (should be a log-file)
    -p    restrict summary to positive (consistent) cases
    -q    return 0 if (last) CSP was consistent (suppresses -v) 
    -r    use random variable ordering 
    -s    return summary info on stdout (even if -q)
    -t <file> print return summary to file after typeid changes
    -v    give verbose output on stderr after solving a CSP
    -w[v] use weighted queue scheme for computing path-consistency 
          (v = van Beek)
    -x <file> print CSPs that could not been solved to file
    -z[p] compute path-consistency only (p=print path-consistent CSP to stdout)

    file[i] are CSP-input files. If none specified, solve uses stdin. 
    More than one CSP can be specified in each file (each must be 
    terminated by a point '.').

    Format of the CSP should be <node1> <node2> '(' <relations> ')'.
    First line of CSP should contain maximum node id and typeid (string).";



#define HARD_NODES 	10000


#include "rcc8.h"
#include "rcc8io.h"
#include "rcc8op.h"

#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <sys/times.h>
#include <sys/types.h>
#include <sys/resource.h>
#include <sys/time.h>

/* should be in stdlib.h ! */
void srand48(long seedval);

/* should be in resource.h ! */
 int getrusage(int who, struct rusage *rusage);


/* switches */
int swhard;
int swdebug;
int swverbose;
int swquiet;
int swsummary;
int swbrief;
int swpositive;
int swnegative;
int swposneg;
int swsplitinfo;
int swrandomorder;
int swwqueue;
int swenvcons;
int swfixed;
int swsolveonly;
int swonlypathcons;
int swpcprint;
int swtesting;
int swmaxvisit;
int swfactor;
int sworthogonal;
int swallorthogonal; 
int swheuristicout;
int swheader;
int swminsize;

/* statistical info */
int taggedwith =5;
int maxnodeid;
char csptype[100];
char lasttype[100];
int consistent;
int cntconsistent;
int pathconsistent;
int cntpathconsistent;
int pcops;
int pcits;
int nodesvisited;
int searchdepth;
int maxdepth;
double cputicks;
double cpumicro;
int trial;
int rectrial;
long int tpcops[MAXTRIAL];
long int tpcits[MAXTRIAL];
long int tnodesvisited[MAXTRIAL];
int tmaxdepth[MAXTRIAL];
double tcputicks[MAXTRIAL];
int tconsistent[MAXTRIAL];
double cumcputicks;
double cumcpumicro;
int cntsize;
int size;
int maxnodes=NV_UPPER_LIMIT;
int minsize=0;
 
struct header headers[MAXHEADER]; 
/* int maxheader;  */

RELTYPE splitinfo[MAXSET][9];
RELTYPE horninfo[MAXSET][9];
RELTYPE c8info[MAXSET][9];
RELTYPE q8info[MAXSET][9];
RELTYPE closebaseinfo[MAXSET][9];
RELTYPE intersectinfo[MAXSET][9];

#if defined(DYNAMIC)
RELTYPE **csp;
struct entry **entry;
char **mark;
int **consval;
int prevmax=0;
#else 
RELTYPE csp[MAXCSP][MAXCSP];
struct entry entry[MAXWT][MAXCSP*MAXCSP];
char mark[MAXCSP][MAXCSP];
int consval[MAXCSP][MAXCSP];
#endif


/* files */
FILE *infile;
char infilename[200];
FILE *splitfile;
char splitfilename[200];
FILE *solveonlyfile;
char solveonlyname[200];
FILE *summaryfile;
char summaryname[200];
FILE *hardfile;
char hardfilename[200];
FILE *heuristicfile;
char heuristicfilename[200];
FILE *headerfile;
char headerfilename[200];

/* timing info */
struct tms local_before, local_after, global_before, global_after;
struct rusage rus_glb_before,rus_glb_after,rus_lcl_before,rus_lcl_after;

/* random variable */
unsigned int randomseed = 0;



void initrand(unsigned int seed)
{
  if (seed == 0)
    randomseed = time(NULL);
  else
    randomseed = seed;

  srand48(randomseed);
}



int path_cons(csp, maxnodeid, node1, node2)
     int       maxnodeid, node1, node2;
#if defined(DYNAMIC) 
     RELTYPE   **csp;
#else 
     RELTYPE csp[MAXCSP][MAXCSP];
#endif
{
  if (swwqueue==1) 
    return(path_cons_wq(csp,maxnodeid,node1,node2));
  else if(swwqueue==2)
    return(path_cons_vb(csp,maxnodeid,node1,node2));
  else
    return(path_cons1(csp,maxnodeid,node1,node2));
}



void usage()
{
  fprintf(stderr,"%s\n",usagestring);
  exit(-1);
}



int int_compare(const void *p1, const void *p2){
  const long int *i1=p1, *i2=p2;
  return(((*i1 < *i2) ? -1 
	  : ((*i1 == *i2) ? 0 : 1)));
}



int double_compare( const void *p1, const void *p2){
  const double *i1=p1, *i2=p2;
  return(((*i1 < *i2) ? -1 
	  : ((*i1 == *i2) ? 0 : 1)));
}



void init_statistics()
{
  trial = 0;
  rectrial = 0;
  cntpathconsistent = 0;
  cntconsistent = 0;
  cntsize = 0; 
}

void heuristic_summary(int minnodes, char *order, char first, int *ordernode, FILE *file)
{
  int i=0;
  char name[20];
  fprintf(file,"%s cons: %i nodes: %i method: %c\n",csptype,consistent,minnodes,first); 
  while(order[i]!='\0') {
    if(ordernode[i]==0) {
      i++;
      continue;
    }
    switch(order[i]) {
    case '1': strcpy(name,"H^/dyn/loc");break;
    case '2': strcpy(name,"H^/dyn/glo");break;
    case '3': strcpy(name,"H^/sta/loc");break;
    case '4': strcpy(name,"H^/sta/glo");break;
    case 'A': strcpy(name,"B^/dyn/loc");break;
    case 'B': strcpy(name,"B^/dyn/glo");break;
    case 'C': strcpy(name,"B^/sta/loc");break;
    case 'D': strcpy(name,"B^/sta/glo");break;
    case 'a': strcpy(name,"B/dyn/loc");break;
    case 'b': strcpy(name,"B/dyn/glo");break;
    case 'c': strcpy(name,"B/sta/loc");break;
    case 'd': strcpy(name,"B/sta/glo");break;
    case 'S': strcpy(name,"Q/dyn/loc");break;
    case 'T': strcpy(name,"Q/dyn/glo");break;
    case 'U': strcpy(name,"Q/sta/loc");break;
    case 'V': strcpy(name,"Q/sta/glo");break;
    case 's': strcpy(name,"C/dyn/loc");break;
    case 't': strcpy(name,"C/dyn/glo");break;
    case 'u': strcpy(name,"C/sta/loc");break;
    case 'v': strcpy(name,"C/sta/glo");break;
    case 'i': strcpy(name,"I/dyn/loc");break;
    case 'j': strcpy(name,"I/dyn/glo");break;
    case 'k': strcpy(name,"I/sta/loc");break;
    case 'l': strcpy(name,"I/sta/glo");break;
    default: strcpy(name,"unknown");
    }
    fprintf(file,"%s: %i\n",name,ordernode[i]);
    i++;
  }
  fflush(file);
}

void print_summary(int brief, char *lasttype, FILE *file)
{
  float sum, avg, med, seventy, ninety, ninetynine, hundred;
  register int i;

  sum = 0.0;
  for (i = 0; i < trial; i++)
    sum += (float)(tcputicks[i]);

  if(!swtesting && !brief) {
    fprintf(file,"time used:\n");
    fprintf(file,"global: %f sec\n",cumcputicks);
    fprintf(file,"local:  %f sec\n",sum);
    fprintf(file,"number: %d\n",trial);
  }

  if (!brief) fprintf(file,"SUMMARY INFORMATION:\n");
  if (trial < 1) {
    fprintf(file,"  No CSP given.\n");
    return;
  }

  if (brief) fprintf(file,"%s \n",lasttype);
  else 
    fprintf(file,"  CSP size=%5.1f (%s), last type=%s\n",
	   ((float)cntsize)/((float)(trial)),
	   ((size == 0) ? "avg." : "all"),
	   lasttype);

  if(swonlypathcons)
    fprintf(file,"  Only checked path-consistency\n");
  if (brief){
      fprintf(file," %5.2f (path) %5.2f (global) ",
		    (((float)cntpathconsistent)/((float)trial))*100.0,
		    (((float)cntconsistent)/((float)trial))*100.0);
  }
  else{
      fprintf(file,"  Consistent: path=%6.2f%%, global=%6.2f%%\n",
	      (((float)cntpathconsistent)/((float)trial))*100.0,
	      (((float)cntconsistent)/((float)trial))*100.0);
  }
  if (swpositive) {
    if (brief) fprintf(file,"C \n");
    else fprintf(file,"  Statistics on CONSISTENT cases only:\n");
  }
  else if (swnegative) {
    if (brief) fprintf(file,"I \n");
    else fprintf(file,"  Statistics on INCONSISTENT cases only:\n");
  }
  else if (brief) fprintf(file,"\n");

  trial = rectrial;

  if (trial <= 0) {
    if (brief) fprintf(file," -------\n");
    else fprintf(file,"  *** no cases\n");
    return;
  }

  if(!brief)
    fprintf(file,"\n\t    average  percentile:   (50)\t   (70)\t   (90)\t   (99)\t  (100)\n");

  avg = sum/((float)trial);
  qsort(tcputicks,trial,sizeof(double),&double_compare);
  if (trial == 1) {
    med = (float)tcputicks[0];
    seventy = (float)tcputicks[0];
    ninety = (float)tcputicks[0];
    ninetynine = (float)tcputicks[0];
    hundred = (float)tcputicks[0];
  } else {
    med = ((float)(tcputicks[(trial/2)-1]+tcputicks[trial/2]))/2.0;
    seventy = ((float)(tcputicks[((trial*7)/10)-1]+
		       tcputicks[((trial*7)/10)]))/2.0;
    ninety = ((float)(tcputicks[((trial*9)/10)-1]+
		       tcputicks[((trial*9)/10)]))/2.0;
    ninetynine = ((float)(tcputicks[((trial*99)/100)-1]+
		       tcputicks[((trial*99)/100)]))/2.0;
    hundred = (float) tcputicks[trial-1];
  }
  if (brief)
    fprintf(file," %6.5f %6.5f %6.5f %6.5f %6.5f %6.5f (cpu)\n",avg,med,seventy,ninety,ninetynine, hundred);
  else
    fprintf(file,"  CPU time: %6.5f\t\t%6.5f %6.5f %6.5f %6.5f %6.5f\n",
	   avg, med, seventy, ninety, ninetynine, hundred);

  if (!brief) {
    avg = 0.0;
    for (i = 0; i < trial; i++)
      avg += (float)(tpcops[i]);
    avg = avg/((float)trial);
    qsort(tpcops,trial,sizeof(long int),&int_compare);
    if (trial == 1) {
      med = (float)tpcops[0];
      seventy = (float)tpcops[0];
      ninety = (float)tpcops[0];
      ninetynine = (float)tpcops[0];
      hundred = (float)tpcops[0];
    } else {
      med = ((float)(tpcops[(trial/2)-1]+tpcops[trial/2]))/2.0;
      seventy = ((float)(tpcops[((trial*7)/10)-1]+
			 tpcops[((trial*7)/10)]))/2.0;
      ninety = ((float)(tpcops[((trial*9)/10)-1]+
			tpcops[((trial*9)/10)]))/2.0;
      ninetynine = ((float)(tpcops[((trial*99)/100)-1]+
			    tpcops[((trial*99)/100)]))/2.0;
      hundred = (float) tpcops[trial-1];
    }
      fprintf(file,"  PC ops:   %7.0f\t\t%7.0f %7.0f %7.0f %7.0f %7.0f\n",
	      avg, med, seventy, ninety, ninetynine, hundred);
 

      avg = 0.0;
      for (i = 0; i < trial; i++)
	avg += (float)(tpcits[i]);
      avg = avg/((float)trial);
      qsort(tpcits,trial,sizeof(long int),&int_compare);
      if (trial == 1) {
	med = (float)tpcits[0];
	seventy = (float)tpcits[0];
	ninety = (float)tpcits[0];
	ninetynine = (float)tpcits[0];
	hundred = (float)tpcits[0];
      } else {
	med = ((float)(tpcits[(trial/2)-1]+tpcits[trial/2]))/2.0;
	seventy = ((float)(tpcits[((trial*7)/10)-1]+
			   tpcits[((trial*7)/10)]))/2.0;
	ninety = ((float)(tpcits[((trial*9)/10)-1]+
			  tpcits[((trial*9)/10)]))/2.0;
	ninetynine = ((float)(tpcits[((trial*99)/100)-1]+
			      tpcits[((trial*99)/100)]))/2.0; 
	hundred = (float) tpcits[trial-1];
      }
      fprintf(file,"  PC its:   %7.1f\t\t%7.1f %7.1f %7.1f %7.1f %7.1f\n",
	      avg, med, seventy, ninety, ninetynine, hundred);
  }

  avg = 0.0;
  for (i = 0; i < trial; i++)
    avg += (float)(tnodesvisited[i]);
  avg = avg/((float)trial);
  qsort(tnodesvisited,trial,sizeof(long int),&int_compare);
  
  if (trial == 1) {
    med = (float)tnodesvisited[0];
    seventy = (float)tnodesvisited[0];
    ninety = (float)tnodesvisited[0];
    ninetynine = (float)tnodesvisited[0];
    hundred = (float)tnodesvisited[0];
  } else {
    med = ((float)(tnodesvisited[(trial/2)-1]+tnodesvisited[trial/2]))/2.0;
    seventy = ((float)(tnodesvisited[((trial*7)/10)-1]+
		       tnodesvisited[((trial*7)/10)]))/2.0;
    ninety = ((float)(tnodesvisited[((trial*9)/10)-1]+
		       tnodesvisited[((trial*9)/10)]))/2.0;
    ninetynine = ((float)(tnodesvisited[((trial*99)/100)-1]+
		       tnodesvisited[((trial*99)/100)]))/2.0;
    hundred = (float) tnodesvisited[trial-1];
  }
  if (brief)
    fprintf(file," %6.5f %6.5f %6.5f %6.5f %6.5f %6.5f (nv)\n",
	   avg, med, seventy, ninety, ninetynine, hundred);
  else