How to find a nearly-optimal covering of a set using SAT? - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-09-18T13:47:19Z https://cs.stackexchange.com/feeds/question/90428 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cs.stackexchange.com/q/90428 0 How to find a nearly-optimal covering of a set using SAT? Mahdi https://cs.stackexchange.com/users/57456 2018-04-09T01:32:56Z 2018-04-11T06:54:22Z <p>I have recently started thinking about application of SAT in solving different problems and how I can encode those problems into a SAT problem.</p> <p>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.</p> <p>In very old representations of an <em>n</em>-input logic circuit, three sets <code>F</code>, <code>R</code>, and <code>D</code> are defined. <code>F</code> represents the ON-set, which corresponds to permutations of input that cause a one in the output. <code>R</code> is the OFF-set, which corresponds to permutations of input that cause a zero in the output. Finally, <code>D</code> 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).</p> <p>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 <code>F</code> and may potentially cover some elements of <code>D</code>, but should not cover any elements of <code>R</code>.</p> <p>For example, assume that a 3-input function is defined in the following way:</p> <pre><code>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 | - </code></pre> <p>where <code>A</code>, <code>B</code>, and <code>C</code> are inputs, <code>Y</code> is the output, and a <code>-</code> determines a don't care output.</p> <p>In this problem, a minimal CNF that meets the objective is <code>O = B</code>, 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 <code>O = ~A B</code>, but DON'T CARE-set has allowed a more compact representation.</p> <p>Is there a method to encode this problem as a SAT problem where inputs are <code>F</code> and <code>R</code>?</p> https://cs.stackexchange.com/questions/90428/-/90523#90523 2 Answer by D.W. for How to find a nearly-optimal covering of a set using SAT? D.W. https://cs.stackexchange.com/users/755 2018-04-11T06:54:22Z 2018-04-11T06:54:22Z <p>This problem is known as <a href="https://en.wikipedia.org/wiki/Logic_optimization#Circuit_minimization_in_Boolean_algebra" rel="nofollow noreferrer">circuit minimization</a>. It falls within the broad area of <a href="https://en.wikipedia.org/wiki/Logic_synthesis" rel="nofollow noreferrer">logic synthesis</a>.</p> <p>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.</p> <p>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.</p> <p>You might be interested in approaches based on interpolation. I believe those approaches use a SAT solver as a building block.</p>