Curious about computer-assisted NP-completeness proofs

Question

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?

Answer 1

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).

Answer 2

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

Answer 3

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 4

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]$!

Answer 5

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. 1^st 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 Mezard / Montanari

• Decomposing satisfiability problems or Using graphs to get a better insight into satisfiability problems, 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 by Stefan Schoenmackers, Anna Cavender and also cs.se question reducing integer factorization problem to NP complete problem & (there are some other related/ scattered (T)CS stackexchange questions on this).

2^nd 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 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 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 Ehlers, Müller, also cites other recent work.