Huub is a Lazy Clause Generation (LCG) solver with a focus on modularity and
maintainability in addition to speed. LCG solvers are a class of solvers that
can be used to solve decision and optimization problems. They are characterized
by their ability to dynamically add new Boolean variables and clauses to a
Boolean Satisfiability (SAT) solver during the search process. This allows the
solver to exploit SAT solver's ability to learn from failures during the search
process, without having to encode the full problem into Boolean variables and
clauses.