<p>From the comment above:</p>

<p>I used the <a href="http://choco-solver.org/">Choco</a> Java library for <a href="http://en.wikipedia.org/wiki/Constraint_programming">Constraint programming</a> to check the correct behaviour of the gadgets used to prove the NP-completeness of the following puzzles: 
Binary Puzzle, Tents, Rolling cube puzzle without free cells, Net.
I didn't have the time to publish them, yet, but the draft papers are available on my blog.</p>

<p>The technique used is similar: all those puzzles can be modeled as a grid graph in which every node can contain a different <em>element</em> (e.g. in binary puzzle the elements are: empty cell, fixed 0, fixed 1, 0, 1), the rules of the puzzle allow or forbid some (local) configurations (e.g. in binary puzzle no more than two $0$s or $1$s next to or below each other are allowed). Then, to prove NP-completeness it is sufficient to build a square $n \times n$ <em>gadget</em> that simulates:</p>

<p>(A) a logic gate (AND + OR) and links, if we want to use PLANAR SAT as the source NPC problem; or</p>

<p>(B) a node of degree 3 in which exactly 1 entrance and 1 exit can be activated at the same time, if we want to use HAMILTONIAN CYCLE on grid graphs as the source NPC problem (note that in this case, there must be another condition that forces a "connected path").</p>

<p>In both cases we use an initial configuration that fixes the boundaries of the gadgets (to forbid unwanted interactions) and we allow the interaction between two adjacent gadgets only through a central element (or group of elements). The configuration of such central element should represent a logic value in the (A) case or a traversal in the (B) case.</p>

<p>For example to model an AND:</p>

<pre><code>***C***   *=fixed elements (initial config. of the puzzle)
*xxxxx*   x=internal logic (some elements can be fixed,
AxxxxxB     other must be completed/traversed)
*xxxxx*   A,B,C=elements shared with adjacent gadgets
*******
</code></pre>

<p>At this point to check the gadget using a SAT solver (it's better to use a CPL) it's enough to implement the rules of the puzzle, then check the satisfiability when A,B,C take all possible combinations of values; and see if they are consistent with the desired behaviour. E.g. in the AND case, in all gadget valid (satisfiable) configurations in which C is true (C represents the logic value true), both A and B must be true.</p>

<p>If gadgets are very complicated (e.g. in the Rolling cube puzzle) I think that it is the only way to ensure that they work correctly (and that the NPC proof is correct).</p>

CC BY-SA 3.0
2015-02-02T15:38:43.973Z
2015-02-02T16:53:08.683Z
2015-02-02T16:53:08.683Z
Marzio De Biasi
<p>I did this very thing — computer-assisted NP-completeness proof — in my bachelor thesis!</p>

<p>The bad part - it's in Russian and wasn't translated to English.
<a href="http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf">http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf</a></p>

<p>I worked with logical gates in 2D problems. The plan is:</p>

<ul>
<li>Manually design what a "wire" looks like in your problem.</li>
<li>Use very smart and optimized search (in fact dynamic programming over sets of profiles) to automatically design all the necessary logical gates.</li>
<li>PROFIT!</li>
</ul>

<p>The code is available, by the way:
<a href="https://code.google.com/p/metadynamic-programming/">https://code.google.com/p/metadynamic-programming/</a></p>

<p>This way, with manual work only to design the wire and to code the rules of the specific 2D problem, I was able to prove NP-completeness of:</p>

<ul>
<li>Minesweeper</li>
<li>Covering area with horizontal dominoes and vertical triminoes</li>
<li>$k$-Cross sum for $k \ge 4$; thus solving an open problem for $k \in [4,6]$!</li>
</ul>

CC BY-SA 3.0
2015-02-10T13:43:04.237Z
Even if you are not planning to publish a paper on automatic generation of gadgets, it might still be worth writing a short summary of your thesis in English, and including the file in your code repository.
András Salamon
CC BY-SA 3.0
2015-02-09T18:11:58.290Z
2015-02-09T18:11:58.290Z
Mikhail Dvorkin
<p>In this paper, I showed that if for some $k\geq 3$ there is a graph with maximum degree $k$ and chromatic edge strength strictly greater than $k$, then it is $\Theta_2^p$-complete to decide if chromatic edge strength is at most $k$. Such graphs were known for $k&gt;3$ and I did a computer search to find a suitable $12$-vertex graph for $k=3$.</p>

<p><a href="http://www.cs.bme.hu/~dmarx/papers/marx-strength.pdf" rel="nofollow">The complexity of chromatic strength and chromatic edge strength.
Computational Complexity, 14(4):308-340, 2006</a> </p>

CC BY-SA 3.0
2015-02-02T11:50:03.913Z
2016-06-01T13:23:21.313Z
2016-06-01T13:23:21.313Z
Daniel Marx
<p>the questioner has indicated he is ok with a more broad interpretation of the Schaefer statement in an answer. coincidentally have been collecting links for a blog on a nearby topic &amp; will write some up here.</p>
<p>the original statement (sec 7 p225) is clear in its intentions as illustrated with example of a NP complete reduction from 2 colorable perfect matching thm 7.1 using the &quot;dichotomy thm&quot; 2.1.</p>
<p>so his stated idea is that one has some algorithm <span class="math-container">$F(x)$</span> that generates SAT clauses, and one <em>a priori</em> does not know the overall structure of these clauses, and that one can generate sample formulas and examine their clause structure to see how they relate to the dichotomy thm. the idea is a sketch and omits some details because obviously even if all <em>finite set</em> of samples adhere to some rule it is not a proof. ie its not <em>automated</em> but <em>&quot;computer assisted.&quot;</em> (human analysis/ interpretation is required).</p>
<p>Schaefer also refers to <em>randomly generating various input configurations</em> ie examining samples <span class="math-container">$F(x)$</span> over random <span class="math-container">$x$</span>.</p>
<p>taking a broad pov these general ideas can be seen to have grown &amp; been explored in many areas of research since these <em>1978</em> musings/ &quot;seed ideas&quot; leading to entire large branches and research programs, still ongoing, none of which existed in almost any form at the time of writing of Schaefers paper. 1<sup>st</sup> one general idea is <em>empirical analysis of NP completeness properties via instance generators/ solvers/ analyzers</em>.</p>
<ul>
<li><p>the largest research area spawned here is into random SAT instances and looking at SAT solver performance on them which led to discovery of the transition point in the mid 1990s, later shown to have deep connections to statistical physics and an apparently ubiquitious/ intrinsic/ fundamental aspect/ characteristic of <em>all</em> NP complete problems. there are very many papers in this area &amp; now a few books. see eg <a href="http://cds.cern.ch/record/1166773/files/9780198570837_TOC.pdf" rel="nofollow noreferrer">Information, physics, and Computation</a> Mezard / Montanari</p>
</li>
<li><p><a href="http://www.st.ewi.tudelft.nl/sat/theses/paul.pdf" rel="nofollow noreferrer">Decomposing satisfiability problems
or Using graphs to get a better insight into satisfiability problems</a>, Herwig 2006 (83pp). this is a somewhat novel approach wrt other published research that looks at the variable-clause graph structure of generated SAT instances and analyzes their structure/ metrics to find correlations with hardness.</p>
</li>
<li><p>one can take conjectured-hard problems and encode them as SAT instances &amp; then examine their structure or run SAT solvers on them &amp; observe the dynamic behavior of the SAT solvers. its not easy to figure out when this was 1st done but an early case is with factoring, probably in the mid 1990s or so, and these instances showed up in the DIMACS SAT solver contests. unfortunately this was not necessarily considered separately publishable research results at the time. there are allusions in a few SAT papers.</p>
<p>see eg <a href="http://courses.cs.washington.edu/courses/cse573/04au/Project/mini1/TheS&amp;Ateam/SATeamFinalPaper.pdf" rel="nofollow noreferrer">Satisfy This: An Attempt at Solving Prime Factorization using Satisfiability Solvers</a> by Stefan Schoenmackers, Anna Cavender and also cs.se question <a href="https://cs.stackexchange.com/questions/6588/reducing-the-integer-factorization-problem-to-an-np-complete-problem">reducing integer factorization problem to NP complete problem</a> &amp; (there are some other related/ scattered (T)CS stackexchange questions on this).</p>
</li>
</ul>
<p>2<sup>nd</sup> another modern general idea/ seed inherent in Schaefers old statement is <em>attacking hard algorithmic or mathematical problems in general by converting them to SAT instances, and using off-the-shelf (but state-of-the-art) SAT solvers</em> (ie SAT solving can be regarded broadly as literally one of the earliest cases in logic/ math of <em>computer automated theorem proving</em> where SAT formula solutions are like &quot;theorems&quot;, although admittedly the modern pov on that may have shifted somewhat) and there are some notable recent successes on this front.</p>
<ul>
<li><p>the <a href="http://en.m.wikipedia.org/wiki/%C2%B11-sequence#Erd.C5.91s_discrepancy_problem" rel="nofollow noreferrer">Erdos Discrepancy problem</a> related to bounds on random walks is very hard and progress was limited with analytic approaches, and a novel/ unprecedented, empirical approach with SAT was recently taken to achieve some key results on a related open problem, celebrated by many as a veritable breakthrough. <a href="http://arxiv.org/abs/1402.2184" rel="nofollow noreferrer">a SAT attack on the Erdos discrepancy conjecture</a> Konev, Lisitsa</p>
</li>
<li><p>research on optimal sorting networks goes back decades and there are natural hard open problems on minimal sizes of networks to sort a given number of elements. within last few years there has been major recent progress in converting these to SAT instances &amp; running standard solvers on them. <a href="http://arxiv.org/abs/1501.06946" rel="nofollow noreferrer">New Bounds on Optimal Sorting Networks</a> Ehlers, Müller, also cites other recent work.</p>
</li>
</ul>

CC BY-SA 3.0
2015-02-01T18:54:56.683Z
2015-02-01T18:54:56.683Z
2020-06-17T09:38:08.363Z
vzn
<p>As for question 2, there are at least two examples of $NP$-completeness proofs that involve computer-assistant.</p>

<p><a href="http://link.springer.com/chapter/10.1007%2F978-3-642-45278-9_13">Erickson and  Ruskey</a> provided a computer-aided proof that <a href="http://alejandroerickson.com/home/blog/im/Erickson-Ruskey-IWOCA-2013.pdf">Domino Tatami Covering</a> is NP-complete. They gave a polynomial time reduction from planar 3-SAT to tatami domino covering. A SAT-solver (Minisat) was used to automate gadgets discovery in the reduction. No other $NP$-completeness proof is known for it.</p>

<p><a href="http://www6.in.tum.de/Main/Publications/Ruepp2010a.pdf">Ruepp and Holzer</a> proved that pencil puzzle Kakuro is $NP$-complete. Some parts of the $NP$-completeness proof were generated automatically using a SAT-solver ( again Minisat).</p>

CC BY-SA 3.0
2015-02-02T12:39:17.027Z
At least partly similar is "Minimum-weight triangulation is NP-hard" by Mulzer and Rote. A computer was used to establish the correctness of gadgets (but maybe the gadgets were found "by hand").
Juho
CC BY-SA 3.0
2015-01-31T16:19:59.343Z
2015-01-31T19:49:39.690Z
2015-01-31T19:49:39.690Z
Mohammad Al-Turkistany
<p>In the paper <a href="http://aleteya.cs.buap.mx/~jlavalle/papers/complexity/p216-schaefer.pdf">"THE COMPLEXITY OF SATISFIABILITY PROBLEMS"</a> by Thomas J. Schaefer, the author has mentioned that</p>

<p><code>This raises the intriguing possibility of computer-assisted NP-completeness proofs. Once the researcher has established the basic framework for simulating conjunctions of clauses, the relational complexity could be explored with the help of a computer. The computer would be instructed to randomly generate various input configurations and test whether the defined relation was non-affine, non-bijunctive, etc.</code></p>

<p>Of course, this is a limitation:</p>

<p><code>The fruitfulness of such an approach remains to be proved: the enumeration of the elements of a relation on lO or 15 variables is Surely not a light computational task.</code></p>

<p>I am curious that </p>

<blockquote>
  <ol>
  <li>Are there follow-up researches in developing this idea of "computer-assisted NP-completeness proofs"? What is the state-of-the-art (may be specific to $\textsf{3SAT}$ or $\textsf{3-Partition}$)?<br>
  Since Schaefer has proposed the idea of "computer-assisted" NP-Completeness proof (at least for reductions from $\textsf{SAT}$), does this mean there are some general principles/structures underlying these reductions (for the ones from $\textsf{3SAT}$ or $\text{3-Partition}$)? If so, what are they?    </li>
  <li>Does anyone have experience in proving NP-completeness with a computer-assistant? Or can anyone make up an artificial example?</li>
  </ol>
</blockquote>

CC BY-SA 3.0
2015-01-31T17:13:30.687Z
It's not the same thing of a "computer-assisted" proof, however I used a SAT solver to check the correct behaviour of the gadgets used in the reductions to prove the NP-completeness of the following games: Binary Puzzle, Tents, Rolling cube puzzle without free cells, Net; the last two are quite complicated gadgets.
Marzio De Biasi
CC BY-SA 3.0
2015-01-31T17:40:50.903Z
that is a _1978_ paper that is now prescient in this regard if interpreted broadly instead of narrowly. there is a lot of empirical analysis of SAT and NP complete problems. transition point research can be seen to be a large manifestation of this idea. also there was a recent breakthrough on the Erdos discrepancy problem wrt SAT. another emerging area is finding small sorting networks encoded in SAT. another example, converting hard problems to SAT like factoring & studying instances. have not seen anyone write a large survey of all this. may try to hammer out some of this into an answer.
vzn
CC BY-SA 3.0
2015-02-01T04:11:33.883Z
@MarzioDeBiasi Would you like to share your experience in this regard (using a SAT solver to check the gadgets is also highly appreciated)? Thanks.
hengxin
CC BY-SA 3.0
2015-02-01T04:16:48.367Z
@vzn Sounds very interesting and exciting. Looking forward to your answer. Thanks in advance. You can interpret it broadly as you want and please feel free to edit the post to make it more attractive to good answers.
hengxin
CC BY-SA 3.0
2015-02-01T21:23:01.703Z
@hengxin: but I didn't have the time to publish them yet, so those papers are still "unofficial" ... however if you want I can post an answer in which I briefly explain the technique used (though it has no deep insights).
Marzio De Biasi
CC BY-SA 3.0
2015-02-02T04:21:26.093Z
@MarzioDeBiasi Your experience will be invaluable. Since Schaefer has proposed the idea of "computer-assisted" NP-Completeness proof (at least for reductions from $\textsf{SAT}$), does this mean there are some general principles/structures underlying these reductions (for the ones from $\textsf{SAT}$ or $\text{3-Partition}$)?
hengxin
CC BY-SA 3.0
2015-02-03T13:42:20.557Z
There's a nice paper of Trevisan et al. that constructs optimum gadgets using LP: http://theory.stanford.edu/~trevisan/pubs/gadgetfull.ps
didest
CC BY-SA 3.0
2015-02-03T13:49:52.303Z
@DiegodeEstrada Interesting. Thanks. Maybe you can convert it into an answer.
hengxin
<cc.complexity-theory><reference-request><soft-question><reductions><proof-assistants>
Curious about computer-assisted NP-completeness proofs
hengxin
# Curious about computer-assisted NP-completeness proofs

(Asked by: username_0 on 2015-01-31)

In the paper ["THE COMPLEXITY OF SATISFIABILITY PROBLEMS"](http://aleteya.cs.buap.mx/~jlavalle/papers/complexity/p216-schaefer.pdf) by Thomas J. Schaefer, the author has mentioned that

`This raises the intriguing possibility of computer-assisted NP-completeness proofs. Once the researcher has established the basic framework for simulating conjunctions of clauses, the relational complexity could be explored with the help of a computer. The computer would be instructed to randomly generate various input configurations and test whether the defined relation was non-affine, non-bijunctive, etc.`

Of course, this is a limitation:

`The fruitfulness of such an approach remains to be proved: the enumeration of the elements of a relation on lO or 15 variables is Surely not a light computational task.`

I am curious that

> 1. Are there follow-up researches in developing this idea of "computer-assisted NP-completeness proofs"? What is the state-of-the-art (may be specific to $\textsf{3SAT}$ or $\textsf{3-Partition}$)?  
>    Since Schaefer has proposed the idea of "computer-assisted" NP-Completeness proof (at least for reductions from $\textsf{SAT}$), does this mean there are some general principles/structures underlying these reductions (for the ones from $\textsf{3SAT}$ or $\text{3-Partition}$)? If so, what are they?
> 2. Does anyone have experience in proving NP-completeness with a computer-assistant? Or can anyone make up an artificial example?

**Tags:** cc.complexity-theory, reference-request, soft-question, reductions, proof-assistants
> **Comments:**
> **username_1**: It's not the same thing of a "computer-assisted" proof, however I used a SAT solver to check the correct behaviour of the gadgets used in the reductions to prove the NP-completeness of the following games: Binary Puzzle, Tents, Rolling cube puzzle without free cells, Net; the last two are quite complicated gadgets.  
> **username_2**: that is a _1978_ paper that is now prescient in this regard if interpreted broadly instead of narrowly. there is a lot of empirical analysis of SAT and NP complete problems. transition point research can be seen to be a large manifestation of this idea. also there was a recent breakthrough on the Erdos discrepancy problem wrt SAT. another emerging area is finding small sorting networks encoded in SAT. another example, converting hard problems to SAT like factoring & studying instances. have not seen anyone write a large survey of all this. may try to hammer out some of this into an answer.  
> **username_0**: @MarzioDeBiasi Would you like to share your experience in this regard (using a SAT solver to check the gadgets is also highly appreciated)? Thanks.  
> **username_0**: @vzn Sounds very interesting and exciting. Looking forward to your answer. Thanks in advance. You can interpret it broadly as you want and please feel free to edit the post to make it more attractive to good answers.  
> **username_1**: @hengxin: but I didn't have the time to publish them yet, so those papers are still "unofficial" ... however if you want I can post an answer in which I briefly explain the technique used (though it has no deep insights).  
> **username_0**: @MarzioDeBiasi Your experience will be invaluable. Since Schaefer has proposed the idea of "computer-assisted" NP-Completeness proof (at least for reductions from $\textsf{SAT}$), does this mean there are some general principles/structures underlying these reductions (for the ones from $\textsf{SAT}$ or $\text{3-Partition}$)?  
> **username_3**: There's a nice paper of Trevisan et al. that constructs optimum gadgets using LP: http://theory.stanford.edu/~trevisan/pubs/gadgetfull.ps  
> **username_0**: @DiegodeEstrada Interesting. Thanks. Maybe you can convert it into an answer.  

---

## 5 answers

### Answer by username_7 on 2015-01-31. Score: 22 | Accepted answer

As for question 2, there are at least two examples of $NP$-completeness proofs that involve computer-assistant.

[Erickson and Ruskey](http://link.springer.com/chapter/10.1007%2F978-3-642-45278-9_13) provided a computer-aided proof that [Domino Tatami Covering](http://alejandroerickson.com/home/blog/im/Erickson-Ruskey-IWOCA-2013.pdf) is NP-complete. They gave a polynomial time reduction from planar 3-SAT to tatami domino covering. A SAT-solver (Minisat) was used to automate gadgets discovery in the reduction. No other $NP$-completeness proof is known for it.

[Ruepp and Holzer](http://www6.in.tum.de/Main/Publications/Ruepp2010a.pdf) proved that pencil puzzle Kakuro is $NP$-complete. Some parts of the $NP$-completeness proof were generated automatically using a SAT-solver ( again Minisat).

> **Comments:**
> **username_8**: At least partly similar is "Minimum-weight triangulation is NP-hard" by Mulzer and Rote. A computer was used to establish the correctness of gadgets (but maybe the gadgets were found "by hand").  

---

### Answer by username_6 on 2015-02-02. Score: 15

In this paper, I showed that if for some $k\geq 3$ there is a graph with maximum degree $k$ and chromatic edge strength strictly greater than $k$, then it is $\Theta\_2^p$-complete to decide if chromatic edge strength is at most $k$. Such graphs were known for $k>3$ and I did a computer search to find a suitable $12$-vertex graph for $k=3$.

[The complexity of chromatic strength and chromatic edge strength.
Computational Complexity, 14(4):308-340, 2006](http://www.cs.bme.hu/~dmarx/papers/marx-strength.pdf)


---

### Answer by username_1 on 2015-02-02. Score: 14

From the comment above:
I used the Choco Java library for Constraint programming to check the correct behaviour of the gadgets used to prove the NP-completeness of the following puzzles: 
Binary Puzzle, Tents, Rolling cube puzzle without free cells, Net.
I didn't have the time to publish them, yet, but the draft papers are available on my blog.
The technique used is similar: all those puzzles can be modeled as a grid graph in which every node can contain a different element (e.g. in binary puzzle the elements are: empty cell, fixed 0, fixed 1, 0, 1), the rules of the puzzle allow or forbid some (local) configurations (e.g. in binary puzzle no more than two $0$s or $1$s next to or below each other are allowed). Then, to prove NP-completeness it is sufficient to build a square $n \times n$ gadget that simulates:
(A) a logic gate (AND + OR) and links, if we want to use PLANAR SAT as the source NPC problem; or
(B) a node of degree 3 in which exactly 1 entrance and 1 exit can be activated at the same time, if we want to use HAMILTONIAN CYCLE on grid graphs as the source NPC problem (note that in this case, there must be another condition that forces a "connected path").
In both cases we use an initial configuration that fixes the boundaries of the gadgets (to forbid unwanted interactions) and we allow the interaction between two adjacent gadgets only through a central element (or group of elements). The configuration of such central element should represent a logic value in the (A) case or a traversal in the (B) case.
For example to model an AND:
***C***   *=fixed elements (initial config. of the puzzle)
*xxxxx*   x=internal logic (some elements can be fixed,
AxxxxxB     other must be completed/traversed)
*xxxxx*   A,B,C=elements shared with adjacent gadgets
*******

At this point to check the gadget using a SAT solver (it's better to use a CPL) it's enough to implement the rules of the puzzle, then check the satisfiability when A,B,C take all possible combinations of values; and see if they are consistent with the desired behaviour. E.g. in the AND case, in all gadget valid (satisfiable) configurations in which C is true (C represents the logic value true), both A and B must be true.
If gadgets are very complicated (e.g. in the Rolling cube puzzle) I think that it is the only way to ensure that they work correctly (and that the NPC proof is correct).


---

### Answer by username_4 on 2015-02-09. Score: 11

I did this very thing — computer-assisted NP-completeness proof — in my bachelor thesis!

The bad part - it's in Russian and wasn't translated to English.
<http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf>

I worked with logical gates in 2D problems. The plan is:

* Manually design what a "wire" looks like in your problem.
* Use very smart and optimized search (in fact dynamic programming over sets of profiles) to automatically design all the necessary logical gates.
* PROFIT!

The code is available, by the way:
<https://code.google.com/p/metadynamic-programming/>

This way, with manual work only to design the wire and to code the rules of the specific 2D problem, I was able to prove NP-completeness of:

* Minesweeper
* Covering area with horizontal dominoes and vertical triminoes
* $k$-Cross sum for $k \ge 4$; thus solving an open problem for $k \in [4,6]$!

> **Comments:**
> **username_5**: Even if you are not planning to publish a paper on automatic generation of gadgets, it might still be worth writing a short summary of your thesis in English, and including the file in your code repository.  

---

### Answer by username_2 on 2015-02-01. Score: -4

the questioner has indicated he is ok with a more broad interpretation of the Schaefer statement in an answer. coincidentally have been collecting links for a blog on a nearby topic & will write some up here.

the original statement (sec 7 p225) is clear in its intentions as illustrated with example of a NP complete reduction from 2 colorable perfect matching thm 7.1 using the "dichotomy thm" 2.1.

so his stated idea is that one has some algorithm $F(x)$ that generates SAT clauses, and one *a priori* does not know the overall structure of these clauses, and that one can generate sample formulas and examine their clause structure to see how they relate to the dichotomy thm. the idea is a sketch and omits some details because obviously even if all *finite set* of samples adhere to some rule it is not a proof. ie its not *automated* but *"computer assisted."* (human analysis/ interpretation is required).

Schaefer also refers to *randomly generating various input configurations* ie examining samples $F(x)$ over random $x$.

taking a broad pov these general ideas can be seen to have grown & been explored in many areas of research since these *1978* musings/ "seed ideas" leading to entire large branches and research programs, still ongoing, none of which existed in almost any form at the time of writing of Schaefers paper. 1st one general idea is *empirical analysis of NP completeness properties via instance generators/ solvers/ analyzers*.

* the largest research area spawned here is into random SAT instances and looking at SAT solver performance on them which led to discovery of the transition point in the mid 1990s, later shown to have deep connections to statistical physics and an apparently ubiquitious/ intrinsic/ fundamental aspect/ characteristic of *all* NP complete problems. there are very many papers in this area & now a few books. see eg [Information, physics, and Computation](http://cds.cern.ch/record/1166773/files/9780198570837_TOC.pdf) Mezard / Montanari
* [Decomposing satisfiability problems
  or Using graphs to get a better insight into satisfiability problems](http://www.st.ewi.tudelft.nl/sat/theses/paul.pdf), Herwig 2006 (83pp). this is a somewhat novel approach wrt other published research that looks at the variable-clause graph structure of generated SAT instances and analyzes their structure/ metrics to find correlations with hardness.
* one can take conjectured-hard problems and encode them as SAT instances & then examine their structure or run SAT solvers on them & observe the dynamic behavior of the SAT solvers. its not easy to figure out when this was 1st done but an early case is with factoring, probably in the mid 1990s or so, and these instances showed up in the DIMACS SAT solver contests. unfortunately this was not necessarily considered separately publishable research results at the time. there are allusions in a few SAT papers.

  see eg [Satisfy This: An Attempt at Solving Prime Factorization using Satisfiability Solvers](http://courses.cs.washington.edu/courses/cse573/04au/Project/mini1/TheS&Ateam/SATeamFinalPaper.pdf) by Stefan Schoenmackers, Anna Cavender and also cs.se question [reducing integer factorization problem to NP complete problem](https://cs.stackexchange.com/questions/6588/reducing-the-integer-factorization-problem-to-an-np-complete-problem) & (there are some other related/ scattered (T)CS stackexchange questions on this).

2nd another modern general idea/ seed inherent in Schaefers old statement is *attacking hard algorithmic or mathematical problems in general by converting them to SAT instances, and using off-the-shelf (but state-of-the-art) SAT solvers* (ie SAT solving can be regarded broadly as literally one of the earliest cases in logic/ math of *computer automated theorem proving* where SAT formula solutions are like "theorems", although admittedly the modern pov on that may have shifted somewhat) and there are some notable recent successes on this front.

* the [Erdos Discrepancy problem](http://en.m.wikipedia.org/wiki/%C2%B11-sequence#Erd.C5.91s_discrepancy_problem) related to bounds on random walks is very hard and progress was limited with analytic approaches, and a novel/ unprecedented, empirical approach with SAT was recently taken to achieve some key results on a related open problem, celebrated by many as a veritable breakthrough. [a SAT attack on the Erdos discrepancy conjecture](http://arxiv.org/abs/1402.2184) Konev, Lisitsa
* research on optimal sorting networks goes back decades and there are natural hard open problems on minimal sizes of networks to sort a given number of elements. within last few years there has been major recent progress in converting these to SAT instances & running standard solvers on them. [New Bounds on Optimal Sorting Networks](http://arxiv.org/abs/1501.06946) Ehlers, Müller, also cites other recent work.


---

