I was reading Combinatorial Sketching for Finite Programs and wanted to understand why synthesis of the sketching language was possible/feasible.

As far as I understand a partial program is transformed to the Quantified Boolean Formula Satisfiability Problem (QBF) and a sketched (partial) program $S$ with specification $P$ and control (i.e. wholes to fill) $c$ satisfy the following:

$$ \exists c \in \{ 0, 1 \}^k, \forall x \in \{ 0,1\}^m ; P(x) = S(x,c) $$

since the problem is decidable since $c$ and $x$ range in finite domains we can solve the above problem.

Obviously it goes without saying that this cannot work in general (otherwise we could somehow solve the halting problem...?) and I am trying to understand what exactly makes this work (since I'd potentially like to design my own sketching language and I'm trying to understand how one goes about doing that). Does it work because:

We have a sketch of the program and a specification to match?

i.e. what is impossible to do is have a general procedure that generates sketches automatically? (otherwise we could solve the halting problem)? Is the only reason this is doable because the human is given a sketch $S$ of the program? Obviously the specification has to be given otherwise how do we know what programs to choose?

  • $\begingroup$ I'm not familiar with the concept but, since QBF is in PSPACE and these programs get converted to QBF, the system can only express PSPACE problems. $\endgroup$ Nov 28 '18 at 15:52
  • $\begingroup$ @DavidRicherby that doesn't matter to me, I'm interested in learning how to transform programs or partial programs to something that is decidable. Then I can check in practice if it works. For example, the paper showed synthesis of real programs like AES ciphers run in less than 1 hour on computers that were at least 12 years old. $\endgroup$ Nov 28 '18 at 15:57

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.