Constraint-Programmierung (Bsp: SAT)

Programm (aussagenlogische F. in konjunktiver NF):

(x₁∨x₂)∧(x₂∨x₃)∧($\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 x₁ = True, x₂ = False, x₃ = 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/