0
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$
    – Ariel
    Apr 9, 2018 at 3:41
  • $\begingroup$ @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. $\endgroup$
    – Matt
    Apr 9, 2018 at 5:48
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kyle Jones
    Apr 9, 2018 at 18:06
  • $\begingroup$ 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. $\endgroup$
    – Matt
    Apr 9, 2018 at 18:49
  • $\begingroup$ So your question is whether adding DON'T-CAREs to the problem puts circuit minimization decision problems into NP? $\endgroup$
    – Kyle Jones
    Apr 9, 2018 at 19:49

1 Answer 1

Reset to default
2
$\begingroup$

This problem is known as circuit minimization. It falls within the broad area of logic synthesis.

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.

Anyway, there is a lot of literature on circuit minimization. As far as I know, one standard approach is to use techniques built on Quine-McClusky, Espresso, etc.

You might be interested in approaches based on interpolation. I believe those approaches use a SAT solver as a building block.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.