Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

IMP- to SATconstruction has polynomial blowup #21

Open
maxhaslbeck opened this issue Nov 2, 2020 · 0 comments
Open

IMP- to SATconstruction has polynomial blowup #21

maxhaslbeck opened this issue Nov 2, 2020 · 0 comments
Milestone
Translation from ...

Comments

@maxhaslbeck
Copy link
Collaborator

maxhaslbeck commented Nov 2, 2020 •
edited
Loading

  • state reg_bound (any register during a computation of an IMP- program only has a number which is polynomially bounded by the input size and the number of steps taken), and maybe prove it as a "sanity check" (but you wont need it now)
  • prove size of result of PI is polynomially bounded
  • prove that PHI in SAS+ -> SAT is polynomially bounded
  • compose PI and PHI_all
  • prove that the composition going from IMP- to SAS+ is polynomially bounded

this includes #9 and #10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
Translation from IMP- to SAT
Development

No branches or pull requests
1 participant
@maxhaslbeck