Constraint-Programmierung (Bsp: SAT)

Programm (aussagenlogische F. in konjunktiver NF):

(x1x2)∧(x2x3)∧($ \overline{x}_{1}^{}$$ \overline{x}_{2}^{}$$ \overline{x}_{3}^{}$) mathend000#

textuelle Syntax:

p cnf 3 3
1 2 0   2 3 0   -1 -2 -3 0

(ausführen mit minisat f.cnf /dev/stdout)

Antwort (erfüllende Belegung):

SAT    1 -2 3 0
ist Notation für x1 = True, x2 = False, x3 = True mathend000#

SAT ist NP-vollständig, aber es gibt Verfahren, die in erstaunlich vielen Fällen Lösungen schnell finden.

siehe http://minisat.se/



Johannes Waldmann 2014-03-31