| | 22 | |
| | 23 | === Translation to Propositional Formulas === |
| | 24 | |
| | 25 | SAT-solvers for propositional formulas can be very fast and compact as demonstrated by miniSAT (600 SLOC of C++ code). To be able to use them, however, we need to be able to express our problem in a form that can be solved by miniSAT, though. |
| | 26 | |
| | 27 | A SAT-solver accepts ''clauses'' as input. A clause is a disjunction of possibly negated variables. A propositional variable can either be true or false. The goal of the SAT-solver is to find an assignments to for each variable that makes all clauses true. |
| | 28 | |
| | 29 | Say we have the following versions of the package {{{bar}}} available: |
| | 30 | {{{ bar-1.2, bar-1.2.3, bar-1.3, bar-1.4 }}} |
| | 31 | Then the constraint {{{bar > 1.2 }}} can be expressed as {{{bar == 1.2.3 || bar == 1.3 || bar == 1.4}}}. We can translate this into propositional variables: |
| | 32 | {{{ |
| | 33 | not <bar-1.2>, <bar-1.2.3>, <bar-1.3>, <bar-1.4> |
| | 34 | }}} |
