# How to find a nearly-optimal covering of a set using SAT?

I have recently started thinking about application of SAT in solving different problems and how I can encode those problems into a SAT problem.

I think one of the interesting problems where SAT solvers can be used is finding a minimal representation for a logic expression. However, I have trouble encoding the problem into a SAT problem.

In very old representations of an n-input logic circuit, three sets F, R, and D are defined. F represents the ON-set, which corresponds to permutations of input that cause a one in the output. R is the OFF-set, which corresponds to permutations of input that cause a zero in the output. Finally, D is the DON'T CARE-set which corresponds to permutations of input where output is not specified (could be set to either one or zero during optimization).

The objective is to find a minimal conjunctive normal form (CNF) that has the minimum number of clauses and each clause has the minimum number of literals. This CNF should cover all elements of F and may potentially cover some elements of D, but should not cover any elements of R.

For example, assume that a 3-input function is defined in the following way:

A B C | Y
---------
0 0 0 | 0
0 0 1 | 0
0 1 0 | 1
0 1 1 | 1
1 0 0 | -
1 0 1 | -
1 1 0 | -
1 1 1 | -


where A, B, and C are inputs, Y is the output, and a - determines a don't care output.

In this problem, a minimal CNF that meets the objective is O = B, because whenever B is true, the output is either true or don't care, but never false. Without having the DON'T CARE-set, a minimal representation would be O = ~A B, but DON'T CARE-set has allowed a more compact representation.

Is there a method to encode this problem as a SAT problem where inputs are F and R?

• The optimality condition is not very clear here. Consider two formulas, one with 3 clauses but two literals in each clause and the other with 2 clauses but 3 literals in each clause, which is minimal? It makes more sense to talk about minimal encoding length relative to some fixed agreed upon representation. – Ariel Apr 9 '18 at 3:41
• @Ariel Some people try to minimize the total literal count when it comes to Boolean logic minimization. In that case, your examples will have the same cost. I personally think that a balanced solution in terms of number of clauses and literals per clause is probably superior. For example, if 16 literals are required, 4 clauses of 4 literals each is probably better than 8 clauses of 2 literals each. Anyway, a solution that works on any of these cost functions is appreciated. – Mahdi Apr 9 '18 at 5:48
• Could you explain in your question why normal circuit minimization algorithms aren't sufficient? E.g. treat the DON'T-CAREs as zeroes, apply Quine-McCluskey, then de Morgan's laws. – Kyle Jones Apr 9 '18 at 18:06
• Because treating DON'T CAREs as zeros will not lead to an optimal solution as I have explained in my example. Additionally, Quine-McCluskey is know to be terribly slow. – Mahdi Apr 9 '18 at 18:49
• So your question is whether adding DON'T-CAREs to the problem puts circuit minimization decision problems into NP? – Kyle Jones Apr 9 '18 at 19:49

The problem is known to be $\Sigma_2^P$-complete. As a result, it is unlikely to be in NP (contrary to what you wrote). And that means that it is unlikely to be solvable in polynomial time with queries to a SAT solver. (NP is basically the class of problems you can solve with a SAT solver in a single query; $P^{NP}$ is the class of problems you can solve with an unlimited number of queries to a SAT solver; and $\Sigma_2^P$ is conjectured to be larger still, so a $\Sigma_2^P$-complete problem is conjectured not to be in NP or $P^{NP}$.) There may still be heuristics that use a SAT solver along the way, but these heuristics either might make mistakes, might fail for some inputs, or might take exponentially long in some cases.