OKlibrary  0.2.1.6
OKsolver_2002_lnk.c
Go to the documentation of this file.
00001 // Oliver Kullmann, 5.3.1998 (Frankfurt)
00002 /* Copyright 1998 - 2007, 2008, 2009, 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00013                        /* OKsolver; 5.3.1998 */
00014 
00015 /* Autor: Oliver Kullmann, Universitaet Frankfurt am Main, Germany */
00016 /* ab Februar 1999: University of Toronto, Computer Science Department */
00017 
00018 
00019 /* Hauptprogramm */
00020 
00021 /* Einheit: OK */
00022 
00023 
00024 /* 21.8.1998: Ersetzen von "ErfK" durch "NeuK" */
00025 
00026 /* 20.9.1998: Bisher wurde beim Finden einer Autarkie oder einer */
00027 /* verallg. 1-Klauseln-Elim. ein neuer "Single-"Knoten erzeugt. */
00028 /* Nun wird diese Belegung direkt ausgefuehrt, und die Auswahl */
00029 /* einer Verzweigungs-Variablen neu begonnen. */
00030 
00031 /* 13.11.1998: Resolutions-Baum-Verwaltung */
00032 
00033 /* 31.3.2000: InitAbstand2() im Falle, dass DYNAMISCH gesetzt wurde */
00034 
00035 /* 27.4.2000: Einlesen von OKVar.h */
00036 
00037 /* 24.7.2000: Die Variablen LitTab und KlTab aus der Prozedure Einlesen */
00038 /* nun mit "calloc" dynamisch erzeugt, und mit "free" dann geloescht. */
00039 
00040 /* 25.7.2000: Ersetzen der drei calloc-Aufrufe durch einen malloc-Aufruf. */
00041 
00042 /* 27.7.2000: Elimination der Rekursion (mittels Indices) */
00043 
00044 /* 29.1.2001: Nun wurde die Elimination der Rekursion dynamisch durchgefuehrt, */
00045 /* d.h., es wird nur soviel Speicherplatz fuer die lokalen Variablen angefordert, */
00046 /* wie auch wirklich benoetigt wird. */
00047 
00048 /* 29.1.2001: Die Speicherung der zweiten Belegung nun korrekt durchgefuehrt */
00049 /* (mittels Dynamisierung). */
00050 
00051 /* 30.1.2001: Elimination von OKVar.h */
00052 
00053 /* 18.2.2001: Liste von Argumenten (mit Optionen) */
00054 
00055 /* 20.2.2001: Ausgabe der Gesamtzeit. */
00056 
00057 /* 27.2.2001: Realisierung der 1-Klauseln-Elimination fuer die Eingabe */
00058 
00059 /* 28.2.2001: Freisetzen von Speicher und Datenstroemen wird nun ueber den */
00060 /* NULL-Wert geregelt. */
00061 /* 28.2.2001: Ein Syntax-Fehler fuehrt nun nicht mehr zum Abbruch. */
00062 /* 28.2.2001: Senden des Signals SIGUSR1 bewirkt Ausdruck der Statistik */
00063 /* (aber nicht in die Datei), und SIGUSR2 bewirkt Abbruch der Bearbeitung */
00064 /* der aktuellen Formel und Ausdruck der Statistik (diesmal in die Datei, */
00065 /* falls gewuenscht). */
00066 
00067 /* 3.3.2001: Dynamisierung von relVarM; die Stapelzeiger nun wirklich als */
00068 /* Zeiger; H und EK im Reduktionsmodul, EinerKl und Huelle im Filtermodul, */
00069 /* sowie relVarM, relVarK und Pfad zusammengefasst; LITTAB als Uebersetzer- */
00070 /* Option bewirkt, dass die Variablenmengen der Eingabeklauseln mit weniger */
00071 /* Speicherplatz abgespeichert werden. */
00072 
00073 /* 6.3.2001: Feld 14 (Redplus) aus der Statistikausgabe gestrichen. */
00074 
00075 
00076 /* ------------------------------------------------------------- */
00077 
00078 #include <stdio.h>
00079 #include <time.h>
00080 #include <stdlib.h>
00081 #include <math.h>
00082 #include <float.h>
00083 #include <string.h>
00084 #include <signal.h>
00085 #include <setjmp.h>
00086 #include <assert.h>
00087 #include <stddef.h>
00088 
00089 #include <sys/stat.h>
00090 #include <unistd.h>
00091 
00092 #include "OK.h"
00093 #include "BaumRes.h"
00094 #include "VarLitKlm.h"
00095 #include "Filter.h"
00096 #include "Belegung.h"
00097 #include "Abstand.h"
00098 #include "Projektion.h"
00099 #include "Einlesen.h"
00100 #include "Parameter.h"
00101 #include "Ausgaben.h"
00102 #include "Speicher.h"
00103 #include "Reduktion.h"
00104 
00105 #ifdef LOKALLERNEN
00106 #include "lokalesLernen.h"
00107 #endif
00108 
00109 #ifdef SYSTIME
00110 #include <sys/times.h>
00111 #endif
00112 
00113 /* ------------------------------------------------------------- */
00114 
00115 const bool internal = false; // keine Entwicklungsversion
00116 
00117 unsigned int Sprache = SPRACHE;
00118 unsigned int Standard = STANDARD;
00119 
00120 #ifndef BELEGUNG
00121 bool Belegung = false;
00122 #else
00123 bool Belegung = true;
00124 #endif
00125 
00126 /* Schalter: */
00127 
00128 bool Dateiausgabe = false;
00129 bool Monitor = false;
00130 bool nurVorreduktion = false;
00131 bool Schranken = false;
00132 unsigned int Zeitschranke = 0;
00133 bool randomisiert = false;
00135 bool splitting_only = false;
00137 bool splitting_n = true;
00139 bool splitting_file = false;
00141 bool splitting_abortion = false;
00142 
00143 // Setzen des voreingestellen Ausgabeformates
00144 
00145 #ifdef DIMACSAUS
00146 #  ifdef XMLAUS
00147 #    error "Keine Kombination von DIMACS- und XML-Format moeglich!"
00148 #  endif
00149 bool spezRueckgabe = true; // Kodierung des Ergebnisses im Rueckgabewert
00150 enum Ausgabeformat Format = Dimacs_Format;
00151 #else
00152 bool spezRueckgabe = false;
00153 Ausgabeformat Format = XML_Format;
00154 #endif
00155 // am 10.3.2002 fuer den SAT-Wettbewerb hinzugefuegt
00156 // falls DIMACS_Format gesetzt ist, so wird die Ausgabe einer Belegung
00157 // als Liste von wahr gemachten Literalen ausgegeben (in einer Zeile),
00158 // und die Kommentarzeile wird in zwei Zeilen aufgespalten:
00159 // der SAT-Wert (0, 1 oder 2) ergibt
00160 // s UNSATISFIABLE (SATISFIABLE, UNKNOWN)
00161 // und die restlichen Zahlen werden in eine Zeile beginnend mit "c "
00162 // geschrieben.
00163 // (Fuer den Wettbewerb muss sowohl BELEGUNG als auch DIMACSAUS
00164 // gesetzt werden.)
00165 
00166 unsigned int MAXN = 30000;
00167 unsigned int MAXL = 400000;
00168 unsigned int MAXK = 150000;
00169 
00170 /* ------------------------------------------------------------- */
00171 
00172 /* Einheiten pro Sekunde */
00173 #ifndef SYSTIME
00174   static const long EPS = CLOCKS_PER_SEC;
00175 #else
00176   static long EPS;
00177 #endif
00178 
00179 #ifdef SYSTIME
00180   struct tms SysZeit;
00181   struct tms* Zeiger = &SysZeit;
00182 #endif
00183 
00184 clock_t akkVerbrauch = 0; /* akkumulierter Verbrauch */
00185 
00186 /* ------------------------------------------------------------- */
00187 
00188 /* Die Darstellung der Eingabe */
00189 
00190 unsigned int P, P0, N, N0, K, K0, L, L0, aktN, aktP;
00191 
00192 /* Hilfsvariablen fuer Reduktion und Filter */
00193 
00194 unsigned int Runde;
00195 
00196 /* ------------------------------------------------------------- */
00197 
00198 /* Statistik */
00199 
00200 StatisticsCount Knoten, SingleKnoten, VerSingleKnoten, QuasiSingleKnoten, PureL, Autarkien, V1KlRed, FastAutarkien, InitEinerRed, neue2Klauseln, maxneue2K;
00201 
00202 StatisticsCount_short Suchbaumtiefe, Ueberschreitung2, init2Klauseln;
00203 
00204 typedef long double Probability;
00206 static Probability proportion_searched;
00208 static Probability proportion_single;
00209 
00210 static clock_t Verbrauch;
00211 
00212 static const char* aktName;
00213 static const char* Wurzel = NULL;
00214 
00216 static unsigned int Rekursionstiefe;
00217 
00218 enum Ergebniswerte {SAT = 1, UNSAT = 0, Unbestimmt = 2};
00219 
00220 static enum Ergebniswerte s = Unbestimmt; /* Ergebniswert */
00221 
00222 #ifdef ALLSAT
00223   nsat_t number_satisfying_assignments;
00224 #endif
00225 
00226 /* ------------------------------------------------------------- */
00227 
00228 /* Lokale Datenstrukturen und Variablen */
00229 
00230 /* Der Stapel, der die Belegungen fuer den jeweils zweiten Zweig enthaelt */
00231 
00232 static StapeleintragFZ zweiteBel = NULL;
00233 
00234 static unsigned int Zeiger2;
00235 static unsigned int Groesse2;
00236 
00237 /* Zur Simulation der Rekursion */
00238 
00239 enum Spruenge { SAT1, SAT2 };
00240 
00241 struct Sammlung {
00242   unsigned int P2, N2, altZeiger2;
00243   enum Spruenge Ruecksprung;
00244   unsigned int* AnzK2;
00245 #ifndef LOKALLERNEN
00246   Pfadinfo* altTiefe;
00247 #else
00248   Marken* Marke;
00249 #endif
00250 #ifdef OUTPUTTREEDATAXML
00251   // clock_t start_run_time;
00252   StatisticsCount number_2_reductions_at_new_node;
00253 #endif
00254   struct Sammlung* davor;
00255   struct Sammlung* danach;
00256 };
00257 
00258 static struct Sammlung* SatVar;
00259 static struct Sammlung* SatVar0 = NULL;
00260 /* speichert den initialen Wert von SatVar */
00261 
00262 /* ------------------------------------------------------------- */
00263 
00264 /* Monitoring the search */
00265 
00267 static unsigned int Beobachtungsniveau = 6;
00268 
00270 static unsigned int* Zweiglast = NULL;
00282 static unsigned int Gesamtlast;
00283 
00285 static unsigned int splitting_cases;
00287 static const char* splitting_store;
00289 static FILE* fpsplit = NULL;
00291 static char* splitting_decisions;
00293 static FILE* fpsplitdec = NULL;
00294 
00301 static unsigned int* beobachtet = NULL;
00303 static unsigned int totalbeobachtet;
00304 
00306 static FILE* fpmo = NULL;
00307 
00326 __inline__ static void Monitorausgabe(const unsigned int count_monitor_nodes) {
00327   static StatisticsCount old_nodes = 0;
00328   static StatisticsCount old_single_nodes = 0;
00329   static StatisticsCount old_autarkies = 0;
00330   static StatisticsCount old_2reductions = 0;
00331   static clock_t old_total_time = 0; /* in ticks */
00332   if (count_monitor_nodes > totalbeobachtet) {
00333     totalbeobachtet = count_monitor_nodes;
00334 #ifndef SYSTIME
00335     const clock_t total_time = clock() - akkVerbrauch;
00336 #else
00337     times(Zeiger);
00338     const clock_t total_time = SysZeit.tms_utime - akkVerbrauch;
00339 #endif
00340     const StatisticsCount new_nodes = Knoten - old_nodes;
00341     const double average_nodes = (double) Knoten / count_monitor_nodes;
00342     const double predicted_nodes = Gesamtlast * average_nodes;
00343     const double new_time = (double) (total_time - old_total_time) / EPS; /* in sec */
00344     const double average_time = ((double) total_time / EPS) / count_monitor_nodes;
00345     {
00346       const double predicted_remaining_time =
00347         (Gesamtlast - count_monitor_nodes) * average_time;
00348       double time_ = round(predicted_remaining_time);
00349       const double sec = fmod(time_, 60);
00350       time_ = (time_ - sec) / 60;
00351       const double min = fmod(time_, 60);
00352       time_ = (time_ - min) / 60;
00353       const double hours = fmod(time_, 24);
00354       time_ = (time_ - hours) / 24;
00355       const double days = fmod(time_, 365);
00356       const double years = (time_ - days) / 365;
00357       printf(
00358              "%6d:%7ld %9.2f %9.2E %8.2fs %8.2fs %5.0fy%4.0fd%3.0fh%3.0fm%3.0fs %5ld %5ld %4d\n",
00359              count_monitor_nodes,
00360              new_nodes,
00361              average_nodes,
00362              predicted_nodes,
00363              new_time,
00364              average_time,
00365              years, days, hours, min, sec,
00366              SingleKnoten - old_single_nodes,
00367              Autarkien - old_autarkies,
00368              Suchbaumtiefe
00369              );
00370     }
00371     if (Dateiausgabe) {
00372       const double average_new_2reductions =
00373         (new_nodes == 0) ? 0 : (double) (V1KlRed-old_2reductions)/new_nodes;
00374       assert((new_nodes != 0) || (V1KlRed == old_2reductions));
00375       fprintf(fpmo,
00376               "%9d %6ld %9.3f %9.3f %9.3f %6ld %5ld %5d %8.2f\n",
00377               count_monitor_nodes,
00378               new_nodes,
00379               average_nodes,
00380               new_time,
00381               average_time,
00382               SingleKnoten - old_single_nodes,
00383               Autarkien - old_autarkies,
00384               Suchbaumtiefe,
00385               average_new_2reductions
00386               );
00387       old_2reductions = V1KlRed;
00388     }
00389     fflush(NULL);
00390     old_nodes = Knoten;
00391     old_single_nodes = SingleKnoten;
00392     old_autarkies = Autarkien;
00393     old_total_time = total_time;
00394   }
00395 }
00396 
00404 __inline__ static void Verzweigungsliteralausgabe(const LIT x, const unsigned int Tiefe) {
00405   const VAR v = Var(x);
00406   const VZ e = (x == Literal(v, Pos)) ? Pos : Neg;
00407   if (Belegung) fprintf(fpmo, "# %-6d %7s %d\n", Tiefe, Symbol(v), e);
00408   fflush(NULL);
00409 }
00410 
00418 __inline__ static void output_decision_levels(FILE* const fp) {
00419   assert(fp);
00420   fprintf(fp, "%d ", Rekursionstiefe);
00421   for (struct {const struct Sammlung* i; ptrdiff_t c;} l = {SatVar0, 0}; l.c !=  (ptrdiff_t) Rekursionstiefe; l.i=l.i->danach, ++l.c)
00422     fprintf(fp, "%d ", l.i->altTiefe - Pfad);
00423   fprintf(fp, "\n");
00424 }
00425 
00426 
00427 /* ------------------------------------------------------------- */
00428 
00429 typedef enum { gleich = 0, groesser = 1, kleiner = 2} VERGL;
00430 
00431 /* Zur Bestimmung, ob einer Gleitpunktzahl "wirklich" groesser ist als eine andere: */
00432 
00434 static VERGL Vergleich(const float a, const float b) {
00435   const float h = b * 4 * FLT_EPSILON;
00436   if (a > b + h) return groesser;
00437   else if (a < b - h) return kleiner;
00438   else return gleich;
00439 }
00440 
00441 /* ------------------------------------------------------------- */
00442 
00443 /* Prozeduren zur Speicherverwaltung */
00444 
00445 static struct Sammlung* neuerKnoten() {
00446   struct Sammlung* s;
00447   s = (struct Sammlung*) xmalloc(sizeof(struct Sammlung) + (P + 1) * sizeof(unsigned int));
00448   s -> AnzK2 = (unsigned int*)(s + 1);
00449   s -> danach = NULL;
00450   return s;
00451 }
00452 
00453 /* ------------------------------------------------------------- */
00454 
00455 /* Randomisierung */
00456 
00457 static long unsigned int Schluessel = 1;
00458 static long unsigned int randx;
00459 static float Verhaeltnis = 0.2;
00460 
00461 __inline__ static void srand_S() { randx = Schluessel; }
00462 
00463 __inline__ static int rand_S() {
00464   return(((randx = randx * 1103515245L + 12345)>>16) & 0x7fff);
00465 }
00466 
00467 __inline__ static float Verschmierung(const double x) {
00468   return (rand_S() / ((float) 0x7fff) * Verhaeltnis + 1) * x;
00469 }
00470 
00471 /* ------------------------------------------------------------- */
00472 
00473 /* Initialisierung */
00474 
00475 void InitSat() {
00476   Groesse2 = N;
00477   zweiteBel = (StapeleintragFZ) xmalloc(Groesse2 * sizeof(StapeleintragF));
00478   SatVar0 = SatVar = neuerKnoten();
00479   SatVar -> davor = NULL;
00480   
00481   Runde = 0; Zeiger2 = 0;
00482   Rekursionstiefe = 0;
00483   proportion_searched = 0;
00484   proportion_single = 0;
00485   if (splitting_only) splitting_cases = 0;
00486 
00487   if (Monitor && (! nurVorreduktion)) {
00488     totalbeobachtet = 0;
00489     Zweiglast = (unsigned int*) xmalloc(Beobachtungsniveau * sizeof(unsigned int));
00490     {unsigned int p = 1;
00491      for (unsigned int* Z = Zweiglast+Beobachtungsniveau; Z != Zweiglast; p *= 2)
00492        *(--Z) = p;
00493      Gesamtlast = p;
00494     }
00495     beobachtet = (unsigned int*) xmalloc(Beobachtungsniveau * sizeof(unsigned int));
00496     beobachtet[0] = 0;
00497   }
00498 }
00499 
00500 static void AufraeumenSat() {
00501   struct Sammlung* Z; struct Sammlung* Z0;
00502   
00503   Knoten = SingleKnoten = VerSingleKnoten = QuasiSingleKnoten = PureL = Autarkien = V1KlRed = Suchbaumtiefe = Ueberschreitung2 = FastAutarkien = InitEinerRed = neue2Klauseln = maxneue2K = init2Klauseln = 0;
00504   proportion_searched = proportion_single = 0;
00505   Tiefe = NULL;
00506 
00507   free(zweiteBel); zweiteBel = NULL;
00508 
00509   Z0 = SatVar0;
00510   while (Z0 != NULL) {
00511     Z = Z0 -> danach;
00512     free(Z0);
00513     Z0 = Z;
00514   }
00515   SatVar0 = NULL;
00516 
00517   free(Zweiglast); Zweiglast = NULL;
00518   free(beobachtet); beobachtet = NULL;
00519 }
00520 
00521 
00522 /* ------------------------------------------------------------- */
00523 
00524 #ifdef OUTPUTTREEDATAXML
00525 
00526 static char* NameTreeDataFile = NULL;
00527 static FILE* TreeDataFile = NULL;
00528 
00529 void BeginTreeElement() {
00530   fprintf(TreeDataFile, "<t l=\"%ld\">", V1KlRed - SatVar -> number_2_reductions_at_new_node);
00531 }
00532 void EndTreeElement() {
00533   fprintf(TreeDataFile, "</t>\n");
00534 }
00535 void FinaliseSATPath() {
00536   do {
00537     EndTreeElement();
00538     SatVar = SatVar -> davor;
00539   } while (SatVar != NULL);
00540 }
00541 
00542 #endif
00543 
00554 static enum Ergebniswerte SATEntscheidung() {
00555   VZ optZweig;
00556 
00557 #ifdef ALLSAT
00558   assert(! Belegung);
00559   mpz_init(number_satisfying_assignments);
00560 #endif
00561 
00562 Anfang:
00563 
00564   ++Knoten;
00565 
00566 #ifdef OUTPUTTREEDATAXML
00567   SatVar -> number_2_reductions_at_new_node = V1KlRed;
00568 #endif  
00569 
00570   /* Reduktionen, die von Autarkien nicht affiziert werden */
00571   /* (zumindest verallgemeinerte 1-Klauseln-Elimination) */
00572 
00573 alleReduktionen:
00574 
00575   switch ( Reduktion1() ) {
00576 
00577   case 1:
00578 #ifdef OUTPUTTREEDATAXML
00579     BeginTreeElement();
00580     FinaliseSATPath();
00581 #endif  
00582     return SAT;
00583 
00584   case 2:
00585     assert(proportion_searched >= 0);
00586     assert(Vergleich(proportion_searched+proportion_single,1) != groesser);
00587     proportion_searched += exp2l(- (int) Rekursionstiefe);
00588 #ifdef OUTPUTTREEDATAXML
00589     BeginTreeElement();
00590 #endif
00591     {const enum Spruenge r = SatVar -> Ruecksprung;
00592      SatVar = SatVar -> davor;
00593      if (SatVar == NULL) {
00594 #ifdef OUTPUTTREEDATAXML
00595        EndTreeElement();
00596 #endif
00597        return UNSAT;
00598      }
00599      assert(Rekursionstiefe >= 1);
00600      --Rekursionstiefe;
00601      switch (r) {
00602      case SAT1 : goto nachSAT1;
00603      case SAT2 : goto nachSAT2;
00604      }
00605     }
00606   }
00607 
00608  Schleife:
00609 
00610 #ifdef DYNAMISCH
00611   InitAbstand2();
00612 #endif
00613 
00614 /* Zwar werden so die Autarkien nicht in die dynamische Gewichtsberechnung 
00615    einbezogen, dieser Effekt scheint mir jedoch gering, waehrend ihr Einbezug
00616    grossen Aufwand mit sich braechte. So wird also nur Reduktion1() 
00617    beruecksichtigt.
00618 */
00619 
00620   /* Reduktionen, die von Autarkien affiziert werden */
00621   /* (zumindest pure Literale): */
00622 
00623   switch ( Reduktion2() ) {
00624     
00625   case 1:
00626 #ifdef OUTPUTTREEDATAXML
00627     BeginTreeElement();
00628     FinaliseSATPath();
00629 #endif
00630     return SAT;
00631 
00632   case 2:
00633     assert(proportion_searched >= 0);
00634     assert(Vergleich(proportion_searched+proportion_single,1) != groesser);
00635     proportion_searched += exp2l(- (int) Rekursionstiefe);
00636 #ifdef OUTPUTTREEDATAXML
00637     BeginTreeElement();
00638 #endif
00639     {const enum Spruenge r = SatVar -> Ruecksprung;
00640      SatVar = SatVar -> davor;
00641      if (SatVar == NULL) {
00642 #ifdef OUTPUTTREEDATAXML
00643        EndTreeElement();
00644 #endif
00645        return UNSAT;
00646      }
00647      --Rekursionstiefe;
00648      switch (r) {
00649      case SAT1 : goto nachSAT1;
00650      case SAT2 : goto nachSAT2;
00651      }
00652     }
00653   }
00654 
00655   {
00656     float opta = 0;
00657     unsigned int optaS = 0;
00658 /*  Schleife ueber alle Variablen, die jeweils dem Filter vorgelegt werden:
00659     Findet dieser eine Entscheidung oder eine Einer-Verzweigung, so wird eine 
00660     solche Variable ausgesucht, und die Schleife abgebrochen.
00661     Andernfalls wird mittels "Abstand" die (Zweier-)Verzweigung bewertet, und
00662     sie ersetzt, falls besser, die alte, bisher beste Verzweigung.
00663     (Die Zweigauswahl wird von "Abstand" mitberechnet.) 
00664 */
00665     for (VAR v = ersteVar(); echteVar(v); v = naechsteVar(v)) {
00666       Filter(v);
00667       if (erfuellt) {
00668         if (Belegung) { /* Durchfuehrung der Belegung (zur Ausgabe) */
00669           const unsigned int DN = DeltaN[Zweig][Schalter];
00670           for (struct {unsigned int i; StapeleintragFZ Z;} l = {0,Huelle[Zweig][Schalter]}; l.i < DN; ++l.i, ++l.Z) {
00671 #ifndef BAUMRES
00672             belege(*l.Z);
00673 #else
00674             belege(l.Z -> l);
00675 #endif
00676           }
00677         }
00678 #ifdef OUTPUTTREEDATAXML
00679         BeginTreeElement();
00680         FinaliseSATPath();
00681 #endif  
00682         return SAT;
00683       }
00684       
00685       if (reduziert) goto alleReduktionen;
00686       
00687       if (Wahl) {
00688         if (Single) {  /* (zur Zeit) der (nicht-erfuellende) Autarkiefall */
00689           /* Durchfuehrung der Belegung: */
00690           const unsigned int DN = DeltaN[Zweig][Schalter];
00691 #ifdef LOKALLERNEN
00692           eintragenTiefe();
00693 #endif
00694           for (struct {unsigned int i; StapeleintragFZ Z;} l = {0,Huelle[Zweig][Schalter]}; l.i < DN; ++l.i, ++l.Z) {
00695 #ifndef BAUMRES
00696             belege(*l.Z);
00697 #else
00698             belege(l.Z -> l);
00699 #endif
00700           }
00701           /* Falls BAUMRES gesetzt ist: */
00702           /* Da der Standard-Filter nur Autarkien hier liefern kann, */
00703           /* die nie zur Erzeugung der leeren Klausel beitragen koennen, */
00704           /* muss hier in relVar nichts eingetragen werden. */
00705           aktP = LaP[Zweig][Schalter];
00706           aktN -= DeltaN[Zweig][Schalter];
00707           memcpy((void*)(aktAnzK + 2), (void*)(LaAnzK[Zweig][Schalter] + 2), (aktP - 1) * sizeof(unsigned int));
00708           goto Schleife;
00709         }
00710         else {
00711           ++QuasiSingleKnoten;
00712           Schalter = ! Schalter;
00713           optZweig = Zweig;
00714           break;
00715         }
00716       }
00717       {
00718         Abstand();
00719         const float a = (randomisiert) ? Verschmierung(Projektion()) : Projektion();
00720         switch (Vergleich(a, opta)) {
00721         case gleich :
00722           if (Projektion2() <= optaS) break;
00723         case groesser :
00724           opta = a; optaS = Projektion2();
00725           Schalter = ! Schalter;
00726           optZweig = Zweig;
00727           break;
00728         case kleiner :
00729           break;
00730         }
00731       }
00732     }
00733   }
00734   
00735   /* Now the branching variable has been determined. */
00736 
00737   // handling of splitting-only:
00738   if (splitting_only &&
00739       ((! splitting_n && Rekursionstiefe == Beobachtungsniveau) ||
00740        (splitting_n && N - aktN >= Beobachtungsniveau))) {
00741     ++splitting_cases;
00742     output_decision_levels(fpsplitdec);
00743     if (splitting_file) AusgabeBelegung(fpsplit);
00744     else {
00745       assert(splitting_cases <= 1073741824U);
00746       char buf[10+1];
00747       snprintf(buf,10+1,"%u",splitting_cases);
00748       char* const name_sc = (char*) xmalloc(strlen(splitting_store)+1+strlen(buf)+1);
00749       strcpy(name_sc,splitting_store); strcat(name_sc,"/"), strcat(name_sc,buf);
00750       FILE* const file_sc = fopen(name_sc, "w");
00751       if (file_sc == NULL) { fprintf(stderr, "%s\n", Meldung(59)); exit(1); }
00752       AusgabeBelegung(file_sc);
00753       fclose(file_sc);
00754     }
00755     const enum Spruenge r = SatVar -> Ruecksprung;
00756     SatVar = SatVar -> davor;
00757     if (SatVar == NULL) {
00758       assert(Rekursionstiefe == 0);
00759 #ifdef OUTPUTTREEDATAXML
00760       EndTreeElement();
00761 #endif
00762       assert(splitting_cases > 0);
00763       return Unbestimmt;
00764     }
00765     assert(Rekursionstiefe >= 1);
00766     --Rekursionstiefe;
00767 #ifdef BAUMRES
00768     printf("NOT IMPLEMENTED: combination of -S with BAUMRES!\n");
00769     exit(1);
00770 #endif
00771 #ifdef LOKALLERNEN
00772     printf("NOT IMPLEMENTED: combination of -S with LOKALLERNEN!\n");
00773     exit(1);
00774 #endif
00775     switch (r) {
00776     case SAT1 : goto nachSAT1;
00777     case SAT2 : goto nachSAT2;
00778     }
00779   }
00780   assert(! splitting_only || Rekursionstiefe < Beobachtungsniveau);
00781 
00782   /* Now branching. */
00783 
00784 #ifdef OUTPUTTREEDATAXML
00785   BeginTreeElement();
00786 #endif
00787 #ifndef LOKALLERNEN
00788   SatVar -> altTiefe = Tiefe;
00789 #else
00790   SatVar -> Marke = Markierung();
00791 #endif
00792 
00793   /* First optZweig: */
00794 
00795   const unsigned int DN = DeltaN[optZweig][! Schalter];
00796   const unsigned int DN2 = DeltaN[! optZweig][! Schalter];
00797 #ifdef LOKALLERNEN
00798   eintragenTiefe();
00799 #endif
00800 #ifndef BAUMRES
00801   for (struct {unsigned int i; StapeleintragFZ Z;} l = {0,Huelle[optZweig][! Schalter]}; l.i < DN; ++l.i, ++l.Z)
00802     belege(*l.Z);
00803 #else
00804   {
00805    StapeleintragFZ Z = Huelle[optZweig][! Schalter];
00806    belege((Z++) -> l);
00807    for (unsigned int i = 1; i < DN; ++i, ++Z) belege_VK(Z -> l, Z -> k);
00808   }
00809 #endif
00810   aktP = LaP[optZweig][! Schalter];
00811   SatVar -> P2 = LaP[! optZweig][! Schalter];
00812   memcpy((void*)(aktAnzK + 2), (void*)(LaAnzK[optZweig][! Schalter] + 2), (aktP - 1) * sizeof(unsigned int));
00813   memcpy((void*)((SatVar -> AnzK2) + 2), (void*)(LaAnzK[! optZweig][! Schalter] + 2), ((SatVar -> P2) - 1) * sizeof(unsigned int));
00814   SatVar -> N2 = aktN - DN2;
00815   aktN -= DN;
00816   SatVar -> altZeiger2 = Zeiger2;
00817 
00818 /* Ist noch genug Speicher fuer die zweite Belegung?!: */
00819 
00820   if (Zeiger2 + DN2 >= Groesse2) {
00821     ++Ueberschreitung2;
00822     Groesse2 += N;
00823     zweiteBel = (StapeleintragFZ) xrealloc(zweiteBel, Groesse2 * sizeof(StapeleintragF));
00824   }
00825   memcpy((void*)(zweiteBel + Zeiger2), (void*)(Huelle[! optZweig][! Schalter]), DN2 * sizeof(StapeleintragF));
00826   Zeiger2 += DN2;
00827   
00828   if (SatVar -> danach == NULL) {
00829     struct Sammlung* Z;
00830     ++Suchbaumtiefe;
00831     SatVar -> danach = (Z = neuerKnoten());
00832     Z -> davor = SatVar;
00833     SatVar = Z;
00834   }
00835   else
00836     SatVar = SatVar -> danach;
00837   SatVar -> Ruecksprung = SAT1;
00838   ++Rekursionstiefe;
00839   if (Monitor)
00840     if (Rekursionstiefe < Beobachtungsniveau) {
00841       beobachtet[Rekursionstiefe] = beobachtet[Rekursionstiefe-1];
00842       if (Dateiausgabe) {
00843         assert(Rekursionstiefe >= 1);
00844 #ifndef BAUMRES
00845     Verzweigungsliteralausgabe(*Huelle[optZweig][! Schalter], Rekursionstiefe - 1);
00846 #else
00847         Verzweigungsliteralausgabe(Huelle[optZweig][! Schalter] -> l, Rekursionstiefe - 1);
00848 #endif
00849       }
00850     }
00851   goto Anfang; // Branching (recursion simulated)
00852 
00853   nachSAT1 :
00854 
00855 #ifdef OUTPUTTREEDATAXML
00856     EndTreeElement();
00857 #endif
00858 
00859     if (Monitor)
00860       if (Rekursionstiefe < Beobachtungsniveau) {
00861         beobachtet[Rekursionstiefe] += Zweiglast[Rekursionstiefe];
00862         Monitorausgabe(beobachtet[Rekursionstiefe]);
00863       }
00864 
00865   /* rueckgaengig machen: */
00866 
00867 #ifdef LOKALLERNEN
00868   Rueckgaengigmachung(SatVar -> Marke);
00869 #else
00870 # ifndef BAUMRES
00871   do {
00872     --Tiefe;
00873     rebelege(PfadLit());
00874   }
00875   while (Tiefe > SatVar -> altTiefe);
00876 # else
00877   while (--Tiefe > SatVar -> altTiefe)
00878     rebelege(PfadLit());
00879   if (rebelege_Verz(PfadLit()))
00880     aktV_eintragen_relV();
00881   else {
00882     Zeiger2 = SatVar -> altZeiger2;
00883     ++SingleKnoten;
00884     assert(proportion_single >= 0);
00885     assert(Vergleich(proportion_searched+proportion_single,1) != groesser);
00886     proportion_single += exp2l(- (int) (Rekursionstiefe) - 1);
00887     {const enum Spruenge r = SatVar -> Ruecksprung;
00888      SatVar = SatVar -> davor;
00889      if (SatVar == NULL) {
00890 #  ifdef OUTPUTTREEDATAXML
00891        EndTreeElement();
00892 #  endif
00893        return UNSAT;
00894      }
00895      assert(Rekursionstiefe >= 1);
00896      --Rekursionstiefe;
00897      switch (r) {
00898      case SAT1 : goto nachSAT1;
00899      case SAT2 : goto nachSAT2;
00900      }
00901     }
00902   }
00903 # endif
00904 #endif
00905 
00906   /* nun der zweite Zweig: */
00907 
00908 #ifdef LOKALLERNEN
00909   eintragenTiefe();
00910 #endif
00911 #ifndef BAUMRES
00912   for (struct {unsigned i; StapeleintragFZ Z;} l = {SatVar->altZeiger2, zweiteBel + (SatVar -> altZeiger2)}; l.i < Zeiger2; ++l.i, ++l.Z)
00913     belege(*l.Z);
00914 #else
00915   {
00916    StapeleintragFZ Z = zweiteBel + (SatVar -> altZeiger2);
00917    belege((Z++) -> l);
00918    for (unsigned int i = SatVar -> altZeiger2 + 1; i < Zeiger2; ++i, ++Z)
00919     belege_VK(Z -> l, Z -> k);
00920   }
00921 #endif
00922 
00923   Zeiger2 = SatVar -> altZeiger2;
00924   aktP = SatVar -> P2;
00925   aktN = SatVar -> N2;
00926   memcpy((void*)(aktAnzK + 2), (void*)((SatVar -> AnzK2) + 2), (aktP - 1) * sizeof(unsigned int));
00927 
00928   if (SatVar -> danach == NULL) {
00929     struct Sammlung* Z;
00930     ++Suchbaumtiefe;
00931     SatVar -> danach = (Z = neuerKnoten());
00932     Z -> davor = SatVar;
00933     SatVar = Z;
00934   }
00935   else
00936     SatVar = SatVar -> danach;
00937   SatVar -> Ruecksprung = SAT2;
00938   ++Rekursionstiefe;
00939   if (Monitor)
00940     if (Rekursionstiefe < Beobachtungsniveau)
00941       beobachtet[Rekursionstiefe] = beobachtet[Rekursionstiefe-1];
00942   goto Anfang;
00943 
00944   nachSAT2 :
00945 
00946 #ifdef OUTPUTTREEDATAXML
00947     EndTreeElement();
00948 #endif
00949 
00950     if (Monitor)
00951       if (Rekursionstiefe < Beobachtungsniveau) {
00952         beobachtet[Rekursionstiefe] += Zweiglast[Rekursionstiefe];
00953         Monitorausgabe(beobachtet[Rekursionstiefe]);
00954       }
00955 
00956 #ifdef LOKALLERNEN
00957   Rueckgaengigmachung(SatVar -> Marke);
00958 #else
00959 # ifndef BAUMRES
00960   do { --Tiefe; rebelege(PfadLit()); }
00961   while (Tiefe > SatVar -> altTiefe);
00962 # else
00963   while (--Tiefe > SatVar -> altTiefe) rebelege(PfadLit());
00964   if (rebelege_Verz(PfadLit())) relVMhinzufuegen();
00965   else ++VerSingleKnoten;
00966 # endif
00967 #endif
00968   {const enum Spruenge r = SatVar -> Ruecksprung;
00969    SatVar = SatVar -> davor;
00970    if (SatVar == NULL) {
00971 #ifdef OUTPUTTREEDATAXML
00972      EndTreeElement();
00973 #endif
00974      return UNSAT;
00975    }
00976    assert(Rekursionstiefe >= 1);
00977    --Rekursionstiefe;
00978    switch (r) {
00979    case SAT1 : goto nachSAT1;
00980    case SAT2 : goto nachSAT2;
00981    default :
00982      assert(0);
00983    }
00984   }
00985 }
00986 
00987 /* ------------------------------------------------------------- */
00988 
00995 void Statistikzeile(FILE* const fp) {
00996   if (Format == Dimacs_Format) {
00997     fprintf(fp, "s ");
00998     switch (s) {
00999     case SAT :
01000       fprintf(fp, "SATISFIABLE"); break;
01001     case UNSAT :
01002       fprintf(fp, "UNSATISFIABLE"); break;
01003     case Unbestimmt :
01004       fprintf(fp, "UNKNOWN"); break;
01005     }
01006     fprintf(fp, "\n");
01007     fprintf(fp,
01008             "c sat_status                            %d\n"
01009             "c initial_maximal_clause_length         %u\n"
01010             "c initial_number_of_variables           %u\n"
01011             "c initial_number_of_clauses             %u\n"
01012             "c initial_number_of_literal_occurrences %u\n"
01013             "c number_of_initial_unit-eliminations   %lu\n"
01014             "c reddiff_maximal_clause_length         %u\n"
01015             "c reddiff_number_of_variables           %u\n"
01016             "c reddiff_number_of_clauses             %u\n"
01017             "c reddiff_number_of_literal_occurrences %u\n"
01018             "c number_of_2-clauses_after_reduction   %u\n"
01019             "c running_time(sec)                     %1.1f\n"
01020             "c number_of_nodes                       %lu\n"
01021             "c number_of_single_nodes                %lu\n"
01022             "c number_of_quasi_single_nodes          %lu\n"
01023             "c number_of_2-reductions                %lu\n"
01024             "c number_of_pure_literals               %lu\n"
01025             "c number_of_autarkies                   %lu\n"
01026             "c number_of_missed_single_nodes         %lu\n"
01027             "c max_tree_depth                        %u\n"
01028             "c proportion_searched                   %1.6e\n"
01029             "c proportion_single                     %1.6e\n"
01030             "c total_proportion                      %1.16g\n"
01031             "c number_of_table_enlargements          %u\n"
01032             "c number_of_1-autarkies                 %lu\n"
01033             "c number_of_new_2-clauses               %lu\n"
01034             "c maximal_number_of_added_2-clauses     %lu\n"
01035             "c file_name                             %s\n",
01036       s, P0, N0, K0, L0,
01037             InitEinerRed, P0 - P, N0 - N, K0 - K, L0 - L, init2Klauseln,
01038             (double) Verbrauch / EPS,
01039       Knoten, SingleKnoten, QuasiSingleKnoten, V1KlRed, PureL,
01040       Autarkien, VerSingleKnoten, Suchbaumtiefe,
01041           (double) proportion_searched, (double) proportion_single, (double)(proportion_searched+proportion_single),
01042       Ueberschreitung2, 
01043       FastAutarkien, neue2Klauseln, maxneue2K,
01044       aktName);
01045           if (splitting_only)
01046             fprintf(fp,
01047             "c splitting_directory                   %s\n"
01048             "c splitting_cases                       %u\n",
01049             splitting_store, splitting_cases);
01050   }
01051   else {
01052     fprintf(fp, "<SAT-solver.output timestamp = \"%ld\" >\n", time(0));
01053     
01054     fprintf(fp, "  <result value = \"");
01055     switch (s) {
01056     case SAT : fprintf(fp, "satisfiable"); break;
01057     case UNSAT : fprintf(fp, "unsatisfiable"); break;
01058     case Unbestimmt : fprintf(fp, "unknown"); break;
01059     }
01060     fprintf(fp, "\" />\n");
01061 
01062     fprintf(fp, "  <processing-description>\n");
01063     fprintf(fp, "    <basic>\n");
01064     fprintf(fp, "      <running-time type = \"core\" sec = \"%.2f\" />\n", (double) Verbrauch / EPS);
01065     fprintf(fp, "      <tree-depth type = \"maximal\" count = \"%d\" />\n", Suchbaumtiefe);
01066     fprintf(fp, "      <autarky-reductions where = \"search-tree\" level = \"pure\" count = \"%ld\" />\n", PureL);
01067     fprintf(fp, "      <autarky-reductions where = \"search-tree\" level = \"non-pure\" count = \"%ld\" />\n", Autarkien);
01068     fprintf(fp, "      <number_of_table_enlargements count = \"%d\" />\n", Ueberschreitung2);
01069     fprintf(fp, "      <nodes type = \"node\" count = \"%ld\" />\n", Knoten);
01070     fprintf(fp, "      <nodes type = \"single\" count = \"%ld\" />\n", SingleKnoten);
01071     fprintf(fp, "      <nodes type = \"quasi-single\" count = \"%ld\" />\n", QuasiSingleKnoten);
01072     fprintf(fp, "      <nodes type = \"missed_single\" count = \"%ld\" />\n", VerSingleKnoten);
01073     fprintf(fp, "      <nodes type = \"splitting_cases\" count = \"%u\" />\n", splitting_cases);
01074 
01075     fprintf(fp, "    </basic>\n");
01076     fprintf(fp, "    <extended>\n");
01077     fprintf(fp, "      <generalised_unit_reductions where = \"initial\" level = \"1\" count = \"%ld\" />\n", InitEinerRed);
01078     fprintf(fp, "      <generalised_unit_reductions where = \"search-tree\" level = \"2\" count = \"%ld\" />\n", V1KlRed);
01079     fprintf(fp, "      <generalised_autarky-reductions where = \"search-tree\" level = \"1\" specifier = \"total\" count = \"%ld\" />\n", FastAutarkien);
01080     fprintf(fp, "      <numbers_of_new_clauses list_of_clause-lengths = \"complete\" type = \"local\" specifier = \"maximum\" >\n");
01081     fprintf(fp, "        <nc_number length = \"2\" count = \"%ld\" />\n", maxneue2K);
01082     fprintf(fp, "      </numbers_of_new_clauses>\n");
01083     fprintf(fp, "      <numbers_of_new_clauses list_of_clause-lengths = \"complete\" type = \"local\" specifier = \"total\" >\n");
01084     fprintf(fp, "        <nc_number length = \"2\" count = \"%ld\" />\n", neue2Klauseln);
01085     fprintf(fp, "      </numbers_of_new_clauses>\n");
01086     fprintf(fp, "    </extended>\n");
01087     fprintf(fp, "  </processing-description>\n");
01088 
01089     if (! splitting_only)
01090     fprintf(fp, "  <instance_specs system-name = \"%s\" >\n", aktName);
01091     else
01092     fprintf(fp, "  <instance_specs system-name = \"%s\" splitting-dir = \"%s\" >\n", aktName, splitting_store);
01093 
01094     fprintf(fp, "    <measures>\n");
01095     fprintf(fp, "      <reduction> <none/> </reduction>\n");
01096     fprintf(fp, "      <number_of_variables specifier = \"exact\" count = \"%d\" />\n", N0);
01097     fprintf(fp, "      <clause-length specifier = \"exact\" type = \"maximal\" value = \"%d\" />\n", P0);
01098     fprintf(fp, "      <total_number_of_clauses specifier = \"exact\" count = \"%d\" />\n", K0);
01099     fprintf(fp, "      <number_of_literal_occurrences specifier = \"exact\" count = \"%d\" />\n", L0);
01100     fprintf(fp, "    </measures>\n");
01101 
01102     fprintf(fp, "    <measures>\n");
01103     fprintf(fp, "      <reduction> <tautological_clauses/> <multiple_literal_occurences_in_clauses/> <unit_clause_elimination/> </reduction>\n");
01104 
01105     if (Knoten == 0) { // nur Vorreduktion
01106       if (s == UNSAT) { // Vorreduktion erzeugte die leere Klausel
01107   fprintf(fp, "      <numbers_of_clauses list_of_clause-lengths = \"incomplete\" >\n");
01108   fprintf(fp, "        <number length = \"0\" specifier = \"lower_bound\" count = \"1\" />\n");
01109   fprintf(fp, "      </numbers_of_clauses>\n");
01110       }
01111       else if (s == SAT) { // Vorreduktion erfuellte die Klauselmenge
01112   fprintf(fp, "      <total_number_of_clauses specifier = \"exact\" count = \"0\" />\n");
01113       }
01114       else { // keine Entscheidung
01115   fprintf(fp, "      <number_of_variables specifier = \"exact\" count = \"%d\" />\n", N);
01116   fprintf(fp, "      <clause-length type = \"maximal\" specifier = \"exact\" count = \"%d\" />\n", P);
01117   fprintf(fp, "      <total_number_of_clauses specifier = \"exact\" count = \"%d\" />\n", K);
01118   fprintf(fp, "      <number_of_literal_occurrences specifier = \"exact\"count = \"%d\" />\n", L);
01119       }
01120     }
01121     else { // nun wurde der Suchbaum aufgebaut
01122       fprintf(fp, "      <number_of_variables specifier = \"exact\" count = \"%d\" />\n", N);
01123       fprintf(fp, "      <clause-length type = \"maximal\" specifier = \"exact\" value = \"%d\" />\n", P);
01124       fprintf(fp, "      <total_number_of_clauses specifier = \"exact\" count = \"%d\" />\n", K);
01125       fprintf(fp, "      <numbers_of_clauses list_of_clause-lengths = \"complete\" >\n");
01126       for (unsigned int i = 0; i <= P - 2; ++i)
01127   if (InitAnzK[i+2] != 0)
01128     fprintf(fp, "        <number length = \"%d\" count = \"%d\" />\n", i+2, InitAnzK[i+2]);
01129       fprintf(fp, "      </numbers_of_clauses>\n");
01130       fprintf(fp, "      <number_of_literal_occurrences specifier = \"exact\" count = \"%d\" />\n", L);
01131     }
01132     fprintf(fp, "    </measures>\n");
01133 
01134     fprintf(fp, "  </instance_specs>\n");
01135 
01136    if (! Belegung || s != SAT || Dateiausgabe)
01137       fprintf(fp, "</SAT-solver.output>\n");
01138   }
01139   return;
01140 }
01141 
01142 const char* BasisName(const char* const name) {
01143   const char* const basis = strrchr(aktName, '/');
01144   if (basis == NULL) return name;
01145   else return basis + 1;
01146 }
01147 
01148 
01149 /* ------------------------------------------------------------- */
01150 
01151 static FILE* fpaus = NULL; /* fuer die Ausgabe der Ergebnisse */
01152 
01153 static void Zustandsanzeige (const int sig) {
01154 #ifndef SYSTIME
01155   Verbrauch = clock() - akkVerbrauch;
01156 #else
01157   times(Zeiger);
01158   Verbrauch = SysZeit.tms_utime - akkVerbrauch;
01159 #endif
01160   Statistikzeile(stdout);
01161   if (Dateiausgabe) Statistikzeile(fpaus);
01162   fflush(NULL);
01163   signal(SIGUSR1, Zustandsanzeige);
01164 }
01165 
01166 jmp_buf Ausgabepunkt;
01167 
01168 static void Abbruch (const int sig) {
01169   signal(SIGINT, Abbruch);
01170   signal(SIGALRM, Abbruch);
01171   if (splitting_only) splitting_abortion = true;
01172   longjmp(Ausgabepunkt, 1);
01173 }
01174 
01175 static FILE* fp = NULL; /* die aktuelle Eingabedatei */
01176 static unsigned int Groesse;
01177 static FILE* fppa = NULL; /* fuer die Ausgabe einer erfuellenden Belegung */
01178 
01179 static unsigned int Argument;
01180 
01181 static char* NameBel = NULL; char* NameMon = NULL;
01182 
01183 
01184 int main(const int argc, const char* const argv[]) {
01185   const char* const Ausgabedatei = "OKs" VERSIONSNUMMER1 "_" VERSIONSNUMMER2 "_" OPTIONENKENNUNG5 OPTIONENKENNUNG6 OPTIONENKENNUNG7 OPTIONENKENNUNG1 OPTIONENKENNUNG2 OPTIONENKENNUNG3 OPTIONENKENNUNG4".res";
01186   const char* const Version = VERSIONSNUMMER1 "." VERSIONSNUMMER2;
01187 
01188 #ifdef SYSTIME
01189   EPS = sysconf(_SC_CLK_TCK);
01190 #endif
01191 
01192   signal(SIGUSR1, Zustandsanzeige);
01193   signal(SIGINT, Abbruch);
01194   signal(SIGALRM, Abbruch);
01195   if (setjmp(Ausgabepunkt)) goto Ausgabe;
01196 
01197   if (Konstantenfehler()) {
01198     fprintf(stderr, "%s\n", Meldung(0));
01199     return 1;
01200   }
01201 
01202   if (argc == 1) {
01203     fprintf(stderr, "%s\n", Meldung(3));
01204     return 0;
01205   }
01206 
01207   setzenStandard();
01208 
01209   for (Argument = 1; Argument < argc; ++Argument) {
01210     if (strcmp("--version", argv[Argument]) == 0) {
01211       printf("%s %s; %s %s\n%s: %s, %s\n", Meldung(24), DATUM, Meldung(2), Version, Meldung(6), __DATE__, __TIME__);
01212       printf("%s", Meldung(44));
01213 #ifdef NBAUMRES
01214       printf(" NBAUMRES");
01215 #endif
01216 #ifdef LITTAB
01217       printf(" LITTAB");
01218 #endif
01219 #ifdef SYSTIME
01220       printf(" SYSTIME");
01221 #endif
01222 #ifdef DYNAMISCH
01223       printf(" DYNAMISCH");
01224 #endif
01225 #ifdef DYNAMISCH
01226       printf(" FAKTOR=%.2f", FAKTOR);
01227 #endif
01228 #ifdef LOKALLERNEN
01229       printf(" LOKALLERNEN");
01230 #endif
01231 #ifdef NL2RED
01232       printf(" NL2RED");
01233 #endif
01234 #ifdef FASTAUTARKIE
01235       printf(" FASTAUTARKIE");
01236 #endif
01237 #ifdef KEININLINE
01238       printf(" KEININLINE");
01239 #endif
01240 #ifdef OUTPUTTREEDATAXML
01241       printf(" OUTPUTTREEDATAXML");
01242 #endif
01243       printf(" STANDARD=%1d", STANDARD);
01244 
01245       printf("\n");
01246       printf("%s %s\n", Meldung(45), Abstandsname);
01247       printf("%s %s\n", Meldung(46), Projektionsname);
01248     }
01249     else if (strcmp("--author", argv[Argument]) == 0)
01250       printf("%s\n", Meldung(25));
01251     else if (strcmp("--help", argv[Argument]) == 0)
01252       printf("%s\n", Meldung(26));
01253     else if (strcmp("-O", argv[Argument]) == 0)
01254       Belegung = ! Belegung;
01255     else if (strcmp("-F", argv[Argument]) == 0)
01256       Dateiausgabe = ! Dateiausgabe;
01257     else if (strcmp("-M", argv[Argument]) == 0)
01258       Monitor = ! Monitor;      
01259     else if (strcmp("-P", argv[Argument]) == 0)
01260       nurVorreduktion = ! nurVorreduktion;      
01261     else if (strcmp("-R", argv[Argument]) == 0)
01262       spezRueckgabe = ! spezRueckgabe;
01263     else if (strcmp("-B", argv[Argument]) == 0)
01264       Schranken = ! Schranken;
01265     else if (strcmp("--info", argv[Argument]) == 0)
01266       printf("%s\n%s\n", Meldung(47), Meldung(48));
01267     else if (strcmp("-RA", argv[Argument]) == 0)
01268       randomisiert = ! randomisiert;
01269     else if (strcmp("-SD", argv[Argument]) == 0)
01270       splitting_n = ! splitting_n;
01271     else if (strcmp("-SF", argv[Argument]) == 0)
01272       splitting_file = ! splitting_file;
01273     else if (strcmp("-DO", argv[Argument]) == 0) {
01274       Format = Dimacs_Format;
01275       spezRueckgabe = true;
01276     }
01277     else if (strcmp("-XO", argv[Argument]) == 0) {
01278       Format = XML_Format;
01279       spezRueckgabe = false;
01280     }
01281     else if (strcmp("--specification", argv[Argument]) == 0) {
01282       printf("<SAT-solver.specification>\n");
01283       printf("  <solver-type mode = \"deterministic\">\n");
01284       printf("    <complete/>\n");
01285       printf("  </solver-type>\n");
01286       printf("  <solver-name base-name = \"%s\" version = \"%s\" url = \"%s\" />\n", "OKsolver", Version, "http://cs.swan.ac.uk/~csoliver/OKsolver");
01287       printf("  <solver-author first_name = \"Oliver\" last_name = \"Kullmann\" country = \"United Kingdom\" e-mail = \"O.Kullmann@Swansea.ac.uk\" www = \"http://cs.swan.ac.uk/~csoliver/\" />\n");
01288       printf("  <programming_language name = \"C\" />\n");
01289       printf("  <compilation_time timestamp = \"%s %s\" />\n", __DATE__, __TIME__);
01290       printf("  <url for = \"executable\" value = \"");
01291       if (argv[0][0] == '/') // absoluter Pfadname
01292         printf("%s\" />\n", argv[0]);
01293       else // relativer Pfadname
01294         printf("%s/%s\" />\n", getenv("PWD"), argv[0]);
01295       printf("  <options string = \"%s\" />\n", OPTIONENKENNUNG5 OPTIONENKENNUNG6 OPTIONENKENNUNG7 OPTIONENKENNUNG1 OPTIONENKENNUNG2 OPTIONENKENNUNG3 OPTIONENKENNUNG4);
01296       if (internal) printf("  <internal/>\n");
01297       printf("</SAT-solver.specification>\n");
01298     }
01299     else if (strncmp("--language=", argv[Argument], 11) == 0) {
01300       int Nummer;
01301       if (sscanf(argv[Argument] + 11, "%d", &Nummer) != 1) {
01302         fprintf(stderr, "%s\n", Meldung(18));
01303         return 1;
01304       }
01305       if ((Nummer < 0) || (Nummer >= ANZSPRACHEN)) {
01306         fprintf(stderr, "%s %2d\n", Meldung(19), ANZSPRACHEN - 1);
01307         return 1;
01308       }
01309       Sprache = Nummer;
01310     }
01311     else if (strncmp("--standard=", argv[Argument], 11) == 0) {
01312       int Nummer;
01313       if (sscanf(argv[Argument] + 11, "%d", &Nummer) != 1) {
01314         fprintf(stderr, "%s\n", Meldung(20));
01315         return 1;
01316       }
01317       if ((Nummer <= 0) || (Nummer > ANZSTANDARDS)) {
01318         fprintf(stderr, "%s %2d\n", Meldung(21), ANZSTANDARDS);
01319         return 1;
01320       }
01321       Standard = Nummer;
01322       setzenStandard();
01323     }
01324     else if (strncmp("-D", argv[Argument], 2) == 0) {
01325       // -D fuer Beobachtungsniveau (depth)
01326       // Verzweigungsliterale werden (falls ueberhaupt Dateiausgabe gesetzt ist)
01327       // nur bis zu zwei Stufen unterhalb der Beobachtungsschicht ausgegeben,
01328       // so dass hierfuer als das Beobachtungsniveau mindestens zwei sein
01329       // sollte.
01330       int Nummer;
01331       if (sscanf(argv[Argument] + 2, "%d", &Nummer) != 1) {
01332         fprintf(stderr, "%s\n", Meldung(31));
01333         return 1;
01334       }
01335       if (Nummer < 0) {
01336         fprintf(stderr, "%s\n", Meldung(32));
01337         return 1;
01338       }
01339       Beobachtungsniveau = Nummer;
01340     }
01341     else if (strncmp("-MAXN=", argv[Argument], 6) == 0) {
01342       int maxn;
01343       if (sscanf(argv[Argument] + 6, "%d", &maxn) != 1) {
01344         fprintf(stderr, "%s\n", Meldung(33));
01345         return 1;
01346       }
01347       if (maxn < 0) {
01348         fprintf(stderr, "%s\n", Meldung(34));
01349         return 1;
01350       }
01351       MAXN = maxn;
01352     }
01353     else if (strncmp("-MAXL=", argv[Argument], 6) == 0) {
01354       int maxl;
01355       if (sscanf(argv[Argument] + 6, "%d", &maxl) != 1) {
01356         fprintf(stderr, "%s\n", Meldung(36));
01357         return 1;
01358       }
01359       if (maxl < 0) {
01360         fprintf(stderr, "%s\n", Meldung(37));
01361         return 1;
01362       }
01363       MAXL = maxl;
01364     }
01365     else if (strncmp("-MAXK=", argv[Argument], 6) == 0) {
01366       int maxk;
01367       if (sscanf(argv[Argument] + 6, "%d", &maxk) != 1) {
01368         fprintf(stderr, "%s\n", Meldung(39));
01369         return 1;
01370       }
01371       if (maxk < 0) {
01372         fprintf(stderr, "%s\n", Meldung(40));
01373         return 1;
01374       }
01375       MAXK = maxk;
01376     }
01377     else if (strncmp("--timeout=", argv[Argument], 10) == 0) {
01378       int t;
01379       if (sscanf(argv[Argument] + 10, "%d", &t) != 1) {
01380         fprintf(stderr, "%s\n", Meldung(42));
01381         return 1;
01382       }
01383       if (t < 0) {
01384         fprintf(stderr, "%s\n", Meldung(43));
01385         return 1;
01386       }
01387       Zeitschranke = t;
01388     }
01389     else if (strncmp("-seed=", argv[Argument], 6) == 0) {
01390       long unsigned int S;
01391       if (sscanf(argv[Argument] + 6, "%lud", &S) != 1) {
01392         fprintf(stderr, "%s\n", Meldung(52));
01393         return 1;
01394       }
01395       Schluessel = S;
01396     }
01397     else if (strncmp("-quot=", argv[Argument], 6) == 0) {
01398       double V;
01399       if (sscanf(argv[Argument] + 6, "%lf", &V) != 1)
01400         {
01401           fprintf(stderr, "%s\n", Meldung(53));
01402           return 1;
01403         }
01404       Verhaeltnis = V;
01405     }
01406     else if (strncmp("-S=", argv[Argument], 3) == 0) {
01407       splitting_only = true;
01408       Belegung = true;
01409       splitting_store = argv[Argument]+3;
01410       if (strlen(splitting_store) == 0) {
01411         fprintf(stderr, "%s\n", Meldung(57));
01412         return 1;
01413       }
01414     }
01415     else if (strncmp("-", argv[Argument], 1) == 0) {
01416       fprintf(stderr, "%s %s\n", Meldung(22), argv[Argument]);
01417       return 1;
01418     }
01419     else {
01420       if (splitting_only) {
01421         if (! Belegung) { fprintf(stderr, "%s\n", Meldung(58)); return 1; }
01422         if (splitting_file) {
01423           if ((fpsplit = fopen(splitting_store, "w")) == NULL) {
01424             fprintf(stderr, "%s %s\n", Meldung(60), splitting_store);
01425             return 1;
01426           }
01427         }
01428         splitting_decisions = (char*) xmalloc(strlen(splitting_store)+10+1);
01429         strcpy(splitting_decisions,splitting_store);
01430         if (splitting_file) strcat(splitting_decisions, "_");
01431         else strcat(splitting_decisions, "/");
01432         strcat(splitting_decisions, "decisions");
01433         if ((fpsplitdec = fopen(splitting_decisions, "w")) == NULL) {
01434           fprintf(stderr, "%s %s\n", Meldung(62), splitting_decisions);
01435           return 1;
01436         }
01437       }
01438       aktName = argv[Argument];
01439       s = Unbestimmt;
01440       alarm(Zeitschranke);
01441 #ifndef SYSTIME
01442       akkVerbrauch = clock();
01443 #else
01444       times(Zeiger);
01445       akkVerbrauch = SysZeit.tms_utime;
01446 #endif
01447       if (randomisiert) srand_S();
01448       if ((fp = fopen(aktName, "r")) == NULL) {
01449         fprintf(stderr, "%s %s\n", Meldung(4), aktName);
01450         return 1;
01451       }
01452       {
01453         struct stat stbuf;
01454         if (stat(aktName, &stbuf) == -1) {
01455           fprintf(stderr, Meldung(7), aktName);
01456           return 1;
01457         }
01458         Groesse = stbuf.st_size;
01459       }
01460       
01461       if (Dateiausgabe) {
01462         if ((fpaus = fopen(Ausgabedatei, "a")) == NULL) {
01463           fprintf(stderr, "%s %s\n", Meldung(30), Ausgabedatei);
01464           return 1;
01465         }
01466         if (Belegung || (Monitor && (! nurVorreduktion))) {
01467           Wurzel = BasisName(aktName);
01468           if (Belegung) {
01469             NameBel = (char*) xmalloc((strlen(Wurzel) + 3 + 1) * sizeof(char));
01470             strcpy(NameBel, Wurzel); strcat(NameBel, ".pa");
01471           }
01472           if (Monitor && (! nurVorreduktion)) {
01473             NameMon = (char*) xmalloc((strlen(Wurzel) + 3 + 1) * sizeof(char));
01474             strcpy(NameMon, Wurzel); strcat(NameMon, ".mo");
01475             if ((fpmo = fopen(NameMon, "w")) == NULL) {
01476               fprintf(stderr, "%s %s\n", Meldung(29), NameMon);
01477               return 1;
01478             }
01479           }
01480         }     
01481       }
01482       
01483 #ifdef OUTPUTTREEDATAXML
01484       {
01485         if (! Wurzel) Wurzel = BasisName(aktName);
01486         NameTreeDataFile = (char*) xmalloc((strlen(Wurzel) + 4 + 1));
01487         strcpy(NameTreeDataFile, Wurzel); strcat(NameTreeDataFile, ".xml");
01488         if ((TreeDataFile = fopen(NameTreeDataFile, "w")) == NULL) {
01489           fprintf(stderr, "%s %s\n", Meldung(54), NameTreeDataFile);
01490           return 1;
01491         }
01492         fprintf(TreeDataFile, "<?xml version=\"1.0\" standalone=\"yes\" ?>\n");
01493         fprintf(TreeDataFile, "<!DOCTYPE t [\n");
01494         fprintf(TreeDataFile, "  <!ELEMENT t (t?, t?)>\n");
01495         fprintf(TreeDataFile, "  <!ATTLIST t\n");
01496         fprintf(TreeDataFile, "    l NMTOKEN #REQUIRED>\n");
01497         fprintf(TreeDataFile, "]>\n\n");
01498         // If already in the preprocessing phase the formula is decided, then
01499         // no tree-xml-element is output, and thus the file with name
01500         // NameTreeDataFile does not contain correct xml.
01501       }
01502 #endif
01503       
01504       switch (Einlesen(fp, Groesse)) {
01505       case Sat : s = SAT; break;
01506       case Unsat : s = UNSAT; break;
01507       case Fehler :
01508         fprintf(stdout, "%s %s.\n", Meldung(17), aktName);
01509         if (Dateiausgabe)
01510           fprintf(fpaus, "%s %s.\n", Meldung(17), aktName);
01511         goto Aufraeumen;
01512       case Norm :
01513         if (nurVorreduktion)
01514           break;
01515         InitVarLitKlm();
01516         InitSat();
01517 #ifdef LOKALLERNEN
01518         InitlokalesLernen();
01519 #endif
01520         if (Monitor) {
01521           printf("\n%s\n %s, %4d, %10d\n", Meldung(28), aktName, Beobachtungsniveau, Gesamtlast);
01522           printf("%s\n\n", Meldung(55));
01523           if (Dateiausgabe) {
01524             fprintf(fpmo, "# %s %4d %11d\n", aktName, Beobachtungsniveau, Gesamtlast);
01525             fprintf(fpmo, "%s\n", Meldung(56));
01526           }
01527         }
01528         
01529         s = SATEntscheidung();
01530         if (splitting_only && splitting_cases != 0) s = Unbestimmt;
01531       }
01532       
01533     Ausgabe :
01534 
01535       if (splitting_abortion) fprintf(stderr, "\n%s\n", Meldung(61));
01536 #ifndef SYSTIME
01537       Verbrauch = clock() - akkVerbrauch;
01538 #else
01539       times(Zeiger);
01540       Verbrauch = SysZeit.tms_utime - akkVerbrauch;
01541 #endif
01542       if (Monitor) printf("\n");
01543       Statistikzeile(stdout);
01544       if (Dateiausgabe) Statistikzeile(fpaus);
01545       
01546       /* Achtung: Die Analyse der Ausgabe verlangt, dass das allererste */
01547       /* Zeichen die SAT-Zugehoerigkeit (d.h.: 0 oder 1) angibt. */
01548       
01549       if (Belegung && (s == SAT))
01550         if (! Dateiausgabe) AusgabeBelegung(stdout);
01551         else {
01552           if ((fppa = fopen(NameBel, "w")) == NULL) {
01553             fprintf(stderr, "%s %s\n", Meldung(27), NameBel);
01554             return 1;
01555           }
01556           AusgabeBelegung(fppa);
01557         }
01558     Aufraeumen :
01559       
01560       alarm(0);
01561       AufraeumenSat();
01562 #ifdef BAUMRES
01563       AufraeumenBaumRes();
01564 #endif
01565 #ifdef LOKALLERNEN
01566       AufraeumenlokalesLernen();
01567 #endif
01568       AufraeumenEinlesen(); /* zuletzt */
01569       free(NameBel); NameBel = NULL;
01570       free(NameMon); NameMon = NULL;
01571 #ifdef OUTPUTTREEDATAXML
01572       fprintf(TreeDataFile, "\n");
01573       free(NameTreeDataFile); NameTreeDataFile = NULL;
01574       if (TreeDataFile != NULL) {
01575         fclose(TreeDataFile); TreeDataFile = NULL;
01576       }
01577 #endif
01578       if (fp != NULL) { fclose(fp); fp = NULL; }
01579       if (fpmo != NULL) { fclose(fpmo); fpmo = NULL; }
01580       if (fpaus != NULL) { fclose(fpaus); fpaus = NULL; }
01581       if (fppa != NULL) { fclose(fppa); fppa = NULL; }
01582     }
01583   }
01584 
01585   if (splitting_abortion) return 1;
01586   if (spezRueckgabe)
01587     switch (s) {
01588     case SAT : return 10;
01589     case UNSAT : return 20;
01590     case Unbestimmt : return 0;
01591     }
01592   else return 0;
01593 }