# Translation to SAT

## Finding A1 via compilation:

`Selected (boolean) functions`

: restrict to some “interesting” selection**s(v)**⊆ BF^{ D v }, and treat the elements of s(v) as the possible values of v.`Admissible partial assignment`

: For each C ∈ F , compile all possibilities for admissible partial satisfying assignments for C into some CNF-representation**P(C)**.