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
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
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 | -
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