1
$\begingroup$

Me and my colleague are exploring new ideas to solve SAT efficiently (i.e. in polynomial time) and it's the case that there is a candidate algorithm.

Unfortunately, neither of us can write scripts well (to test more examples to prove its correctness) or more accurately ... have the sufficient mathematical maturity to write a Research Article about it.

We want to contact some researcher in the field to help us formally describe the algorithm and prove that it works for all inputs (if it holds).

We have tested a few instances of (sat,unsat) and it works (relatively small instaces but not related to DPLL).

In addition, the description of the algorithm matches the concept of nondeterminism (i,e. parallel computations, gussing phase and verification phase,etc.) can be stated / defined precisely.

Given that it is SAT, most reasearchers would consider an attempt to solve it as something invalid, how can we convince someone that this might acutally work ?

What can be a Zero Knowledge Proof (ZKP) for $SAT$ to prove that it works from the tested examples ?

Will a description of some Phases / Techniques used in the algorithm along with the solutions of tested instances suffice ?

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ I don't see the relevance of ZKP. ZKP lets you prove to me that you have a satisfying assignment without revealing what that assignment is. But you're trying to prove to me that you have a satisfying assignment without revealing how you found it. But that's easy -- just tell me the satisfying assignment! It's unlikely that that could reveal anything about your algorithm. $\endgroup$ – David Richerby Sep 29 '18 at 22:47
  • $\begingroup$ @DavidRicherby If i state to you the satisfying assignment (only) of small sized instances, you might disregard them as generated from some current approach (i.e. Brute Force), i want to explicitly state that its a new approach by describing a few steps and / or techniques that lead to it. $\endgroup$ – Black Jr. Sep 30 '18 at 1:41
  • $\begingroup$ My thought is, when i do the above described ... it will be the equivalent of having a satisfying assignment (which is proving there is a new approach used to solve $SAT$) without revealing the actual algorithm (the equivalent to the assignment of the satisfying assignment) using those small sized instances. So, it becomes an equivalent ZKP of the algorithm ? $\endgroup$ – Black Jr. Sep 30 '18 at 1:41
  • $\begingroup$ Even though the prizes have been withdrawn the RSA challenge numbers are still out there, and several have yet to be factored. Take one of them, convert it to a SAT instance and feed it to your algorithm. If you can factor RSA-2048 (for example) that will make more than a few people perk up and pay attention. $\endgroup$ – Kyle Jones Oct 1 '18 at 15:29
  • $\begingroup$ Your question seems to be related to program checking. See Section 5 of The complexity of decision versus search. $\endgroup$ – Yuval Filmus Oct 3 '18 at 3:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.