Crate varisat_utils

Crate varisat_utils 

Source

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