DE19903633A1 - Implementierung von Boolescher Erfüllbarkeit mit nichtchronologischer Rückwärtsverarbeitung in rekonfigurierbarer Hardware - Google Patents

Abstract

Eine Boolesche SAT-Lösungsvorrichtung verwendet rekonfigurierbare Hardware, um ein spezifisches Eingabeproblem zu lösen. Jede der mehreren geordneten Variablen weist eine entsprechende von mehreren Zustandsmaschinen auf. Jede Zustandsmaschine weist eine Implikationsschaltung für ihre jeweilige Variable auf und arbeitet parallel entsprechend einer identischen Zustandsmaschine. Eine Zustandsmaschine implementiert das Davids-Putnam-Verfahren in Hardware und stellt eine verbesserte Leistung gegenüber Software infolge der parallelen Prüfung von direkten und transitiven Implikationen bereit. Eine andere Zustandsmaschine implementiert ein neuartiges nichtchronologisches Rückwärtsverarbeitungsverfahren, das die parallele Implikationsprüfung ausnutzt und das Bedürfnis vermeidet, im Fall von Rückwärtsverarbeitung einen GRASP-Implikationsgraphen aufrechtzuerhalten oder durchzugehen. Die neuartige nichtchronologische Rückwärtsverarbeitung sorgt dafür, daß eine Sperrvariable als eine Blattvariable gesetzt wird und daß nur der Wert der Blattvariablen geändert wird, jedoch möglicherweise sowohl der Wert als auch die Identität einer Rückwärtsverarbeitungsvariablen geändert werden.

Description

Diese Erfindung betrifft die Beschleunigung einer automa­ tischen Testmustererzeugung (ATPG) und logischen Synthese/Veri­ fikation durch Beschleunigung des Booleschen Erfüllbarkeits- (SAT-) Problems. Insbesondere sorgt die Erfindung für ein kon­ figurierbares Berechnungsverfahren zum SAT-Lösen, das wesent­ liche Beschleunigungen (< 200× in vielen Fällen) gegenüber her­ kömmlichen Softwareverfahren bieten kann. Da Boolesche Erfüll­ barkeitsverfahren intensive logische Operationen erfordern, kann das Hardware-Verfahren große Vorteile durch direktes Ab­ bilden von Teilen der SAT-Ausdrücke auf Verknüpfungsglieder (Logikgatter) und durch Nutzbarmachen großer Beträge an Paral­ lelität in der Auswertung der Logik zeigen.

Ein FPGA (feldprogrammierbares Gate-Array) ist eine be­ kannte integrierte Schaltung, deren Funktionalität in Software selbst programmiert und verändert werden kann. Da FPGAs wohl­ bekannt und kommerziell erhältlich sind (zum Beispiel der VIRTUALOGIC SLI EMULATOR von IKOS Systems, Inc.), werden deren De­ tails zur Klarheit weggelassen. FPGAs sind in konfigurierbaren Hardware-Systemen nützlich. Das heißt, FPGAs können eine Hard­ ware-Maschine bereitstellen, deren Funktionalität sich als Re­ aktion auf Programmieren durch Software ändern kann.

Konfigurierbare Hardwaresysteme sind auf unterschiedliche Arten verwendet worden. Frühere Verwendungen von konfigurier­ barer Berechnung sind häufig auf Anwendungen gerichtet gewesen, die rechenintensiv sind und einheitliche Daten aufweisen. Frü­ here konfigurierbare Berechnungsanwendungen sind daher im all­ gemeinen dadurch gekennzeichnet gewesen, daß die programmier­ bare Logik der FPGAs typischerweise aus einer großen Anzahl von parallelen Datenwegen und sehr geringer Steuerung besteht. Mit anderen Worten haben konfigurierbare Berechnungsanwendungen nur einen einfachen Steuerablauf verwendet.

Die Boolesche SAT ist ein Problem, das mehr als einen ein­ fachen Steuerablauf erfordert, und ein erstes konfigurierbares Hardware-System zum Implementieren der Booleschen SAT wurde durch dieselben Erfinder in der am 28. August 1997 eingereichten US-Patentanmeldung 08/919,282 vorgeschlagen, die hierin in ih­ rer Gesamtheit als Verweisquelle aufgenommen wird. Dieses erste SAT-lösende konfigurierbare Hardware-System zeichnete sich durch eine SAT-Lösungsvorrichtung aus, die allgemein auf dem Davis-Putnam-Algorithmus beruht. Der Davis-Putnam-Grundalgo­ rithmus sorgt für eine Rückwärtsverarbeitung, die chronologisch ist. Das heißt, der Algorithmus verarbeitet zu der zuletzt zu­ gewiesenen Variablen rückwärts.

Die Erfinder kennen zwei andere Vorschläge zur Lösung von SAT unter Verwendung von rekonfigurierbarer Hardware:

• - T. Suyama, M. Yokoo, und H. Sawada. Solving Satisfiability Problems on FPGA's. In 6th Int'1 Workshop on Field-Pro­ grammable Logic and Applications, Sept. 1996.
• - M. Abramovici und D. Saab. Satisfiability on Reconfigurable Hardware. In Seventh International Workshop on Field Pro­ grammable Logic and Applications, Sept. 1997.

Suyama u. a. (Suyama im folgenden) schlagen ihren eigenen SAT-Algorithmus vor, der kein Davis-Putnam-Verfahren ist. Im Suyama-Algorithmus weist jede Variable in der SAT-Formel immer einen gewissen zugewiesenen Wert auf. Der Suyama-Algorithmus fährt fort, indem er von einem vollständig definierten Satz von Werten zu einem anderen vollständig definierten Satz von Werten übergeht. Die Autoren von Suyama schlagen Heuristik vor, um den Suchraum einzuschränken, geben jedoch zu, daß die Anzahl von Zuständen, die in ihrem Verfahren aufgesucht werden, achtmal größer als das Davis-Putnam-Grundverfahren sein kann. Zusätz­ lich erfordert das Suyama-Verfahren einen Maximum-Rechner und einen komplexen Regelprüfer, was es sehr hardwareressourcenin­ tensiv macht.

Der oben genannte Vorschlag von Abramovici u. a. (Abramovici im folgenden) ist ebenfalls keine Implementierung des Davis- Putnam-SAT-Algorithmus. Der Abramovici-Vorschlag ist im Grunde eine Implementierung eines auf PODEM beruhenden Algorithmus in rekonfigurierbarer Hardware. Ein auf PODEM beruhender Algorith­ mus setzt voraus, daß eine erfüllende Zuweisung für die gesamte CNF-Formel gefunden werden kann, indem Werte einem vordefinier­ ten Teilsatz von Variablen in der Formel zugewiesen werden. Für mehr Information über diesen Algorithmustyp, siehe das folgende Dokumente das hierdurch wegen seiner nützlichen Hintergrundin­ formation als Verweisquelle aufgenommen wird:

• - P. Goel. An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic Circuits. IEEE Transactions on Computers, C30(3): 215-222, März 1981.

Dies findet eine direkte Anwendung in dem SAT-Problem, das in der ATPG-Domäne erzeugt wird, da die getestete Schaltung wohldefinierte Haupteingänge und -Ausgänge aufweist, und da der Testvektor an die Haupteingänge angelegt werden muß, wobei das Ergebnis an einem Hauptausgang beobachtet wird. Der Abramovici- Vorschlag kann daher keine generische CNF-Formel direkt behan­ deln.

Ein anderer Nachteil von PODEM (und folglich Abramovici) ist es, daß es,obwohl die Anzahl der Variablen im SAT-Entschei­ dungsbaum vermindert wird, nicht notwendigerweise eine Vermin­ derung der Anzahl von Zuständen gibt, die während der Suche auf­ gesucht werden. Es ist gezeigt worden, daß das Gewinnen von Be­ ziehungen zwischen internen Variablen in effizienten Daten­ strukturen von Davis-Putnam gegenüber PODEM den aufgesuchten Zustandsraum reduziert und die Ausführungszeit bedeutend redu­ ziert.

Ein weiterer Nachteil des Abramovici-Vorschlages sind die Hardware-Anforderungen. Diese Anforderungen schließen ein: (i) getrennte Schaltungen zur Vorwärts- und Rückwärtsimplikation, von denen jede einige Male größer als die ursprüngliche Schal­ tung ist, (ii) eine komplexe Steuerschaltung mit 2n Eingängen, 2n Ausgängen und 3 n-Bit-Registern, wobei n die Anzahl der Haupteingänge ist, (iii) einen sehr großen Stack, der n breit und n tief ist, (iv) und zwei Kopien der gesamten ursprünglichen Schaltung, um einen Test auf einen Fehler zu erzeugen. Obwohl die Autoren des Abramovici-Vorschlages zeigen, daß die Größe des Stacks potentiell reduziert werden kann, geht eine solche Verminderung mit den Kosten eines beträchtlich erhöhten Codier- und Decodierschaltungskomplexes einher. Folglich ist der Abra­ movici-Vorschlag darin nachteilig, daß die Hardware-Anforderun­ gen sehr groß sind. Wenn eine große Schaltung getestet wird, überfordert dies die gegenwärtige Chipintegrations- oder Logik­ emulationsgrenzen. Folglich sind die Hardware-Kosten um zwei Schaltungskopien zusätzlich zu Stacks und anderen Steuerstruk­ turen zu erhalten, groß.

Die meiste Software zur SAT-Lösung beruht heutzutage auf dem Davis-Putnam-Algorithmus. Neuere Software-Implementierun­ gen des Davis-Putnam-Algorithmus haben ihn auf verschiedene Weise verbessert, während derselbe grundlegende Ablauf aufrecht erhalten wird. Um mehr über die Verbesserungen zu erfahren, siehe die folgenden Dokumente, von denen jedes als Verweis­ quelle wegen seiner nützlichen Hintergrundinformation aufgenom­ men wird:

• - T. Larrabee. Test Pattern Generation Using Boolean Satis­ fiability. In IEEE Transactions on Computer-Aided Design, Ausgabe 11, Seiten 4-15, Januar 1992.
• - S. Chakradhar, V. Agrawal und S. Rothweiler. A transitive closure algorithm for test generation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(7): 1015-1028, Juli 1993.
• - P. Stephan, R. Brayton und A Sangiovanni-Vincentelli. Com­ binational Test Generation Using Satisfiability. Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, 1992. UCB/ERL Memo M92/112.
• - J. Silva und K. Sakallah. GRASP-A New Search Algorithm for Satisfiability. In IEEE ACM International Conference on CAD-96, Seiten 220-227, Nov. 1996.

Der Beitrag der GRASP-Arbeit ist beachtenswert, da sie nichtchronologische Rückwärtsverarbeitung und eine dynamische Klauselhinzufügung anwendet, um den Suchraum weiter einzu­ schränken. Die oben genannten Dokumente, die die Verbesserungen am Davis-Putnam-Algorithmus betreffen, sind auf Software-Imple­ mentierungen gerichtet. Es gibt einen Bedarf für die Implemen­ tierung solcher Verbesserungen in rekonfigurierbarer Hardware, jedoch haben keine früheren Bemühungen die erforderliche kom­ plexe Ablaufsteuerung erfolgreich erreicht. Der Steuerablauf, der mit nichtchronologischer Rückwärtsverarbeitung verbunden ist, ist sehr komplex. Nach bestem Wissen der Erfinder sind we­ der der Suyama- noch der Abramovici-Vorschlag tatsächlich über­ haupt auf einer Hardware-Plattform implementiert worden, und es sind bis jetzt nur Simulationsergebnisse präsentiert worden.

Die Erfindung ist eine Klasse eingabespezifischer konfigu­ rierbarer Hardware-Anwendungen, die sich aggressiv die zuneh­ menden Integrationsstufen und Rekonfigurierbarkeit von FPGAs nutzbar macht, indem sie schablonenbetriebene Hardware-Gestal­ tungen für jedes Problem oder jeden Datensatz, der gelöst wird, durchführt.

Eine beispielhafte Ausführungsform der Erfindung ist eine neuartige SAT-Lösungsvorrichtung. Die SAT-Lösungsanwendung konfigurierbarer Berechnung wurde ausgewählt, weil sie die Un­ terschiede zwischen früheren Anwendungen konfigurierbarer Be­ rechnung und dem erfindungsgemäßen Verfahren hervorhebt. Ins­ besondere ist die SAT-Lösung eine suchintensive Anwendung, wo­ hingegen frühere Verwendungen konfigurierbarer Berechnung sich auf Anwendungen gerichtet haben, die rechenintensiv sind und einheitliche Daten aufweisen. Frühere konfigurierbare Berech­ nungsanwendungen haben sich auf das Letztgenannte konzentriert, wobei die programmierbare Logik typischerweise aus einer großen Zahl paralleler Datenwege und sehr geringer Steuerung bestand. Folglich zeigt die beispielhafte SAT-Lösungsvorrichtung, als eine Ausführungsform, ein Verfahren der Verwendung konfigurier­ barer Berechnung für Algorithmen mit komplexem Steuerablauf. Es wird erkannt werden, daß die Ausführungsform lediglich bei­ spielhaft für die breitere Erfindung des Implementierens eines komplexen Steuerablaufes in rekonfigurierbarer Hardware ist.

Frühere Versuche, konfigurierbare Berechnung in Anwendungen zu verwenden, haben Implementierungen mit ziemlich einfachen datenzentrischen verkürzten Gestaltungen bereitgestellt. Diese Erfindung sorgt für eine Implementierung komplexer Steuerstruk­ turen. Wohingegen die Suchalgorithmen, die bisher durch konfi­ gurierbare Berechnung implementiert worden sind, im allgemeinen einfache Signalverarbeitungspipelines aufweisen, offenbart die Erfindung, wie ein Baumsuchalgorithmus mit einer Hardware-Aus­ führung nichtchronologischer Rückwärtsverarbeitung implemen­ tiert werden kann, die ähnlich zu jener ist, die in Software- SAT-Lösungsvorrichtungen zu sehen ist. Dies erfordert komplexe Steuerstrukturen, um die Rückwärtsverarbeitungsschritte zu ver­ walten.

Ein weiterer Grund dafür, daß die SAT-Lösungsvorrichtung nützlich für die Lehre der Erfindung ist, ist es, daß es wahr­ scheinlich ist, daß jede Suchstrategie eine beträchtliche Menge von Logikoperationen auf Bitebene verwendet. Dieser Aspekt nutzt die Logikparallelität auf Bitebene direkt aus, die durch programmierbare Logik angeboten wird, und stellt eine Berech­ nungsbeschleunigung bereit.

Der Ausdruck "eingabespezifische" konfigurierbare Hard­ ware-Anwendung bedeutet die Verwendung konfigurierbarer Hard­ ware (z. B. FPGAs), um Berechnungen zu beschleunigen, die auf einem spezifischen Problem beruhen. Das heißt, ausgehend von einer allgemeinen Lösungsschablonengestaltung, sorgt die Erfin­ dung für die Spezialisierung der Beschleunigervorrichtungs­ gestaltung auf die besondere SAT-Formel, die gelöst wird. Folg­ lich wird die Hardware konfiguriert, um die besonderen Probleme zu lösen, die gelöst werden müssen (d. h. die "Eingabe"). Da die Hardwarekonfiguration auf die Eingabe oder das Problem zuge­ schnitten ist, erwachsen größere Vorteile als in der Situation, in der die Hardware allgemeiner konfiguriert ist.

Andere Ausführungsformen der Erfindung schließen das neu­ artige nichtchronologische Verfahren ein, wie es auf Suchpro­ bleme im allgemeinen angewandt wird; wie es auf SAT-Probleme im besonderen angewandt wird; wie es in einem Computersystem aus­ geführt wird, das konfigurierbare Hardware aufweist; wie es in einem Computersystem ohne konfigurierbare Hardware ausgeführt wird; und wie es in Softwareanweisungen auf einem computerver­ wendbaren Medium ausgeführt wird.

Fig. 1 zeigt einen Pseudocode für einen grundlegenden Suchal­ gorithmus.

Fig. 2 zeigt eine Schaltung zur Implikation und Konfliktdetek­ tion.

Fig. 3 zeigt eine globale Schaltungstopologie.

Fig. 4 zeigt ein Zustandsdiagramm für eine Maschine mit chro­ nologischer Rückwärtsverarbeitung.

Fig. 5 zeigt ein Zustandsdiagramm für eine Maschine mit nicht­ chronologischer Rückwärtsverarbeitung.

Fig. 6 zeigt ein Suchbeispiel für grundlegende Rückwärtsverar­ beitung.

Fig. 7(a) und 7 (b) zeigen zwei Suchbeispiele für nicht­ chronologische Rückwärtsverarbeitung. Insbesondere zeigt Fig. 7(a) den Algorithmus im Hardware-Algorithmus der Erfindung, und Fig. 7(b) zeigt einen in GRASP ver­ wendeten Software-Algorithmus.

Das SAT-Problem

Das Boolesche Erfüllbarkeits-(SAT-) Problem ist ein wohl­ bekanntes Zwangserfüllungsproblem mit vielen Anwendungen bei computergestützter Gestaltung integrierter Schaltungen, wie z. B. Testerzeugung, Logikprüfung und Timinganalyse. Bei einer gege­ benen Booleschen Formel ist die Aufgabe entweder (a) eine Zu­ weisung von 0-1 Werten zu den Variablen zu finden, so daß die Formel sich als wahr berechnet, oder (b) festzustellen, daß eine solche Zuweisung nicht existiert.

Die Boolesche Formel wird typischerweise in Konjunktivnor­ malform (CNF) ausgedrückt, die auch als Summenproduktform be­ zeichnet wird. Jede Boolesche Formel kann in CNF ausgedrückt werden. In dieser Form ist ein Summenausdruck (Klausel) in der CNF eine Summe von einzelnen Literalen, wobei ein Literal eine Variable oder deren Negation ist. Eine n-Klausel ist eine Klau­ sel mit n Literalen. Zum Beispiel ist (v_i + v_j + v_k) eine 3-Klausel. Damit sich für die gesamte Formel 1 ergibt, muß jede Klausel erfüllt werden, d. h. 1 ergeben.

Eine Zuweisung von 0-1 Werten zu einem Teilsatz von Varia­ blen (als partielle Zuweisung bezeichnet) könnte einige Klau­ seln erfüllen und andere unbestimmt lassen. Zum Beispiel würde eine Zuweisung von v_i = 1 (v_i +v_j + v_k) erfüllen, während v_i = 0 die Klausel unbestimmt läßt. Wenn eine unbestimmte Klausel in sich nur ein nichtzugewiesenes Literal aufweist, muß sich die­ ses Literal zu 1 berechnen, um die Klausel zu erfüllen. In einem solchen Fall heißt es, daß die entsprechende Variable zu jenem Wert impliziert ist. Zum Beispiel impliziert die partielle Zu­ weisung v_i = 0, v_k = 0, daß v_j = 0. Eine Variable, die nicht impliziert ist, wird als frei betrachtet. Ein Konflikt oder Wi­ derspruch tritt auf, wenn der zu einer Variablen implizierte Wert sich von dem Wert unterscheidet, der vorher zu jener Va­ riablen impliziert oder zugewiesen worden ist. Die Detektion eines Konflikts läßt darauf schließen, daß die entsprechende partielle Zuweisung kein Teil irgendeiner gültigen Lösung sein kann.

Die meisten gegenwärtigen SAT-Lösungsvorrichtungen beruhen auf dem Davis-Putnam-Algorithmus, wie in Fig. 1 dargestellt. Das folgende wird wegen seinem nützlichen Hintergrund zu diesem Thema als Verweisquelle aufgenommen: M. Davis und H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, 7 :201-215, 1960. Der Grundalgorithmus geht von einer lee­ ren partiellen Zuweisung aus. Er fährt fort, indem er jeweils einen Wert von 0 oder 1 einer freien Variable zuweist. Nach je­ der Zuweisung stellt der Algorithmus die direkten und transi­ tiven Implikationen jener Zuweisung auf andere Variablen fest. Wenn kein Widerspruch während der Implikationsprozedur festge­ stellt wird, wählt der Algorithmus die nächste freie Variable, und wiederholt die Prozedur. Andernfalls versucht der Algorith­ mus eine neue partielle Zuweisung, indem er das Komplement der zuletzt zugewiesenen Variable bildet, für die bisher nur ein Wert ausprobiert worden ist. Dieser Schritt wird Rückwärtsver­ arbeitung genannt. Der Algorithmus endet, wenn keine freien Va­ riablen verfügbar sind und keine Widersprüche angetroffen wor­ den sind (was darauf schließen läßt, daß alle der Klauseln er­ füllt worden sind und eine Lösung gefunden worden ist), oder wenn alle möglichen Zuweisungen erschöpft worden sind. Der Al­ gorithmus ist darin vollständig, daß er eine Lösung finden wird, wenn sie existiert.

Das Bestimmen von Implikationen ist entscheidend für ein Einschränken des Suchraums, da (1) es dem Algorithmus gestat­ tet, ganze Bereiche des Suchraums, die widersprüchlichen par­ tiellen Zuweisungen entsprechen, zu überspringen, und (2) jede implizierte Variable einer freien Variablen weniger entspricht, an der die Suche ausgeführt werden muß. Leider ist das Detek­ tieren von Implikationen in Software sehr langsam, da jede Klau­ sel, die die neu zugewiesene oder implizierte Variable enthält, abgetastet und sequentiell aktualisiert wird, wobei der Prozeß wiederholt wird, bis keine neuen Implikationen detektiert wer­ den.

Die für den Algorithmus zentrale Implikationsprozedur ist sowohl parallelisierbar als auch auf Grundverknüpfungsglieder abbildbar. Die gesamte Hardware-Architektur der Erfinder ist so gestaltet, daß diese Parallelität ausgenutzt wird. Im folgenden wird die Abbildung des Davis-Putnam-Algorithmus auf rekonfigu­ rierbare Hardware in einer formelspezifischen Weise detailliert dargelegt.

Formelspezifische Abbildung: Davis-Putnam-Algorithmus Hardware-Organisation

Analog zu Software weist die Hardware-Implementierung der Erfinder des Davis-Putnam-Algorithmus zwei Teile auf: (i) die Implikationsschaltung, und (ii) eine Zustandsmaschine, um die auf Rückwärtsverarbeitung beruhende Untersuchung des Suchraums zu verwalten. Eine SAT-Formel vorausgesetzt werden beide Hard­ ware-Module automatisch erzeugt.

Die Beschleunigung gegenüber Software rührt von der Imple­ mentierung der Erfinder der Implikationsschaltung her. Im Ge­ gensatz zu Software findet diese Schaltung alle direkten Impli­ kationen einer neu zugewiesenen oder aller neu implizierten Va­ riablen in einem einzigen Taktzyklus. Folglich können alle transitiven Implikationen einer neuen Variablenzuweisung in ei­ nem kleinen Bruchteil der Taktzyklen bestimmt werden, die bei Software erforderlich sind.

In der Erfindung weist jede Variable eine Implikations­ schaltung auf.

Die Implikationsschaltung

Fig. 2a und Fig. 2b zeigen die Details einer beispielhaften Implikationsschaltung. Der Zustand jeder Variablen in der Schaltung wird durch die Werte codiert, die durch seine Literale angenommen werden. Wenn eine Variable v gegeben ist, hat die Variable v, wenn ihr Literalpaar (v,v) den Wert (0,0) aufweist, weder durch Implikation noch durch Zuweisung einen Wert zuge­ wiesen bekommen und ist frei. Wenn sie den Wert (1,0) oder (0,1) aufweist, ist zu verstehen, daß die Variable v jeweils den Wert 1 oder 0 aufweist. Wenn schließlich (v,v) den Wert (1,1) an­ nimmt, gibt es einen Widerspruch, da die Variable v nicht gleichzeitig die Werte 1 und 0 annehmen kann.

Die Rolle der Implikationsschaltung ist es, den implizier­ ten Wert jedes Literals zu bestimmen. Ein Literal ergibt 1, wenn es entweder zu 1 impliziert oder 1 zugewiesen ist. In der Schal­ tung ist der Wert jedes Literals daher das Boolesche ODER seiner implizierten und zugewiesenen Werte. Es tritt ein Widerspruch auf, wenn beide Literale jeder Variable 1 werden. Das Wider­ spruchssignal wird als das Boolesche ODER des UNDs jedes Paares von Literalen erzeugt.

Um den implizierten Wert eines Literals zu bestimmen, muß die Schaltung die Beziehungen zwischen Variablen zusammenfas­ sen, die sich aus den Klauseln in der CNF-Formel ergeben. Die Schaltung wird normalerweise für jede Variable unterschiedlich sein.

Eine beispielhafte Implikationsschaltung für ein Literal a wird nun unter Bezugnahme auf Fig. 2a beschrieben. Wenn die Klauseln (c + a) (d + a) (b + c + a) (e + a) (c + a) gegeben sind, kann ge­ schlossen werden, daß dann, wenn c = 1, oder wenn d = 1, oder wenn b = 1 und c = 0, a den Wert 1 annehmen muß, d. h. a ist zu 1 impliziert. Entsprechend ist, wenn e = 0 oder c = 0, a zu 0 impliziert. In diesem Beispiel würde die Gleichung für den im­ plizierten Wert des Literals a a_imp = c + d + bc sein, wie in Fig. 2a gezeigt. c, d, b und c sind die Literale für die entsprechen­ den Variablen. Entsprechend würde die Gleichung für das Literal a a_imp = e + c sein.

Eine beispielhafte Implikationsschaltung für das Literal c wird nun unter Bezugnahme auf Fig. 2b beschrieben. Wenn diesel­ ben fünf Klauseln (c + a) (d + a) (b + c + a) (e + a) (c + a) gegeben sind, kann aus der ersten Klausel geschlossen werden, daß dann, wenn a den Wert 0 annimmt, c zu 1 impliziert ist. Die zweite Klausel. Die zweite Klausel impliziert c nicht. In der dritten Klausel kann geschlossen werden, daß dann, wenn a = 0 und b = 0, c zu 1 impliziert ist. Die vierte Klausel impliziert c nicht. Es kann aus der fünften Klausel geschlossen werden, daß dann, wenn a = 0 ist, c zu 1 impliziert ist. Die Gleichung für den implizierten Wert des Literals c würde c_imp = ab + a sein; diese Gleichung spie­ gelt sich in den Verknüpfungsgliedern der Fig. 2b wider. Die Gleichung für das Literal c würde c_imp = a sein. Fig. 2b zeigt zur Veranschaulichung a als die einzige Eingabe zu einem ODER-Glied.

Folglich variiert die Implikationsschaltung für jedes Li­ teral, abhängig von den CNF-Klauseln im zu lösenden Problem.

Selbst das kleine Beispiel oben weist eine Schleife in den Implikationsabhängigkeiten auf, da die Werte der Literale a und c voneinander abhängig sind. Theoretisch kann die gesamte Schal­ tung zur Berechnung der Werte aller Literale in der Formel ohne irgendwelche Flipflops implementiert werden, trotz des Vorhan­ denseins solcher Schleifen. Da die Schleifen alle nichtinver­ tierend sind, gewährleistet die Kombinationsschaltung, daß sie zu korrekten Werten konvergiert, aber es kann extrem lange Korn­ binationswege und sich daraus ergebende lange Zykluszeiten ge­ ben.

Um diese Probleme zu vermeiden, wird eine Schaltung verwen­ det, in der jedes Literal durch ein getaktetes D-Flipflop zwi­ schengespeichert wird, bevor es zurückgeführt wird. Während je­ des Taktzyklus bestimmt die Schaltung parallel die direkten Im­ plikationen aller Variablen, die im vorhergehenden Zyklus zu­ gewiesen oder impliziert wurden. Die Prozedur endet, wenn keine neuen Implikationen während eines Taktzyklus detektiert werden. Neue Implikationen werden detektiert, indem eine EXKLUSIV-ODER-Ver­ knüpfung der Eingabe und Ausgabe des D-Flipflops für jedes Literal vorgenommen wird. Wenn irgendeines der EXKLUSIV-ODER-Glie­ der eine Ausgabe von 1 aufweist (d. h. LChange 1 ist), muß die Schaltung einen weiteren Taktzyklus durchlaufen. Die Anzahl von Taktzyklen vom Anfang der Implikationsprozedur mit der jüngsten Variablenzuweisung bis zur Erzeugung des Vollendungs­ signals ist potentiell sehr viel kleiner als bei Software, da eine potentiell größere Anzahl neuer Implikationen in jedem Taktzyklus erzeugt wird, und alle der folgenden direkten Impli­ kationen, die sich aus diesen neu implizierten Variablen erge­ ben, sofort im nächsten Taktzyklus parallel bestimmt werden. Diese Parallelität ist in der Praxis ziemlich beachtlich: für das aim-100-6_0-yes1-1-Beispiel in der DIMACS-Reihe, ergibt dieses Verfahren einen Mittelwert von 41,9 Parallelklauselbe­ rechnungen pro Zyklus. In jenem Beispiel werden 395 Klauseln in einem einzigen Zyklus effektiv verarbeitet. Diese Zahlen sind typisch für andere Leistungsvergleiche.

Globale Schaltungstopologie und die Rückwärtsverarbitungs- Zustandsmaschine

Zwei wichtige Merkmale der erfindungsgemäßen Schaltungsor­ ganisation sind es, daß (i) eine getrennte Zustandsmaschine für jede Variable implementiert wird, (ii) die Reihenfolge, mit der Variablen zugewiesen werden, im voraus festgelegt wird. Dement­ sprechend nimmt die erfindungsgemäße globale Schaltungstopolo­ gie die in Fig. 3 gezeigte Form an. Jeder Kasten in der Figur enthält die Literalberechnungsschaltung und die Zustandsma­ schine für jede Variable. Diese verteilte Topologie hält die globalen Signale auf einem Minimum und verringert die Hardware- Kosten. Auf jeden Fall übt nur eine Zustandsmaschine die Kon­ trolle aus. Sobald jene Zustandsmaschine die Verarbeitung be­ endet hat, bestätigt sie E_or (d. h. Freigabesignal zum Abgeben nach rechts), um die Kontrolle zur Zustandsmaschine auf der rechten Seite zu übertragen (wenn bei der Berechnung vorwärts verarbeitet wird) oder sie bestätigt E_ol (d. h. Freigabesignal zum Abgeben nach links), die Kontrolle nach links (wenn rück­ wärtsverarbeitet wird). Jede Zustandsmaschine weiß, ob ihre Va­ riable zugewiesen worden ist, impliziert oder frei ist.

Die Zustandsmaschine für eine einzelne Variable wird in Fig. 4 gezeigt. Die fünf Zustände in der Zustandsmaschine werden durch drei Bit codiert. Jede Zustandsmaschine ist im wesentli­ chen identisch. Zwei Bit entsprechen den Werten der positiven und negativen Literale ihrer Variable. Das dritte Bit zeigt an, ob diese besondere Zustandsmaschine aktiv ist.

Die Eingänge zu jeder Zustandsmaschine schließen E_il (d. h. Freigabesignal Eingehen von links), E_ir (Freigabesignal Eingehen von rechts), GContra (das globale Widerspruchssignal), GChange (das globale Wechselsignal) und GClear (das globale Signal, um alle Flipflops rückzusetzen) ein. Jede Zustandsmaschine wird in üblicher Weise durch ein gemeinsames Taktsignal getaktet.

Die Ausgänge von jeder Zustandsmaschine schließen (die be­ reits erwähnten) E_ol und E_or, LContra (das lokale Widerspruchs­ signal), LChange (das lokale Wechselsignal), LClear (das lokale Löschsignal) ein. In Fig. 3 werden die Eingänge und Ausgänge für jede Zustandsmaschine gezeigt. Die Maschine v_i-1 ist links von der Maschine v_i; die links von der Maschine v_i+1 ist. Obwohl es der Klarheit willen nicht gezeigt wird, werden alle LChange- Ausgänge miteinander ODER-verknüpft, um GChange zu erzeugen; werden alle LContra-Ausgänge miteinander ODER-verknüpft, um GContra zu erzeugen; und werden alle LClear-Ausgänge miteinander ODER-verknüpft, um GClear zu erzeugen. Ebenfalls der Klarheit willen nicht gezeigt wird, daß der GChange-Eingang jeder Ma­ schine gemeinsam ist, wie es der GContra-Eingang und der GClear- Eingang sind.

Auch wird in den Figuren nicht gezeigt, daß es ein Impli­ kationssignal gibt. Man erinnere sich, daß jede Maschine über­ wacht, ob seine Variable frei, zugewiesen oder impliziert ist. Wenn ein Wert von 1 das Ergebnis für entweder v_imp oder v_imp ist, dann ist die Variable impliziert. Ein lokales Implikationssi­ gnal kann folglich so verstanden werden, daß es innerhalb einer bestimmten Zustandsmaschine aus v_imp + v_imp erhältlich ist. Das lokale Implikationssignal ist darin nützlich, daß es der Zu­ standsmaschine erlaubt, schnell durch Zustände zu springen, wo ein Wert einer Variablen schon impliziert ist.

In Fig. 4 wird die folgende Konvention verwendet. Nahe bei jeder Zustandsübergangslinie erscheint eine Legende. Jede Le­ gende hat das Format Eingabe/Ausgabe. Das heißt, die Einträge, die dem Schrägstrich (/) vorangehen, sind die Eingaben, die er­ forderlich sind, um die Zustandsmaschine zu veranlassen, von ihrem gegenwärtigen Zustand zu dem Zustand über zugehen, der durch die Zustandsübergangslinie angezeigt wird. Die Einträge, die dem Schrägstrich folgen, sind die Ausgaben, die als ein Er­ gebnis des Zustandsübergangs geliefert werden. Insbesondere sind diese Ausgaben E_ol und E_or.

Es gibt zum Beispiel eine Zustandsübergangslinie vom init- Zustand zum active 1-Zustand. Die Legende, die nahe dieser Zu­ standsübergangslinie erscheint, ist E_il()/00. Diese Le­ gende bedeutet, daß dann, wenn sich die Zustandsmaschine im init- Zustand befindet, wenn E_il 1 wird und es keine Werte gibt, die für die Variable v impliziert sind, der Zustand der Zustands­ maschine zum active 1-Zustand übergeht und die Zustandsmaschine 0 für E_ol und 0 für E_or ausgibt (wodurch die gegenwärtige Zu­ standsmaschine als die aktive Zustandsmaschine gehalten wird).

Vorwärtsberechnung: Nach der Initialisierung befinden sich alle Zustandsmaschinen im init-Zustand. Wenn eine Zustandsma­ schine ein Freigabesignal erhält, werden die gegenwärtigen Li­ teralwerte und die Freigaberichtung verwendet, um festzustel­ len, ob ein neuer Wert geltend gemacht wird, und welcher neue Wert geltend gemacht wird. Wenn die Kontrolle von der linken Seite übertragen wird (d. h. E_il = 1) und der Wert der Variable gegenwärtig frei ist (d. h. sie sich im init-Zustand befindet und kein Wert impliziert ist; (v,v) weist den Wert (0,0) auf), dann macht sie den Wert 1 geltend (der zu active 1 übergegangen ist) und bestimmt alle der transitiven Implikationen jener Zuwei­ sung. Das heißt, (v,v) wird auf (1,0) gesetzt. Auf Fig. 2a be­ zugnehmend, würde z. B. das Setzen von (a,a) auf (1,0) erreicht, indem a_state = 1 und a_state = 0 gesetzt werden. Während die Impli­ kationen sich noch setzen (d. h. solange GChange geltend gemacht wird) und es keinen Widerspruch gibt (d. h. solange, wie GContra 0 ist), wartet der Prozeß, indem er wiederholt in denselben Zu­ stand übergeht. Sobald sich die Implikationen gesetzt haben, kann es Widersprüche geben. Wenn dem so ist, (d. h. GContra gel­ tend gemacht wird) wird sie statt dessen den Wert 0 ausprobieren (active 0) und den Implikationsschritt wiederholen. Wenn nicht, überträgt sie die Kontrolle an die Zustandsmaschine zu ihrer Rechten und geht in den passive 1-Zustand über. Von active 0 wird sie, wenn ein Widerspruch detektiert wird, rückwärts verarbei­ ten. Ihr Zustand wird auf init rückgesetzt und die Kontrolle wird nach links weitergegeben. Andererseits geht sie, wenn sich Im­ plikationen ohne einen Widerspruch gesetzt haben, von active 0 zu passive 0 und gibt die Kontrolle nach rechts weiter.

Wenn, wie oben, die Kontrolle an eine Zustandsmaschine von links übertragen wird, jedoch ihr Variablenwert schon durch eine vorhergehende Zuweisung impliziert worden ist (d. h. ent­ weder v_imp = 1 oder v_imp = 1), dann gibt sie beim nächsten Takt­ zyklus lediglich die Kontrolle an die Zustandsmaschine zu ihrer Rechten weiter und verbleibt im init-Zustand.

Rückwärtsverarbeitung: Wenn die Kontrolle auf eine Zu­ standsmaschine von der rechten Seite übertragen wird, dann ist infolge eines Widerspruchs das Berechnen eine Rückwärtsverar­ beitung, und das Ziel ist es, zu versuchen, eine neue Zuweisung zu finden, die den Widerspruch vermeidet. In diesem Szenario gibt es drei mögliche Reaktionen, die wiederum von den gegen­ wärtigen lokalen Variablenwerten abhängen.

Erstens, wenn sich die Zustandsmaschine im init-Zustand be­ findet (was der Fall sein kann, wenn die Variable während einer früheren Vorwärtsberechnung durch eine vorhergehende Zuweisung impliziert worden ist), dann bleibt die Zustandsmaschine im init- Zustand und gibt die Kontrolle an die Zustandsmaschine zu ihrer Linken weiter.

Zweitens, wenn der Variablen gegenwärtig der Wert 1 zuge­ wiesen ist (d. h. sie sich im passive 1-Zustand befindet), dann weist sie ihr statt dessen den Wert 0 zu (geht zu active 0), und bestimmt die Implikationen jener Zuweisung. Wenn kein Wider­ spruch gefunden wird, dann ist der Konflikt aufgeklärt worden, und die Berechnung kann noch einmal fortschreiten, indem diese Zustandsmaschine die Kontrolle zu ihrer Rechten weitergibt. Wenn jedoch wieder ein Widerspruch gefunden wird, dann wird sie auf init rückgesetzt und überträgt die Kontrolle nach links.

Das dritte mögliche Szenario ist es, daß diese Variable schon den zugewiesen Wert 0 aufweist (d. h. sich im passive 0-Zu­ stand befindet). Dies zeigt an, daß der Prozeß schon beide mög­ lichen Werte für diese Variable ausprobiert hat; in diesem Fall geht er in den init-Zustand über, wodurch die Zuweisung seines Werts freigegeben wird, und verarbeitet rückwärts, indem die Kontrolle nach links übertragen wird.

Finden einer Lösung: An jeder Stelle in den obigen Beschrei­ bungen ist eine Lösung gefunden worden, wenn die am weitesten rechts liegende Zustandsmaschine weiter versucht, die Kontrolle nach rechts weiterzugeben. Andererseits, wenn die am weitesten links liegende Zustandsmaschine versucht, rückwärts zu verar­ beiten, indem sie weiter die Kontrolle nach links weitergibt, dann zeigt dies an, daß keine Lösung für das Problem existiert.

Formelspezifische Abbildung: Nichtchronologische Rückwärtsverarbeitung Algorithmus

Wenn der Davis-Putnam-Algorithmus zu der zuletzt zugewie­ senen Variable rückwärtsverarbeitet, wird seine Rückwärtsver­ arbeitung chronologisch genannt. Wenn andererseits ein Algo­ rithmus über mehrere vorher zugewiesene Variablen zu einer Va­ riablen springt, die mehr als eine Ebene über der gegenwärtigen Variablen liegt, wird die Rückwärtsverarbeitung nichtchronolo­ gisch genannt. Um direkt zu einer vorhergehenden Ebene zu sprin­ gen, muß der Algorithmus zuerst feststellen, daß keine Kombi­ nation von Werten bei den übersprungenen Variablen zu einer er­ füllenden Zuweisung führen wird. Durch intelligentes Springen über diese Variablen vermeidet der Algorithmus es, die Zeit zu verschwenden, die es braucht, um diese Variablen explizit ihrer vorherigen Kombination von Werten zuzuweisen, nur um festzu­ stellen, daß alle diese Kombinationen zu einen Widerspruch füh­ ren. GRASP ist eine jüngste Implementierung nichtchronologi­ scher Rückwärtsverarbeitung in einer SAT-Lösungsvorrichtung. Die GRASP-Arbeit demonstrierte, daß nichtchronologische Rück­ wärtsverarbeitung zu beträchtlichen Verringerungen der Laufzeit führen kann.

GRASP erhält eine Datenstruktur aufrecht, die als ein Im­ plikationsgraph bezeichnet wird, aus dem man die Kette von Im­ plikationen ableiten kann, die zu dem Widerspruch führen. GRASP verwendet diese Datenstruktur, um die Ebene zu identifizieren, zu der er springen kann.

Es ist sehr schwierig, in rekonfigurierbarer Hardware einen solchen Implikationsgraph zu implementieren. Dies würde bein­ halten, zusätzliche Hardware hinzuzufügen, um die Implikations­ schaltungen zu durchgehen, um die Quelle der Konflikte oder Wi­ dersprüche zu identifizieren. Es wird daran erinnert, daß die Erfindung die schnelle Entwicklung einer kundenspezifischen Hardwareschaltung beinhaltet, um ein spezifisches Problem zu lösen. Für dieses Verfahren darf es, um im Vergleich zur Ver­ wendung von nur Software insgesamt Zeit einzusparen, nicht zu lange brauchen, die kundenspezifischen Hardwareschaltung anzu­ ordnen, und sie darf nicht zu aufwendig hinsichtlich der Hard­ ware-Ressourcen sein.

Das erfindungsgemäße Verfahren nutzt die Tatsache aus, daß infolge der Parallelität das Bestimmen von Implikationen in der oben genannten Hardware-Implementierung der SAT-Lösungsvor­ richtung sehr schnell ist. Insbesondere wenn ein Widerspruch für beide Zuweisungen einer bestimmten Variablen auftritt, ist es das Ziel, auf die Variable zurückzukommen, die der gegenwär­ tigen Variable am nächsten ist, so daß, indem der Wert zu dieser früheren Variablen gekippt wird, der Widerspruch dazu gebracht werden kann, zu verschwinden. Dieses Verfahren spart Zeit, da der Prozeß zu dieser früheren Variable zurückkommt, ohne eine Exponentialzahl von Kombinationen von Werten bei den Variablen ausprobiert zu haben, die übersprungen wurden.

Es wird angenommen, daß v_i die Variable ist, für die ein Widerspruch für beide Zuweisungen zu v_i detektiert wurde, wobei i ihre Ebene ist. Die erfindungsgemäße Prozedur arbeitet sich die Ebenen hoch, jeweils eine Ebene auf einmal. Auf jeder Ebene j (< i), ruft die Prozedur die Implikationsroutine zweimal auf, einmal für jeden Wert für v_i, während v_j einen gekippten Wert aufweist. Die Variablen v_k zwischen i und j (j < k < i) bleiben nicht zugewiesen wenn die Implikationsroutine aufgerufen wird, d. h. beide Literale v_k und v_k werden auf 0 gesetzt. Der Algo­ rithmus muß zu v_j rückwärts verarbeiten, wenn ein Nichtwider­ spruchsfall für eine der beiden Zuweisungen gefunden wurde. Wenn beide Zuweisungen von v_i einen Widerspruch verursachen, kann die Variable v_j übersprungen werden, und die Prozedur wie­ derholt diesen Schritt für die Variable v_j-1.

Weiter unten wird diese Operation erläutert, wobei ein de­ taillierteres Beispiel verwendet wird, in dem v_i verwendet wird, und in dem diskutiert wird, daß v_k gleich v_i-1 ist, und diskutiert wird, daß v_j gleich v_i-2 ist.

Dies Prozedur erfordert nur 2n Aufrufe der Implikationsrou­ tine, wenn der Algorithmus um n Ebenen zurückkommt. Da die Pro­ zedur die Implikationsroutine nicht eine Exponentialzahl von Malen aufruft, und da die Implikationsroutine in Hardware sehr schnell ist, kann erwartet werden, daß diese Analyse für nicht­ chronologische Rückwärtsverarbeitung ebenfalls sehr schnell ist. Im Vergleich weist GRASP den Organisationszusatz auf, daß die Implikationsgraph-Datenstruktur aufrechterhalten wird und sie analysiert wird, wenn ein Widerspruch gefunden wird, aber er führt nicht die 2n Implikationen aus.

Das folgende einfache Beispiel, das in Beziehung zu Fig. 6 zu verstehen ist, zeigt, wie die erfindungsgemäße Prozedur ar­ beitet. Angenommen, es gibt die folgende Formel:

(v₁ + v₁₂ + v₁₃) (v₁ + v₁₂ + v₁₃) (v₁ + v₁₂ + v₁₄) (v₁ + v₁₂ + v₁₄) . . .

Es wird an­ genommen, daß jede Zuweisung für die Variablen v₂-v₁₁ zu keinem Widerspruch führt. Der grundlegende Suchbaum für diese Formel wird in Fig. 6 gezeigt. In der Figur stellt jeder durchgezogene Pfeil das Zuweisen eines neuen Wertes und Bestimmen seiner Im­ plikationen dar. Er beginnt, indem v₁ = 1 zugewiesen wird und geht weiter bis v₁₁ = 1. Zuletzt wird v₁₂ = 1 ausprobiert. Dies führt zu einem Widerspruch, da es erforderlich ist, daß v₁₃ gleichzeitig 0 und 1 ist (aufgrund der ersten beiden Klauseln der obigen Formel).

Entsprechend führt auch v₁₂ = 0 zu einem Widerspruch (auf­ grund auch der dritten und vierten Klauseln oben). Die normale Rückwärtsverarbeitungsprozedur würde v₁₂ auf unbekannt rückset­ zen und sie würde zu v₁₁ rückwärts verarbeiten. Der Konflikt ver­ schwindet zeitweilig, wird aber jedesmal wieder auftauchen, wenn v₁₂ gesetzt wird.

Fig. 7(a) zeigt die Ausführung der erfindungsgemäßen nicht­ chronologischen Rückwärtsverarbeitung. Die gepunkteten Pfeile zeigen ein Überspringen an und ziehen keinerlei Berechnung nach sich; sie zeigen nur einfach, welche Werte vor einer Implika­ tionsberechnung angenommen werden. Die Suche ist dieselbe wie vor dem Erreichen von v₁₂. Die Rückwärtsverarbeitung unterschei­ det sich jedoch. Wenn bei jeder Ebene rückwärts verarbeitet wird, wird die Implikationsprozedur zweimal aufgerufen. Das heißt, eine Rückwärtsverarbeitung zu v₁ findet, nachdem die Im­ plikationsprozedur effektiv nur 22 mal aufgerufen wird, eher statt als nach 4082 Versuchen mit dem Standardrückwärtsverar­ beitungsverfahren. Während dieses einfache Beispiel hauptsäch­ lich pädagogisch ist, existiert auch ein dramatisches Beschleu­ nigungspotential bei tatsächlichen Leistungsvergleichen. Zum Beispiel sucht im aim-100-1_6-yes1-1-Leistungsvergleich aus der SAT-Reihe, die chronologische Rückwärtsverarbeitung 606578 par­ tielle Zuweisungen auf, während der nichtchronologische Rück­ wärtsverarbeitungsalgorithmus nur 1384 partielle Zuweisungen aufsucht.

Das neuartige Rückwärtsverarbeitungsverfahren für die re­ konfigurierbare Hardware-SAT-Lösungsvorrichtung wird nun auf eine andere Weise erläutert. Man kann sagen, daß die SAT-Lö­ sungsvorrichtung mehrere Zustandsmaschinen aufweist, wobei jede nur einer der mehreren Variablen in einem Booleschen SAT-Pro­ blem entspricht. Die mehreren Variablen werden beruhend auf ei­ ner vorherbestimmten Heuristik geordnet, wodurch auch eine An­ ordnung der Zustandsmaschinen bereitgestellt wird, wobei die erste Zustandsmaschine der ersten Variablen entspricht und die letzte Zustandsmaschine der letzten Variablen entspricht.

Da die Variablen Boolesche sind, kann der Suchraum als ein Binärbaum mit der ersten Variablen an der Spitze oder höchsten Ebene betrachtet werden. Die Variable kann als ein Knoten be­ trachtet werden. Die beiden Werte, die die Variable annehmen kann, definieren Zweige, die vom Knoten zu einer nächst tieferen Ebene abwärts führen. Die Ebene unter der höchsten Ebene enthält einen Knoten für jeden der Zweige, und alle Knoten auf dieser Ebene entsprechen der Variable nach der ersten Variable (d. h. der zweiten Variable). Der Binärbaum geht weiter bis zur unter­ sten Ebene, auf der alle möglichen Knoten der letzten geordneten Variable entsprechen.

Durch Konvention sind die beiden Zweige, die von allen Kno­ ten führen, selbst geordnet (d. h. der Zweig, der dem Wert 1 ent­ spricht, ist der am weitesten links gelegene, und der Zweig, der dem Wert 0 entspricht, ist der am weitesten rechts gele­ gene). Zur sprachlichen Bequemlichkeit können die beiden Binär­ werte so beschrieben werden, daß sie ein erster Wert und ein zweiter Wert sind. In den Beispielen wird der erste Wert 1 sein und der zweite Wert 0, obwohl dies sicherlich beliebig ist und nur der Erläuterung dient. Auch ist der erste Wert durch Vorgabe der Wert, der einer Variablen zuerst zugewiesen wird, wenn auf logische Übereinstimmung oder Widerspruch geprüft wird. Folg­ lich werden in den Beispielen freie Variablen normalerweise zu­ erst dem ersten Wert (von 1) zum Prüfen gegeben, und dann, falls notwendig, anschließend dem zweiten Wert (von 0) gegeben.

Während der Verarbeitung weist jede Variable einen Zustand oder eine Bedingung auf, die entweder zugewiesen, impliziert, oder frei ist. Um Verwirrung mit den Zuständen der Zustandsma­ schine zu vermeiden, die unten beschrieben wird, wird der Aus­ druck Bedingung üblicherweise verwendet, um zu bezeichnen, ob eine Variable zugewiesen, impliziert oder frei ist. Folglich kann eine Variable als in einer freien Bedingung, einer impli­ zierten Bedingung oder einer zugewiesen Bedingung befindlich bezeichnet werden. Wenn die rekonfigurierbare Hardware-SAT-Lö­ sungsvorrichtung nach einer Lösung sucht, ist es normal, daß einige Variablen sich in einer zugewiesenen Bedingung befinden werden, einige sich in einer implizierten Bedingung befinden werden, und andere sich in einer freien Bedingung befinden wer­ den. Eine logische Gesamtkonsistenz unter den zugewiesenen und den implizierten Variablen besteht, wenn es keinen Widerspruch unter ihnen gibt (da freie Variablen keinen logischen Wert auf­ weisen, beeinflussen sie die logische Gesamtkonsistenz nicht). Die zugewiesenen und die implizierten Variablen können zu einem gegebenen Zeitpunkt im folgenden insgesamt als die logisch be­ wertete Netzliste bezeichnet werden.

An einer gegebenen Ebene der Verarbeitung, der Ebene i, be­ treffen alle Knoten die Variable v_i. Die Ebene über der Ebene i in Richtung der höchsten Ebene können als Ebene i-1 verstanden werden, und alle Knoten auf Ebene i-1 betreffen die Variable v_i-1. Die Ebene über Ebene i-1 wird als Ebene i-2 verstanden werden und enthält Knoten, die die Variable v_i-2 betreffen. Eine ent­ sprechende Terminologie gilt für Ebenen unter der Ebene i.

Wenn beide möglichen Binärwerte für v_i beruhend auf den zu­ gewiesenen und die implizierten Werte der anderen der mehreren geordneten Variablen (d. h. beruhend auf der logisch bewerteten Netzliste) zu einem logischen Widerspruch führen, ist es klar, daß weiteres Vorrücken zur niedrigsten Ebene nie eine SAT-Lö­ sung liefern würde. Um es zu vermeiden, Zeit damit zu verschwen­ den, durch Knoten vorzurücken, die unmöglich eine Lösung lie­ fern könnten, wird eine Rückwärtsverarbeitung durchgeführt. Ge­ nauer gesagt wird eine nichtchronologische Rückwärtsverarbei­ tung durchgeführt, um ein Maximum an Zeit zu sparen. Zur Be­ quemlichkeit kann eine Variable v_i, für die beide möglichen Bi­ närwerte zu einem logischen Widerspruch für die gegenwärtige logisch bewertete Netzliste führen, im folgenden als eine Sperrvariable bezeichnet.

Nichtchronologische Rückwärtsverarbeitung kann im Detail wie folgt durchgeführt werden. Die Sperrvariable wird als eine Blattvariable festgelegt. Die Blattvariable ist, wie unten zu sehen sein wird, dadurch gekennzeichnet, daß sie zwischen dem ersten Wert und dem zweiten Wert geschaltet wird, bis der Wi­ derspruch geklärt ist.

Dann wird die Variable v_i-1 betrachtet. Die Variable v_i-1 wird gegenwärtig als eine betrachtete Variable der oberen Ebene oder, zur Bequemlichkeit, als die Rückwärtsverarbeitungsvaria­ ble bezeichnet. Es gibt zwei Möglichkeiten, die die Rückwärts­ verarbeitungsvariable betreffen. Eine Möglichkeit ist es, daß die Rückwärtsverarbeitungsvariable den ersten Wert aufweist. Eine andere Möglichkeit ist es, daß die Rückwärtsverarbeitungs­ variable den zweiten Wert aufweist. Jede dieser beiden Möglich­ keiten wird der Reihe nach erörtert.

Es wird nun die erste Möglichkeit erörtert. Wenn der Rück­ wärtsverarbeitungsvariable schon der erste Wert zugewiesen ist, dann wird die Rückwärtsverarbeitungsvariable gekippt. Mit an­ deren Worten wird der Rückwärtsverarbeitungsvariable der zweite Wert statt des ersten Wertes zugewiesen. Nachdem der Rückwärts­ verarbeitungsvariable der zweite Wert zugewiesen ist, wird festgestellt, ob es eine Zuweisung der Blattvariablen gibt, die zu keinem gegenwärtigen Widerspruch führt. Das heißt, die lo­ gisch bewertete Netzliste wird mit der Rückwärtsverarbeitungs­ variable, die den zweiten Wert aufweist, und mit der Blattva­ riable, die den ersten Wert aufweist, auf logische Konsistenz geprüft. Wenn ein Widerspruch detektiert wird, dann wird die Blattvariable auf den zweiten Wert gekippt. Dann wird die lo­ gisch bewertete Netzliste wieder mit der Rückwärtsverarbei­ tungsvariable, die den zweiten Wert aufweist, aber mit der Blattvariable, die den zweiten Wert aufweist, auf logische Kon­ sistenz geprüft. Wenn die Variable v_i-1, die zum zweiten Wert gekippt worden ist, einen Widerspruch für jeden möglichen Wert der Blattvariable v_i liefert, dann wird die Variable der nächst höheren Ebene (d. h. Variable v_i-2) als die Rückwärtsverarbei­ tungsvariable gekennzeichnet und wird zur selben Zeit die Va­ riable v_i-1 in eine freie Bedingung gesetzt.

Es wird nun die zweite Möglichkeit erörtert. Wenn der Rück­ wärtsverarbeitungsvariable schon der zweite Wert zugewiesen ist, dann muß der erste Wert zu einem gewissen vorhergehenden Widerspruch geführt haben. Wenn der Rückwärtsverarbeitungsva­ riable schon der zweite Wert zugewiesen ist, wird daher die Rückwärtsverarbeitungsvariable nicht gekippt. Statt dessen wird die Variable der nächst höheren Ebene (d. h. Variable v_i-2) als die Rückwärtsverarbeitungsvariable gekennzeichnet und wird zur selben Zeit die Variable v_i-1 in eine freie Bedingung gesetzt.

Wenn die Variable der nächst höheren Ebene in jeder der bei­ den oben erwähnten Möglichkeiten als die Rückwärtsverarbei­ tungsvariable gekennzeichnet wird, folgt dieselbe Analyse. Mit anderen Worten gibt es zwei Möglichkeiten, die die neue Rück­ wärtsverarbeitungsvariable betreffen. Eine Möglichkeit ist es, daß die Rückwärtsverarbeitungsvariable den ersten Wert auf­ weist. Eine andere Möglichkeit ist es, daß die Rückwärtsverar­ beitungsvariable den zweiten Wert aufweist.

Wie aus der vorhergehenden Erläuterung verstanden werden wird, beinhaltet der nichtchronologische Rückwärtsverarbei­ tungsprozeß, daß eine Sperrvariable detektiert wird und sie als die Blattvariable gesetzt wird, und dann die Werte der Blatt­ variablen variiert werden, ohne jemals eine andere Variable als die Blattvariable auszuwählen. Um es anders auszudrücken, be­ inhaltet der Prozeß, daß der Wert der Blattvariable, aber nicht die Identität der Blattvariable variiert wird.

Der nichtchronologische Rückwärtsverarbeitungsprozeß be­ inhaltet auch, daß die Werte der Rückwärtsverarbeitungsvaria­ blen variiert werden, und beinhaltet auch, daß Variablen höhe­ rer und höherer Ebene ausgewählt werden, die Rückwärtsverarbei­ tungsvariable zu sein, bis der Widerspruch geklärt wird. Um es anders auszudrücken, beinhaltet der erfindungsgemäße Prozeß, daß der Wert und die Identität der Rückwärtsverarbeitungsvaria­ ble variiert werden.

Die Rückwärtsverarbeitung endet, wenn die logische Konsi­ stenz in der gegenwärtigen logisch bewerteten Netzliste er­ reicht ist. Nachdem die Rückwärtsverarbeitung endet, wird die oben erwähnte normale Vorwärtsberechnung unternommen, um eine Lösung für das SAT-Problem zu identifizieren. Beim Umschalten von Rückwärtsverarbeitung auf die Vorwärtsberechnung, wird die Blattvariable in eine freie Bedingung gesetzt. Die Vorwärtsbe­ rechnung geht von der gegenwärtigen Rückwärtsverarbeitungsva­ riablen nach unten weiter.

Hardware-Organisation

Um den obigen neuartigen nichtchronologischen Rückwärtsver­ arbeitungsalgorithmus zu implementieren, muß die Zustandsma­ schine von der Ausführungsform mit chronologischer Rückwärts­ verarbeitung modifiziert werden. Als ein besonders vorteilhaf­ ter Aspekt der gegenwärtig bevorzugten Ausführungsform werden keine neuen globalen Signale hinzugefügt und die Implikations­ schaltung wird auch nicht modifiziert.

Die Zustandsmaschine, um die nichtchronologische Rückwärts­ verarbeitung durchzuführen, wird in Fig. 5 gezeigt. Sie weist mehr Zustände und Übergänge auf, um die komplexe Rückwärtsver­ arbeitungsprozedur widerzuspiegeln, die vorhergehend skizziert worden ist. Obwohl die Zustandsmaschine größer geworden ist, benötigen die zusätzlichen Zustände nur ein Codierbit mehr.

Obwohl die Bedeutung der in Fig. 5 gezeigten Zustandsma­ schine in wesentlichen für jene selbsterklärend ist, die auf diesem Gebiet Bescheid wissen, wird nun eine kurze Erläuterung von ihr bereitgestellt werden.

Jede Variable beginnt im init-Zustand. Im init-Zustand kann die Variable v_i sich in einer freien Bedingung oder in einer implizierten Bedingung befinden. Im init-Zustand bewirkt dann, wenn die Variable nicht impliziert ist (d. h. wenn (v_imp + v_imp)), ein E_il-Signal einen Übergang von init zu active 1. Wenn sie sich in active 1 befindet, wird der Variable v_i der erste Wert gegeben, der in dieser Ausführungsform 1 ist. Nimmt man keinen Wider­ spruch an, wird GChange sich im Hochpegelzustand befinden, bis sich alle Implikationen setzen und der Zustand wird normaler­ weise nicht übergehen. Wenn GChange auf einen Tiefpegelzustand geht, haben sich die Implikationen gesetzt. Kein Widerspruch bedeutet, daß sich GContra im Tiefpegelzustand befindet. Wenn sich sowohl GChange als auch GContra im Tiefpegelzustand befin­ den, werden die Bedingungen erfüllt, um zu passive 1 überzugehen. Übergehen zu passive 1 bewirkt auch eine Ausgabe von 0 für E_ol und 1 für E_or. Die Ausgabe 1 für E_or aktiviert die Maschine zur Rech­ ten, die der Variable v_i+1 der nächst tieferen Ebene entspricht.

Wenn sie sich in active 1 befindet, erinnere man sich, daß der Variable v_i der erste Wert gegeben worden ist. Wenn dieser Wert zu einem Widerspruch mit der logisch bewerteten Netzliste führt, dann wird das GContra-Signal empfangen. Sobald das GCon­ tra-Signal empfangen wird, ob die Implikationen entschieden sind oder nicht, werden die Bedingungen erfüllt, um zu active 0 über­ zugehen. Übergang zu active 0 bewirkt eine Ausgabe von 0 für E_ol und 0 für E_or. Mit anderen Worten führt ein Übergang zu active 0 dazu, daß die gegenwärtig aktive Zustandsmaschine aktiv bleibt.

Wenn sie sich in active 0 befindet, wird der Variable der zweite Wert gegeben, der in dieser Ausführungsform 0 ist. Wenn der Variable der zweite Wert gegeben wird, werden die Implika­ tionen überall in der logisch bewerteten Netzliste durch jede Implikationsschaltung bestimmt. Angenommen, die Implikationen setzen sich ohne Widerspruch, dann wird GChange in den Tiefpe­ gelzustand gehen und GContra sich im Tiefpegelzustand befinden. Diese Signale erfüllen die Bedingungen, um zu passive 0 überzu­ gehen. Übergehen zu passive 0 von active 0 bewirkt eine Ausgabe von 0 für E_ol und eine Ausgabe von 1 für E_or. Die Ausgabe von 1 für E_or aktiviert die Maschine zur Rechten, die der Variable v_i+1 der nächst tieferen Ebene entspricht.

Die vorhergehenden Operationen hinsichtlich der Zustände init, active 1, passive 1, active 0 und passive 0 sind im wesentlichen dieselben wie in der oben identifizierten Ausführungsform, die chronologische Rückwärtsverarbeitung verwendet. Die Art, in der die erfindungsgemäße Ausführungsform mit nichtchronologischer Rückwärtsverarbeitung sich unterscheidet, wird nun beschrieben werden.

Es wird angenommen, daß es drei benachbarte Zustandsmaschi­ nen in einem größeren Satz von benachbarten Zustandsmaschinen gibt. Von diesen drei Maschinen entspricht die tiefste der Va­ riablen v_i; entspricht die Maschine der nächst höheren Ebene v_i-1 und entspricht die Maschine der nächsten zunehmend höheren Ebene der Variablen v_i-2. Zur Bequemlichkeit können die drei Ma­ schinen als die v_i-2-Maschine, die v_i-1-Maschine und die v_i-Ma­ schine bezeichnet werden.

Es wird angenommen, daß während der Vorwärtsberechnung v_i-2 der erste Wert 1 ohne Widersprüche zugewiesen wurde und in den passive 1-Zustand überging, und daß v_i-1 und v_i dann noch in einer freien Bedingung waren. Als die v_i-2-Maschine zu passive 1 über­ ging, gab sie E_or = 1 aus. Dieses E_or von der v_i-2-Maschine wurde durch die v_i-1-Maschine als E_il = 1 empfangen. Dieses Signal ver­ anlaßte die Maschine v_i-1 in den active 1-Zustand überzugehen, in dem der erste Wert (d. h. 1) v_i-1 zugewiesen wurde. Es wird ange­ nommen, daß die Implikationen sich ohne Widerspruch (d. h. GCon­ tra Tiefpegelzustand) entschieden (d. h. GChange Tiefpegelzu­ stand), dann ging die v_i-1 Maschine zu passive 1 über und gab, als sie überging, E_or = 1 aus. Für dieses Beispiel wird auch ange­ nommen werden, daß die Zuweisung von v_i-1 = 1 die Bedingung von v_i von frei nicht änderte.

Die v_i Maschine empfing das E_or von der v_i-1-Maschine als E_il und da v_i in einer freien Bedingung war, ging die v_i-Maschine von init zu active 1 über. In active 1 wies die v_i-Maschine den ersten Wert v_i zu (d. h. v_i = 1). Als der erste Wert v_i zugewiesen wurde, stellten die Implikationsschaltungen fest, ob die logisch be­ wertete Netzliste noch logisch konsistent war oder ob v_i = 1 einen Widerspruch lieferte. Für dieses Beispiel wird angenommen, daß v_i = 1 zu einem logischen Widerspruch führt. Folglich gab die Implikationsschaltung, die den Widerspruch detektierte, LContra = 1 aus. Dieses Signal, das, wie in Fig. 3 gezeigt, mit den anderen LContra-Signalen ODER-verknüpft wird, führte zu GContra = 1. Die v_i-Maschine ging auf das Empfangen eines hohen Wertes für GContra hin vom active 1-Zustand zum active 0-Zustand über.

In active 0 wies die v_i-Maschine den zweiten Wert v_i zu (d. h. v_i = 0). Erneut stellten die Implikationsschaltungen fest, ob diese Zuweisung einen Widerspruch lieferte. Für dieses Beispiel wird angenommen, daß v_i = 0 zu einem logischen Widerspruch führte. Mit anderen Worten führten für v_i die Zuweisung des er­ sten Wertes und des zweiten Wertes beide zu einem logischen Wi­ derspruch innerhalb der logisch bewerteten Netzliste. Um es an­ ders auszudrücken, war v_i dann eine Sperrvariable bezüglich der gegenwärtigen logisch bewerteten Netzliste. Folglich ist eine Rückwärtsverarbeitung erforderlich.

Das durch die v_i-Maschine als Reaktion auf die Zuweisung des zweiten Wertes zu v_i empfangene GContra-Signal veranlaßte die v_i-Maschine von active 0 in den leaf 1-Zustand überzugehen. Als die v_i-Maschine vom active 0 zum leaf 1-Zustand überging, gab sie E_ol = 1 und E_or = 0 aus. Im leaf 1-Zustand setzte die v_i-Maschine v_i = 1. Mit anderen Worten wurde die Sperrvariable als die Blattva­ riable gesetzt.

Die Zustände in der Zustandsmaschine werden als Hardware in der konfigurierbaren Hardware implementiert. Die Hardware, die die vorhergehenden Zustände implementiert, die zu der Identi­ fikation einer Sperrvariablen führen, und dazu, sie als eine Blattvariable zu setzen, können als ein konkretes Beispiel ei­ ner Einrichtung zum Identifizieren einer Sperrvariablen als eine Blattvariable verstanden werden.

Die E_ol = 1-Ausgabe durch die v_i-Maschine wurde durch die v_i-1-Maschine als E_ir = 1 empfangen. Die v_i-1-Maschine befand sich im passive 1-Zustand. Als die v_i-1-Maschine E_ir = 1 empfing, veran­ laßte dies die v_i-1-Maschine, in den bk 0 a Zustand überzugehen. Die v_i-1-Maschine ging in den bk 0 a-Zustand im wesentlichen zur gleichen Zeit über, als die v_i-Maschine in den leaf 1-Zustand über­ ging. Im bk 0 a-Zustand kippte die v_i-1-Maschine v_i-1 von 1 auf 0. Mit anderen Worten wies in bk 0 a die v_i-1-Maschine v_i-1 = 0 zu.

Folglich ist, wie oben erwähnt, v_i-2 = 1 und die v_i-2-Maschine befindet sich in passive 1; v_i-1 = 0 und die v_i-1 Maschine befindet sich in bk 0 a; und v_i = 1 und seine Maschine befindet sich in leaf 1. Was passiert ist, ist daß als v_i einen Widerspruch für beide möglichen Werte lieferte und folglich eine Sperrvariable bezüglich der gegenwärtigen logisch bewerteten Netzliste war, wurde v_i als die Blattvariable gesetzt. Ebenso wurde die Varia­ ble auf der nächst höheren Ebene (d. h. v_i-1) die Rückwärtsverar­ beitungsvariable. Es gab zwei Möglichkeiten, die die Rückwärts­ verarbeitungsvariable betrafen. Ihr hätte der erste Wert oder der zweite zugewiesen sein können. Da die Rückwärtsverarbei­ tungsvariable den ersten Wert aufwies, wurde die Rückwärtsver­ arbeitungsvariable zum zweiten Wert gekippt. Ebenso wurde der Blattvariable v_i der erste Wert zugewiesen.

Als v_i-1 dem zweiten Wert (v_i-1 = 0) in bk 0 a zugewiesen wurde und v_i der erste Wert zugewiesen wurde, prüften die Implikati­ onsschaltungen auf logische Konsistenz in der logisch bewerte­ ten Netzliste. Für dieses Beispiel wird angenommen werden, daß ein Widerspruch detektiert wurde und daß GContra in den Hoch­ pegelzustand ging.

Sobald GContra in den Hochpegelzustand ging, gingen die v_i-1-Ma­ schine und die v_i-Maschine über. Insbesondere ging die v_i-1-Ma­ schine in den Zustand bk 0 b über und ging die v_i-Maschine in den Zustand leaf 0 über. In bk 0 b hielt die v_i-1-Maschine die Rück­ wärtsverarbeitungsvariable v_i-1 auf dem zweiten Wert. Im leaf 0-Zu­ stand, kippte die v_i-Maschine die Blattvariable v_i auf den zweiten Wert (d. h. v_i = 0). Die Implikationsschaltungen prüften auf logische Konsistenz in der logisch bewerteten Netzliste mit der Rückwärtsverarbeitungsvariable v_i-1 auf dem zweiten Wert (d. h. 0) und der Blattvariable auf dem zweiten Wert (d. h. 0).

Für dieses Beispiel wird angenommen werden, daß ein Wider­ spruch detektiert wurde, der GContra veranlaßte, in den Hoch­ pegelzustand zu gehen. Sobald GContra in den Hochpegelzustand ging, wurden alle drei Maschinen beeinflußt.

Insbesondere ging die v_i-Maschine von leaf 0 zurück zu leaf 1, was folglich zu v_i = 1 führt. Das heißt, die Blattvariable be­ hielt dieselbe Identität, änderte jedoch ihren Wert auf die Detektion des Widerspruches hin.

Die v_i-1-Maschine ging von bk 0 b auf init über. Als sie über­ ging, gab sie E_ol = 1 und E_or = 0 ab. In init wurde die Variable v_i-1 auf die freie Bedingung gesetzt.

Die E_ol = 1-Ausgabe durch die v_i-1-Maschine wurde durch die v_i-2-Maschine als E_ir = 1 empfangen. Diese Eingabe in die v_i-2-Ma­ schine verursachte einen Übergang von passive 1 zu bk 0 a. Mit anderen Worten wurde die Variable v_i-2 die Rückwärtsverarbei­ tungsvariable. In bk 0 a wurde der Wert von v_i-2 auf den zweiten Wert (d. h. 0) gesetzt.

Folglich befand sich die v_i-2-Maschine dann im Zustand bk 0 a mit v_i-2 = 0; befand sich die v_i-1 Maschine dann im init-Zustand mit v_i-1 in einer freien Bedingung; und befand sich die v_i-Ma­ schine dann im leaf 1-Zustand mit v_i = 1. Es wird beachtet werden, daß, als v_i-1 die Rückwärtsverarbeitungsvariable war und dem zweiten Wert zugewiesen war, und als Widersprüche für beide Werte der Blattvariable v_i detektiert wurden, die Bedingung der Rückwärtsverarbeitungsvariable auf frei gesetzt wurde, und daß die Identität der Rückwärtsverarbeitungsvariable auf die Varia­ ble v_i-2 der nächst höheren Ebene gesetzt wurde.

An dieser Stelle prüften die Implikationsschaltungen auf Widersprüche in der logisch bewerteten Netzliste mit v_i-2 = 0; v_i-1 frei; und v_i = 1. Für dieses Beispiel wird angenommen werden, daß kein Widerspruch detektiert wurde. Folglich blieb, sobald sich alle der Implikationen setzten (d. h. GChange in den Tief­ pegelzustand ging), das Signal GContra im Tiefpegelzustand.

Mit sowohl GChange als auch GContra im Tiefpegelzustand wur­ den die drei Maschinen wie folgt beeinflußt. Die v_i-2-Maschine ging von bk 0 a zu passive 0 über. Als sie überging, gab sie E_ol = 0 und E_or = 1 aus. Es wird aus Fig. 5 deutlich, daß dann, wenn die Kontrolle an die v_i-2-Maschine zurückgeht, die v_i-2-Maschine zum init-Zustand übergehen wird und die Kontrolle an die nächst höhere Ebene übergeben wird. Dies ist in Einklang mit dem oben identifizierten nichtchronologischen Rückwärtsverarbeitungs­ verfahren. Wenn v_i-2 die Rückwärtsverarbeitungsvariable wird und sie schon den zweiten Wert aufweist (d. h. v_i-2 ist schon auf 0 gesetzt), dann soll keine weitere Prüfung auf der v_i-2-Ebene ge­ schehen und die Prüfung muß auf einer höheren Ebene weitergehen. Im vorliegenden Beispiel bleibt jedoch die v_i-2-Maschine auf pas­ sive 0.

Als sowohl GChange als auch GContra in den Tiefpegelzustand gingen, wurde die v_i-1-Maschine ebenfalls beeinflußt. Insbeson­ dere war die v_i-1-Maschine im init-Zustand mit der Variable v_i-1 in der freien Bedingung (d. h. kein implizierter Wert) gewesen. An­ genommen, daß kein Wert für v_i-1 durch die letzte Prüfung auf Widersprüche durch die Implikationsschaltungen impliziert wor­ den war, dann wurde die v_i-1 Maschine zu active 1 übergehen.

Als sowohl GChange als auch GContra in den Tiefpegelzustand gingen, wurde die v_i-Maschine ebenfalls beeinflußt. Insbesondere ging die v_i-Maschine vom leaf 1-Zustand mit v_i = 1 in den init-Zu­ stand über. Im init-Zustand wurde die Variable v_i auf die freie Bedingung gesetzt.

Die Hardware-Implementierung der leaf 1- und leaf 0-Zustände kann man sich als ein konkretes Beispiel einer Einrichtung zum Variieren des Wertes der Blattvariablen vorstellen. Die Hard­ ware-Implementierung der bk 0 a- und bk 0 b-Zustände in der näch­ sten Zustandsmaschine darüber von der Zustandsmaschine, die die Blattvariable führt, kann entsprechend als eine Einrichtung zum Setzen und Variieren einer ersten Rückwärtsverarbeitungsvaria­ ble auf einer Ebene, die höher als eine Ebene der Blattvariable ist, verstanden werden. Desgleichen kann die Hardware-Implemen­ tierung der bk 0 a- und bk 0 b-Zustände in der nächsten Zustands­ maschine darüber von der Zustandsmaschine mit der ersten Rück­ wärtsverarbeitungsvariable als eine Einrichtung zum Setzen und Variieren einer zweiten Rückwärtsverarbeitungsvariable, wenn die erste Rückwärtsverarbeitungsvariable einen logischen Wider­ spruch erzeugt, verstanden werden.

Wie das vorhergehende Beispiel darstellt, sorgt diese Aus­ führungsform der Erfindung für eine nichtchronologische Rück­ wärtsverarbeitung unter Verwendung rekonfigurierbarer Hard­ ware.

Abhängig von den Problemeigenschaften, kann die konfigu­ rierbare Berechnungsimplementierung häufig eine beträchtliche Beschleunigung gegenüber einer Software-SAT-Lösungsvorrichtung bieten, und die Hardware-Lösungsvorrichtung mit nichtchronolo­ gischer Rückwärtsverarbeitung kann eine zusätzliche Beschleu­ nigung gegenüber der Hardware-Lösungsvorrichtung mit chronolo­ gischer Rückwärtsverarbeitung bieten.

Damit die Beschleunigung nützlich ist, muß sie jedoch Lei­ stungsvorteile selbst dann bieten, nachdem die Hardware-Kompi­ lierungszeit und Konfigurationszeit berücksichtigt wird. Aus diesem Grund ist es zu empfehlen, daß die konfigurierbaren Hard­ ware-Techniken hauptsächlich bei SAT-Problemen mit sehr langen GRASP-Laufzeiten (Stunden oder Tage) oder in Fällen verwendet werden, wo GRASP abbricht. In solchen Fällen werden die erfor­ derlichen Hardware-Synthesezeiten akzeptabel sein.

Allgemein wird ein System ins Auge gefaßt, wo leichte SAT-Pro­ bleme noch in Software gelöst werden; sehr große Probleme, d. h. diejenigen, die häufig wegen Zeitüberschreitung abbrechen, werden den Hardware-Kompilierer und eine FPGA-Schaltplatte zu Hilfe rufen, die dabei helfen sollen, diese Probleme zu lösen.

Die ins Auge gefaßte Hardware-Plattform ist eine Hochlei­ stungs-Workstation mit einer FPGA-Schaltplatte, die über eine externe Verbindung oder den I/O-Bus angeschlossen ist. Leicht zu lösende Probleme werden durch Software bearbeitet, die auf der Workstation selbst läuft, während länger laufende Probleme durch die FPGA-Schaltplatte bearbeitet werden. Die Anforderun­ gen für die FPGA-Schaltplatte selbst sind teilweise eine Funk­ tion der Hardwaregröße der Probleme, die gelöst werden; dies wird im folgenden Teilabschnitt erläutert.

Die Hardware-Anforderungen für das erfinderische Verfahren sind eine Funktion der Größe und Komplexität der Formel, die gelöst wird. Die auf Schablonen beruhende Gestaltung zum SAT-Lösen gemäß der Erfindung erfordert weder einen Speicher noch werden irgendwelche Eingabedaten vor oder während der Problem­ lösung zugeladen. Statt dessen wird das ganze Problem in die kon­ figurierbaren Logikblöcke (CLBs) der FPGA eingebettet.

Die CLB-Anforderungen der SAT-Lösungsvorrichtung variieren natürlicherweise mit der zu lösenden Formel weit. Quer durch die DIMACS-Leistungsvergleiche betragen die mittleren CLB-An­ forderungen 3655. Allgemein werden verhältnismäßig wenige (we­ niger als 30%) dieser Probleme in die CLB-Grenzen von 1000 oder 2000 der gegenwärtigen FPGA-Chips passen (für nähere Einzelhei­ ten betreffend FPGA-Chips, siehe das folgende nützliche Hinter­ grunddokument, das hierin als Verweisquelle aufgenommen wird:
The Programmable Logic Data Book, Xilinx Corp. San Jose, CA, 1994). Die meisten jedoch werden auf weniger als zehn FPGAs pas­ sen.

Die Verteilung der Gestaltung über die FPGAs ist wegen der verwendeten regulären Topologie unkompliziert. Bei den Experi­ menten haben die Erfinder die Verteilungs- und Stiftmultiplex­ techniken im IKOS SLI Logikemulationssystem verwendet, das ur­ sprünglich als Teil der MIT-Virtual-Wires-Bemühung entwickelt wurde. Für weitere Informationen über die MIT-Virtual-Wires-Be­ mühung, siehe bitte das folgenden Dokument, das wegen seiner Hintergrundinformation als Verweisquelle aufgenommen wird:

• - J. Babb, R. Tessier, und A. Agarwal. Virtual Wires: Over­ coming pin limitations in FPGA-based logic emulators.
  In Proceeding & IEEE Workshop on FPGA-based Custom Compu­ ting Machines, Seiten 142-151, Apr. 1993.

Diese Verteilungs-Software kann mehrere Zwischen-Chipsi­ gnale multiplexen, um dieselben physikalischen Stifte zu ver­ wenden, wodurch die Stiftbegrenzungen umgangen werden, die häu­ fig die CLB-Nutzung von FPGA-Gestaltungen begrenzen. Ferner führt die Software dieses Multiplexen mit minimalem Einfluß auf die Hardware-Zykluszeiten aus.

Allgemein stellt die Erfindung mehrere wichtige Beiträge bereit. Erstens wird eine Systemgestaltung für formelspezifi­ sche Boolesche Erfüllbarkeitslösungen beruhend auf einer kon­ figurierbaren Hardware-Implementierung bereitgestellt. Die Hardwareanforderungen der neuartigen Gestaltung sind ziemlich bescheiden. Überdies zeigen die Leistungsergebnisse der erfin­ dungsgemäßen Hardware an, daß das konfigurierbare Hardware-Ver­ fahren das Potential für dramatische Verbesserungen gegenüber selbst den besten gegenwärtigen auf Software beruhenden Tech­ niken aufweist.

Die Erfindung stellt auch ein neuartiges Verfahren zur nichtchronologischen Rückwärtsverarbeitung bereit, das in kon­ figurierbarer Hardware implementiert werden kann. Jedoch kann die erfindungsgemäße nichtchronologische Rückwärtsverarbeitung auch auf andere Arten implementiert werden. Zum Beispiel kann es in einem Computersystem ohne konfigurierbare Hardware imple­ mentiert werden. Das heißt, ein Computersystem, das die Erfin­ dung ausführt, wird Hardware und Software enthalten, die es ihm ermöglichen, das nichtchronologische Rückwärtsverarbeitungs­ verfahren auszuführen.

Entsprechend kann die oben identifizierte Erfindung in ei­ nem Computerprogrammprodukt ausgeführt werden, wie nun erläu­ tert werden wird.

Auf einer praktischen Ebene wird die Software, die es dem Computersystem ermöglicht, das oben identifizierte Verfahren und die Operationen der Erfindung auszuführen, auf irgendeinem einer Vielzahl von Medien geliefert. Die Software kann insbe­ sondere ein System betreffen, das konfigurierbare Hardware auf­ weist, oder eines ohne konfigurierbare Hardware. Im erstgenann­ ten Fall wird die Software Konfigurationsanweisungen einschlie­ ßen.

Ferner kann die tatsächliche Implementierung des Verfahrens und der Operationen der Erfindung tatsächlich aus Anweisungen bestehen, die in einer Programmiersprache geschrieben werden. Solche Programmiersprachen-Anweisungen veranlassen, wenn sie durch einen Computer ausgeführt werden, den Computer, gemäß dem bestimmten Inhalt der Anweisungen zu arbeiten. Ferner kann die Software, die es einem Computersystem ermöglicht, erfindungs­ gemäß zu arbeiten, in jeder Zahl von Formen bereitgestellt wer­ den, die ursprünglichen Quellcode, Assemblercode, Objektcode, Maschinensprache, komprimierte oder verschlüsselte Versionen des Vorhergehenden, und alle und jede Äquivalente einschließen, aber nicht auf sie begrenzt sind.

Ein Fachmann wird erkennen, daß "Medien" oder "computerles­ bare Medien", wie sie hier verwendet werden, eine Diskette, ein Band, eine Compact-Disk, eine integrierte Schaltung, eine Kas­ sette, eine Fernübertragung über eine Kommunikationsschaltung oder jedes andere ähnliche Medium, das durch Computer verwend­ bar ist, einschließen kann. Zum Beispiel kann der Lieferant, um Software zu liefern, um es einem Computersystem zu ermöglichen, erfindungsgemäß zu arbeiten, eine Diskette bereitstellen oder er könnte die Software in einer gewissen Form über Satelliten­ übertragung, über eine direkte Telephonverbindung oder über das Internet übertragen.

Obwohl die ermöglichende Software "auf" eine Diskette "ge­ schrieben", einer integrierten Schaltung "gespeichert", oder "über" eine Kommunikationsschaltung "übertragen" werden könnte, wird erkannt werden, daß für die Zwecke dieser Anwendung das computerverwendbare Medium als die Software "tragend" be­ zeichnet wird. Folglich wird beabsichtigt, daß der Ausdruck "tragend" die obigen und alle äquivalenten Arten umfaßt, in der Software mit einem computerverwendbaren Medium verbunden ist.

Der Einfachheit halber wird daher der Ausdruck "Programm­ produkt" folglich verwendet, um ein computerverwendbares Medium zu bezeichnen, wie oben definiert, das in irgendeiner Form Soft­ ware trägt, um es einem Computersystem zu ermöglichen, entspre­ chend der oben identifizierten Erfindung zu arbeiten. Folglich wird die Erfindung auch in einem Programmprodukt ausgeführt, das Software trägt, die es einem Computer ermöglicht, das oben beschriebene erfindungsgemäße nichtchronologische Rückwärts­ verarbeitungsverfahren auszuführen.

Claims (10)

1. Konfigurierbare Vorrichtung zur Lösung eingegebener Such­ probleme, die aufweist:
einen Speicher, der Konfigurationsanweisungen aufweist;
ein Hardware-System, das gemäß den Konfigurationsanweisun­ gen konfigurierbar ist;
wobei die Konfigurationsanweisungen das Hardware-System konfigurieren, um eine Suche beruhend auf einem gegenwär­ tigen der eingegebenen Suchprobleme auszuführen; und
die Konfigurationsanweisungen das Hardware-System so kon­ figurieren, daß für jedes der eingegebenen Suchprobleme eine Rückwärtsverarbeitung, die während der Suche durchgeführt wird, nichtchronologische Rückwärtsverarbeitung unter Steuerung des Hardware-Systems einschließt.

2. Konfigurierbare Vorrichtung nach Anspruch 1, wobei die ein­ gegebenen Suchprobleme auf Boolesche Erfüllbarkeits(SAT-)­ Probleme reduziert werden, und wobei die Konfigurationsan­ weisungen das Hardware-System so konfigurieren, daß für die Booleschen SAT-Probleme die Suche eine Booleschen SAT-Lö­ sungssuche mit der nichtchronologischen Rückwärtsverarbei­ tung ist.

3. Konfigurierbare Vorrichtung nach Anspruch 2, wobei die Kon­ figurationsanweisungen das Hardware-System konfigurieren, um zu definieren:
Einrichtungen zum Identifizieren einer Sperrvariable als eine Blattvariable;
Einrichtungen zum Variieren des Wertes der Blattvariablen;
Einrichtungen zum Setzen und Variieren einer ersten Rück­ wärtsverarbeitungsvariablen auf einer Ebene, die höher als eine Ebene der Blattvariablen ist; und
Einrichtungen zum Setzen und Variieren einer zweiten Rück­ wärtsverarbeitungsvariablen auf einer Ebene, die höher als die Ebene der ersten Rückwärtsverarbeitungsvariablen ist, wenn die erste Rückwärtsverarbeitungsvariable einen logi­ schen Widerspruch erzeugt.

4. Verfahren zur nichtchronologischen Rückwärtsverarbeitung einer Netzliste von Variablen, das aufweist:
Identifizieren einer Sperrvariablen als eine Blattvariable; Variieren des Wertes der Blattvariablen;
Setzen als eine erste Rückwärtsverarbeitungsvariable einer Variablen mit einer Ebene, die höher als die Ebene der Blattvariablen ist, und Variieren des Wertes der ersten Rückwärtsverarbeitungsvariablen;
Auswerten der Netzliste auf logische Konsistenz beruhend auf dem Wert der Blattvariablen und dem Wert der ersten Rück­ wärtsverarbeitungsvariablen;
wenn die Auswertung einen logischen Widerspruch erzeugt, Va­ riieren einer Rückwärtsverarbeitungsvariablenidentität durch Setzen als eine zweite Rückwärtsverarbeitungsvariable einer anderen der Variablen mit einer Ebene, die höher als die Ebene der ersten Rückwärtsverarbeitungsvariablen ist, und Variieren des Wertes der anderen Rückwärtsverarbei­ tungsvariablen; und dann
Auswerten der Netzliste auf logische Konsistenz beruhend auf dem Wert der Blattvariablen und dem Wert der zweiten Rück­ wärtsverarbeitungsvariablen.

5. Nichtchronologisches Rückwärtsverarbeitungsverfahren zum Bestimmen einer erfüllenden Variablenzuweisung für eine Konjunktivnormalform- (CNF-) Darstellung eines Satzes Boolescher Formelvariablen, die in Ebenen geordnet sind, wo­ bei jede der Variablen eine jeweilige Ebene aufweist, der Satz Variablen eine logisch bewertete Netzliste definiert, wobei das Verfahren aufweist:
Identifizieren einer Sperrvariablen als eine Blattvariable, und Variieren des Wertes der Blattvariablen;
Setzen als eine erste Rückwärtsverarbeitungsvariable einer der Variablen mit einer Ebene, die höher als die Ebene der Blattvariablen ist, und Variieren des Wertes der ersten Rückwärtsverarbeitungsvariablen;
paralleles Auswerten der logisch bewerteten Netzliste auf logische Konsistenz beruhend auf dem Wert der Blattvariablen und dem Wert der ersten Rückwärtsverarbeitungsvariablen;
als Reaktion darauf, daß die Auswertung einen logischen Wi­ derspruch erzeugt, Variieren einer Rückwärtsverarbeitungs­ variablen-Identität durch Setzen als eine zweite Rückwärts­ verarbeitungsvariable, eine andere der Variablen mit einer Ebene, die höher als die Ebene des ersten Rückwärtsverar­ beitungsvariablen ist, und Variieren des Wertes der anderen Rückwärtsverarbeitungsvariablen;
paralleles Auswerten der logisch bewerteten Netzliste auf logische Konsistenz beruhend auf dem Wert der Blattvariablen und dem Wert der zweiten Rückwärtsverarbeitungsvariablen.

6. Nichtchronologisches Rückwärtsverarbeitungsverfahren zum Bestimmen einer erfüllenden Variablenzuweisung für eine Konjunktivnormalform- (CNF-) Darstellung eines Satzes Boolescher Formelvariablen, die in jeweiligen Ebenen geord­ net sind und Definieren einer logisch bewerteten Netzliste, wobei das Verfahren aufweist:

• (a) Variieren bezüglich einer Blattvariablen nur eines Blattvariablenwertes, wobei der Blattwert beruhend auf einer Sperrvariablen bestimmt wird;
• (b) Variieren bezüglich einer Rückwärtsverarbeitungsvaria­ blen einer Rückwärtsverarbeitungsvariablenidentität und eines Rückwärtsverarbeitungsvariablenwertes, wobei die Rückwärtsverarbeitungsvariable eine höhere Ebene als jene der Blattvariablen aufweist; und
• (c) paralleles Auswerten der logisch bewerteten Netzliste auf logische Konsistenz beruhend auf dem Blattvaria­ blenwert, dem Rückwärtsverarbeitungsvariablenwert und der Rückwärtsverarbeitungsvariablenidentität.

7. Nichtchronologisches Rückwärtsverarbeitungsverfahren nach Anspruch 6, wobei der Auswerteschritt aufweist:
Bereitstellen einer geordneten Mehrzahl von Zustandsmaschi­ nen, wobei jede einer der Booleschen Formelvariablen ent­ spricht und identisch damit geordnet ist;
für jede der mehreren Zustandsmaschinen, Bereitstellen ei­ ner Implikationsschaltung;
Kombinieren der Ausgabe jeder Implikationsschaltung, um ein globales Widerspruchssignal bereitzustellen, das anzeigt, daß die logisch bewertete Netzliste nicht logisch konsistent ist.

8. Nichtchronologisches Rückwärtsverarbeitungsverfahren nach Anspruch 7, wobei der Kombinationsschritt ferner das Be­ reitstellen eines globalen Änderungssignals aufweist, das anzeigt, ob alle transitiven Implikationen der logisch be­ werteten Netzliste bestimmt worden sind.

9. Computersystem, das angepaßt ist, um eine erfüllende Varia­ blenzuweisung für eine Konjunktivnormalform- (CNF-) Dar­ stellung eines Satzes Boolescher Formelvariablen zu bestim­ men, die in jeweiligen Ebenen geordnet sind und eine logisch bewertete Netzliste definieren, wobei das System aufweist:
einen Prozessor, und
einen Speicher, der Software-Anweisungen aufweist, die an­ gepaßt sind, es dem Computersystem zu ermöglichen, die Schritte auszuführen:

• (a) Variieren bezüglich einer Blattvariablen nur eines Blattvariablenwertes, wobei der Blattwert beruhend auf einer Sperrvariablen bestimmt wird;
• (b) Variieren bezüglich einer Rückwärtsverarbeitungsvaria­ blen einer Rückwärtsverarbeitungsvariablenidentität und eines Rückwärtsverarbeitungsvariablenwertes, wobei die Rückwärtsverarbeitungsvariable eine höhere Ebene als jene der Blattvariablen aufweist; und
• (c) paralleles Auswerten der logisch bewerteten Netzliste auf logische Konsistenz beruhend auf dem Blattvaria­ blenwert, dem Rückwärtsverarbeitungsvariablenwert und der Rückwärtsverarbeitungsvariablen-Identität.

10. Computerprogrammprodukt, um es einem Computer zu ermögli­ chen, eine erfüllende Variablenzuweisung für eine Konjunk­ tivnormalform- (CNF-) Darstellung eines Satzes von Boole­ schen Formelvariablen zu bestimmen, die in jeweiligen Ebenen geordnet sind und eine logisch bewertete Netzliste definie­ ren, wobei das Produkt aufweist:
Software-Anweisungen, um es dem Computer zu ermöglichen, vorherbestimmte Operationen auszuführen, und
ein computerlesbares Medium, das die Software-Anweisungen trägt;
wobei die vorherbestimmten Operationen die Schritte aufwei­ sen:

• (a) Variieren bezüglich einer Blattvariablen nur eines Blattvariablenwertes, wobei der Blattwert beruhend auf einer Sperrvariablen bestimmt wird;
• (b) Variieren bezüglich einer Rückwärtsverarbeitungsvaria­ blen einer Rückwärtsverarbeitungsvariablenidentität und eines Rückwärtsverarbeitungsvariablenwertes, wobei die Rückwärtsverarbeitungsvariable eine höhere Ebene als jene der Blattvariablen aufweist; und
• (c) paralleles Auswerten der logisch bewerteten Netzliste auf logische Konsistenz beruhend auf dem Blattvaria­ blenwert, dem Rückwärtsverarbeitungsvariablenwert und der Rückwärtsverarbeitungsvariablen-Identität.