It sounds like you are trying to solve a partial maxsat problem. Partial maxsat uses two sets of clauses, hard and soft clauses. The hard clauses must be satisf

It sounds like you are trying to solve a partial maxsat problem. Partial maxsat uses two sets of clauses, hard and soft clauses. The hard clauses must be satisfied and the soft clauses are "nice to haves." The goal for the solver is to satisfy all the hard clauses and as many as the soft clauses as possible. Pysat is a python package for that provides efficient SAT solver APIs and encodings, including a partial maxsat solver. https://pysathq.github.io/docs/html/index.html https://pysathq.github.io/docs/html/index.html RC2 partial maxsat algorithm: https://pysathq.github.io/docs/html/api/examples/rc2.html https://pysathq.github.io/docs/html/api/examples/rc2.html