Theoretical Computer Science

Curious about computer-assisted NP-completeness proofs

In the paper "THE COMPLEXITY OF SATISFIABILITY PROBLEMS" 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?


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

Erickson and Ruskey provided a computer-aided proof that Domino Tatami Covering 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 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 (1)

  • +1 – 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"). — Feb 02, 2015 at 12:39