6
$\begingroup$

I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin transformation. From the nature of my problem I know that there are redundant constraints. For example, I have a rule: $$AND\:(OR\: (x1,x2),\: OR\: (x3,x4)) \,\,\,\,\,\,(1)$$

and another: $$AND\:(OR\: (x1,x2),\: OR\: (x3,x4), \:OR\:(x5,x6))\,\,\,\,\,\, (2)$$ where $x_i$ are inputs. Both constraints have in common subnodes, for example $OR (x1,x2)$. Due to this I know that there is no point in having both constraints - if the first one becomes FALSE, then the second equals FALSE too. So the second one is redundant. This example is the easiest. One more, closer to what might be found in my formula: $$AND\:(x1,\:x2,\: OR \:(AND \:(x3,x4), \:AND\:(x5,x6)))\,\,\,\,\,\,(3)$$ and the second one: $$AND\:(x3,x4)\,\,\,\,\,\,(4)$$ In this case, I can simplify the first one to the form of: $$AND\:(x1,\:x2,\:AND\:(x5,x6))\,\,\,\,\,\,(5)$$ due to (4).

I prefer to have a lot of small rules (by a lot I mean $10^3$ or $10^4$, which in CNF become $10^5-10^6$ of clauses). The rules are not complicated - 10 ANDs and ORs and 20-30 inputs per rule at most, but they are usually much simpler.

Is there an efficient way to remove such redundancy from a formula? Is it possible with CNF formulation or I should use some other representation of the formula (BDD, for example)? Any help and directions will be useful.

$\endgroup$
7
  • $\begingroup$ You "can simplify the first one to the form of:" $AND(x1,x2)$ "due to" (4). $\;$ $\endgroup$
    – user12859
    Jul 31, 2014 at 21:53
  • $\begingroup$ The first thing I'd suggest you do is test whether removing this redundancy actually improve the efficiency of the SAT solver or not. It's possible that SAT solvers might already take advantage of this redundancy internally. There's no point spending a lot of energy on removing the redundancy if it won't help speed up the SAT solver. Do you want to try that experiment, and then report back? $\endgroup$
    – D.W.
    Jul 31, 2014 at 22:06
  • $\begingroup$ @RickyDemer Yes, it's true, but in this case you can consider 2 example separately. $\endgroup$ Aug 1, 2014 at 3:47
  • $\begingroup$ @D.W. My main concern in this activity is memory consumption. It seems that problem will evolve to the much greedier form, in terms of memory. So it seems to be a good idea to have such solution, which can be run before SAT solver, probably even incrementally at some points of time. I studied tools, like CNF minimizers and SAT solver sources, but I think that they do not perform such application specific optimizations. They operate on clause level, but here we have sets of clauses. $\endgroup$ Aug 1, 2014 at 3:56
  • 1
    $\begingroup$ @D.W. I've run some artificial tests. Memory consumption was reduced by 20-30% and runtime was not affected significantly. Actually, it was improved by 1-3%, but I consider these results as a noise. I'm still looking for general solution for my simplification problem, probably I will post here results in a couple of weeks. $\endgroup$ Aug 4, 2014 at 10:34

3 Answers 3

3
$\begingroup$

The simplification you're describing is called subsumption. It's a standard technique and some SAT solvers (e.g. minisat) will apply it along with other simplification techniques as a preprocessing step before attacking the SAT problem itself. In particular, subsumption and equivalent variable substitution together, applied to the generated CNF formula, are enough to do the common subformula elimination you described in the question. That's because each circuit transformation yields an output variable, and output variables derived from the same circuit can be efficiently identified and reduced to references to a single variable. After that normal subsumption rules applied to clauses will eliminate the common subformulas.

If you're using a solver that doesn't do this preprocessing, then you can do the rough equivalent of it during conversion to CNF. First you'll need to apply duplicate circuit suppression while you're doing the Tseitin tranformation. As you're doing the transformation to CNF, memoize each circuit you've converted. If you encounter the circuit again, skip the circuit conversion and use the same output variable that you used for the memoized circuit. Once you've converted everything to clauses, do normal clause subsumption, i.e. check each clause A against every other longer B clause to see if A's literals are a subset of B's. If so, then A subsumes B and clause B can be discarded from the formula.

$\endgroup$
0
1
$\begingroup$

I finally found an appropriate solution.

My CNF minimization problem actually consists from 2 different tasks and requires 2 different techniques, which are described in these 2 papers:

  1. Hyper-binary resolution, HBR (link)

This technique allows to perform something like 'structural hashing'. Consider two logic gates $AND1(a,b)$ and $AND2(a,b)$. It is obvious, that they are the same, but in CNF form it is not so clear:$$(and1|-a|-b)(-and1|a)(-and1|b)(and2|-a|-b)(-and2|a)(-and2|b).$$ Using 'tail' clauses like $(-and1|a)(-and1|b)$, HBR allows to conclude that $and1==and2$. This technique only appends additional clauses to CNF.

2. Hidden tautology elimination, HTE (link)

Consider following CNF: $$(a|b|c)(a|d)(d|-c).$$ In case of binary clauses, we can 'glue' them together, if clauses have some literals in common: $$(a|b|c),(a|d)\rightarrow(a|b|c|d)$$ $$(a|b|c|d),(d|-c)\rightarrow (a|b|c|d|-c).$$ Resulting clause always will be true due to $(c|-c)$, so these clauses must be removed or considered in some other way.

In conclusion, in our case, memory consumption has been reduced by x3-x10. Runtime in some cases have been improved by x2, sometimes it have been degraded. We use some additional problem specific optimizations, but there is no point to discuss them. Main goal have been successfully achieved.

$\endgroup$
2
  • 1
    $\begingroup$ I don't understand what's going on in your part 2. Why would we 'glue' together $(a \lor b \lor c) \land (a \lor d)$ to $(a \lor b \lor c \lor d)$? That loses information. Are you talking about adding a new clause, or replacing existing clauses? Adding a new clause seems counter-productive if you want to minimize the set of clauses. Replacing existing clauses seems incorrect, as it may change the set of satisfying assignments. On the other hand, replacing $(a \lor b \lor c \lor d) \land (d \lor \neg c)$ with $(a \lor b \lor d)$ is valid, if no other clause mentions $c$. $\endgroup$
    – D.W.
    Oct 9, 2014 at 21:50
  • $\begingroup$ @D.W. Thanks for pointing this out, this completely my mistake. There is a much simpler explanation. Consider just two clauses $(a \vee b) \wedge (b \vee x)$. We can add $x$ to the first one. We can do this iteratively until some fixpoint, traversing through other binary clauses, and we can end up with something like $(a \vee b \vee x \vee \neg x)$. In this case we can remove some clauses, due to they always will imply TRUE. $\endgroup$ Oct 14, 2014 at 16:17
-1
$\begingroup$

there are basically 3 fundamental techniques that can be found in various algorithms for solving SAT, and there is a lot of research on this topic in SAT solver minimization/ simplification heuristics, often integrated into leading solvers. in other words a lot of this logic is already built into good SAT solvers and it is often treated as an optimizing "black box" by practitioners.

  • KJ mentions subsumption in his answer.
  • Davis-Putnam algorithm & DPLL use subsumption & another technique called "unit propagation". this applies to formulas where there are some single-literal clauses. the truth value can be "propagated" to other clauses in a sort of chain-reaction that also can trigger other new simplifications such as subsumption.
  • a more general technique can be seen in the Quine-Mccluskey method of generating/ enumerating minterms and new more efficient "minterm covers". this can lead to exponential blowup but find simplifications that are not available from unit propagation or subsumption.

another more general/ emerging technique is to look at clause-variable graphs (eg Decomposing SAT problems by Herwig) which can reveal the overall structure of the SAT instance and "dependent vs independent variables" also known as "backbone" related elements (active area of research).

$\endgroup$

Your Answer

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

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