<p>suppose that two SAT formulas on different variables $F_1, F_2$ are given on the input that are known to be true and the problem is to build an algorithm that finds a solution to each. the formulas actually are generated by another algorithm which creates/ generates instances $F_n$ for any $n$. the solving algorithm can find/ exploit "similar structures" contained in each by analyzing eg the clause-variable graph, eg looking for graph isomorphisms etc.</p>

<blockquote>
  <p>has this problem of finding "similarities" between two SAT formulas by a solver been studied?</p>
</blockquote>

<p>there is some rough connection of this eg implications of worst case bounds in this paper <a href="http://eccc.hpi-web.de/report/2014/075/">A simple proof that AND-compression of NP-complete problems is hard</a> (Dell), but am looking for more direct algorithm(s) and possibly more empirical approaches/ analysis, eg somewhat similar to strategies/ heuristics used in SAT solver implementations. (this problem has applications in eg <a href="http://en.wikipedia.org/wiki/Automated_theorem_proving">automated theorem proving</a>.)</p>

CC BY-SA 3.0
2014-07-26T09:55:47.020Z
There are sat portfolios like satzilla that use machine learning to try to identify which solver is the best. But not sure if that's what you're looking for. If the set of variables remains the same, one easy technique would be to keep activities and polarities from the last formula for the next one.
Mikolas
CC BY-SA 3.0
2014-07-27T17:08:29.453Z
"Learning" is an important componant of most sat solvers. In particular, finding interpolants between formulas is an active area for improving or making feasible the proof of certain difficult SAT instances. Conceivably, finding an interpolant between a proven instance P and an unproven one Q may help prove Q more quickly. I think this is a very interesting question!
cody
<reference-request><sat><machine-learning><application-of-theory><automated-theorem-proving>
extracting/ exploiting similarity of SAT instances by solver
vzn
# extracting/ exploiting similarity of SAT instances by solver

(Asked by: username_0 on 2014-07-25)

suppose that two SAT formulas on different variables $F\_1, F\_2$ are given on the input that are known to be true and the problem is to build an algorithm that finds a solution to each. the formulas actually are generated by another algorithm which creates/ generates instances $F\_n$ for any $n$. the solving algorithm can find/ exploit "similar structures" contained in each by analyzing eg the clause-variable graph, eg looking for graph isomorphisms etc.

> has this problem of finding "similarities" between two SAT formulas by a solver been studied?

there is some rough connection of this eg implications of worst case bounds in this paper [A simple proof that AND-compression of NP-complete problems is hard](http://eccc.hpi-web.de/report/2014/075/) (Dell), but am looking for more direct algorithm(s) and possibly more empirical approaches/ analysis, eg somewhat similar to strategies/ heuristics used in SAT solver implementations. (this problem has applications in eg [automated theorem proving](http://en.wikipedia.org/wiki/Automated_theorem_proving).)

**Tags:** reference-request, sat, machine-learning, application-of-theory, automated-theorem-proving

> **Comments:**
> **username_1**: There are sat portfolios like satzilla that use machine learning to try to identify which solver is the best. But not sure if that's what you're looking for. If the set of variables remains the same, one easy technique would be to keep activities and polarities from the last formula for the next one.  
> **username_2**: "Learning" is an important componant of most sat solvers. In particular, finding interpolants between formulas is an active area for improving or making feasible the proof of certain difficult SAT instances. Conceivably, finding an interpolant between a proven instance P and an unproven one Q may help prove Q more quickly. I think this is a very interesting question!  

---

## 0 answers

