integer constraints

[Jan Bruns]

Ganz kurz+kompakt was zum Thema (integer) constraint solving:


Ein schönes Beispiel dafür,
1.) warum "selects" (s.u.) Klauseln überlegen sind und
2.) wann inverse Implikationen Klauseln so richtig helfen

und irgendwie indirekt auch:
3.) warum es nicht gut ist, integer-constraints
in boolean zu wandeln (als Folgerung aus 1.,
zumindest sehe ich nicht, wie man "selects"
aus dem Ausgangsproblem dann noch nativ im
boolean solver unterstützen könnte)



Example:
========

+ : allowed combination
# : disallowed combination

r
123456789

1 +#+++++++
2 +#+++++++
3 +#+++++++
4 +#+++++++
5 #+#######
v 6 +#+++++++
7 +#+++++++
8 +#+++++++
9 +#+++++++



the missing vectors:

v,r

1,2 ###
2,2 ###
3,2 ###
4,2 ###
5,1 ###
5,3 ###
5,4 ###
5,5 ###
5,6 ###
5,7 ###
5,8 ###
5,9 ###
6,2 ###
7,2 ###
8,2 ###
9,2 ###

assume propagation has deactivated
all values for v, except 7 and 8.

A "select" (a complete list of allowed combinations
over a given set of variables) would notice that it
doesn't have any active vectors for r=2 in this case.

The clauses (7,2) and (8,2) however wouldn't deactivate
r=2 in normal propagation, because v isn't fully
decided.

To become more specific, the given example doesn't
allow r=2 without v=5. So we'd like to see propagation
to deactivate r=2 when v=5 is deactivated somehow.

This can't be directly expressed using clauses, but
solver implementations might allow tied symbol
deactivation. In conflict analysis, tied deactivates
can be recursively resolved until a totally forced
variable is found.

Symbols to tie can be found in polynomal time
by scanning the problem for first-order implications.

In the given example, r=2 implies v=5, so we can always
deactivate r=2 whenever v=5 is assumed to be disallowed.


Gruss

Jan Bruns


--
Ein paar Fotos: http://abnuto.de/gal/

[Jan Bruns]

Jan Bruns:

> Ganz kurz+kompakt was zum Thema (integer) constraint solving:

Falls es wen interessieren sollte, hier eine Implementation dazu (1.2MB):

http://abnuto.de/jan/code/sypromedor/sypromedor.zip

Enthalten sind der eigentlich noch so gar nicht vorzeigbare Quelltext
(freepascal), vorcompilierte binaries (bitte nur in VMs verwenden) für
win32 und linux64, einige Problembeispieldateien für die
Beispielprobleme "boolean cnf" und "sudoku".

Etwas schade ist, daß die momentan einzige integer-Problemstellung
das sudoku ist, was nun constraint-technisch so einfach ist, daß
man da mit DPLL-assoziierten Lösungsstrategieen (Auswahl-Strategie)
rangehen will, die nun gerade mit diesem Aufbau nur grottenlangsam
quasi emuliert werden können.

Boolean cnf performance ist mässig. Konkret immerhin etwa so, daß bei
der SAT-competition09 in der crafted-Kathegorie zumindest so einige
preprocessing-points zu sehen sind.

Momentan ist der Schwachpunkt wohl die Konflikanalyse. Es wird
immer nur eine Klausel gelernt, und zwar die kürzere von den beiden
Varianten "deciroots" und "first UIP". Bin erstmal froh, daß das
so auch zusammen mit selects und integers funktioniert.

[Jan Bruns]

Jan Bruns:

Sorry, link falsch: http://abnuto.de/jan/code/sypromedor/

Schaut euch mal das neue Dateiformat an.

Wollte man nicht schon immer lieber so mit solvern reden?
Ich finds jedenfalls irgendwie angenehm.

Und selbst wenn man nur knf codiert gibt das durch die bessere
Ausnutzung des Zeichensatzes sicherlich kürzere Dateien.

So, ich beende dann mal diesen Monolog.