Crate varisat_utils

Functions

add_at_most_one

Adds a clause requiring at most one input variable to be true This uses the same efficient encoding as the commander

add_exactly_one

Adds a clause requiring exactly one input variable to be true This uses the same efficient encoding as the commander

commander_exactly_one

Returns a literal that is true if exactly one of the input variables is true This uses an efficient encoding from https://www.cs.cmu.edu/~wklieber/papers/2007_efficient-cnf-encoding-for-selecting-1.pdf

exactly_k