Clause satisfiability status.
Formula satisfiability status.
Applies the negation to value depending on the sign of lit.
Returns the value of the literal as found in model.
Formula level propagation until fixed point.
Formula level propagation until fixed point.
the formula to run propagation on
A pair (result, model), the model can be inconsistent with formula if status is FUnsat
Clause level propagation.
Formula level single pass of propagation to detect status and units.
Very naive implementation of a unit propagation routine only meant to test propagation properties of clausal encodings for small problems/operators. Performance is not an issue, correctness is however required.