-
Recent Posts
- Fault Detection in Logic Circuits March 8, 2024
- Minimum Weight And/Or Graph Solution February 15, 2024
- Decision Tree February 2, 2024
- Simply Deviated Disjunction January 19, 2024
- Matrix Cover January 8, 2024
Recent Comments
Archives
- March 2024
- February 2024
- January 2024
- December 2023
- October 2023
- September 2023
- August 2023
- March 2023
- January 2023
- December 2022
- November 2022
- October 2022
- September 2022
- August 2022
- June 2022
- May 2022
- December 2021
- November 2021
- October 2021
- September 2021
- August 2021
- July 2021
- May 2021
- April 2021
- March 2021
- February 2021
- January 2021
- December 2020
- November 2020
- October 2020
- September 2020
- August 2020
- March 2020
- February 2020
- January 2020
- December 2019
- November 2019
- October 2019
- September 2019
- August 2019
- July 2019
- June 2019
- May 2019
- April 2019
- March 2019
- February 2019
- January 2019
- December 2018
- November 2018
- October 2018
- September 2018
- August 2018
- July 2018
- June 2018
- May 2018
- April 2018
- March 2018
- February 2018
- January 2018
- December 2017
- November 2017
- October 2017
- September 2017
- August 2017
- July 2017
- June 2017
- May 2017
- April 2017
- March 2017
- February 2017
- January 2017
- December 2016
- November 2016
- October 2016
- September 2016
- August 2016
- July 2016
- June 2016
- May 2016
- April 2016
- March 2016
- February 2016
- January 2016
- December 2015
- November 2015
- October 2015
- September 2015
- August 2015
- July 2015
- June 2015
- May 2015
- April 2015
- March 2015
- February 2015
- January 2015
- December 2014
- November 2014
- October 2014
- September 2014
- August 2014
- July 2014
- June 2014
Categories
- Algebra and Number Theory
- Appendix- Algebra and Number Theory
- Appendix- Automata and Language Theory
- Appendix- Games and Puzzles
- Appendix- Mathematical Programming
- Appendix- Network Design
- Appendix- Program Optimization
- Appendix- Sets and Partitions
- Appendix-Graph Theory
- Appendix-Logic
- Appendix: Miscellaneous
- Appendix: Sequencing and Scheduling
- Appendix: Storage and Retrieval
- Chapter 3 Exercises
- Core Problems
- Overview
- Problems not in appendix
- Uncategorized
Tag Archives: 3SAT
Protected: Cyclic Ordering
Enter your password to view comments.
Posted in Appendix: Miscellaneous
Tagged 3SAT, Cyclic Ordering, MS2
Programs With Formally Recursive Procedures
This is the last of the “Program Optimization” problems, and the next section is the last one on “Miscellaneous” problems, which has 19 problems in it. So, unless some diversion into a problem not in the book happens, we’re on the countdown through the last 20 problems! The end is in sight!
The problem: Programs with Formally Recursive Procedures. This is problem PO20 in the Appendix.
The description: Given a set of function definitions and a program that makes a sequence of function calls using those definitions (the paper by Winklmann uses Algol because he wrote it in 1982. But any language that allows recursion should work). Are any of the procedures in the program formally recursive? For our purposes, “formally recursive” means that there exists a chain of calls that has a call to a function higher in the chain (not necessarily a parent, any ancestor will do).
My first instinct was to wonder if this problem was actually undecidable. It’s not because we will have some fixed # of procedures d, and so any call chain needs to be checked only to depth d+1- if we get that far, we must have a repeat someplace. If we never get that far, we can back up and check other call chains, eventually checking all of the paths through the call tree exhaustively. The proof that the problem is in NP is in the paper, but it involves representing the call tree as a DAG so we can use one vertex for two equivalent paths. Winklmann says that if you do that the number of vertices is “bounded” by the number of procedures in the program (he doesn’t say what that bound is, though).
Example: It’s hard to make a small example that’s not obvious. How about this:
E(){
E();
}
D(){
}
C(){
A();
}
B(){
D();
}
A(){
B();
F
}
main(){
A()
}
If “F” is replaced by a call to C, the program is formally recursive, because the call chain main->A->C->A has a repeat. If we replace that F with another call to B the program is not formally recursive because even though recursive functions like E exist (and even though B gets called twice in two different chains), there is no call chain that will start at main and hit E (or anything) more than once.
Reduction: Winklmann uses 3SAT. So we start with a formula B with m clauses and n variables. We’ll write some functions:
AssignXi(c1..cm)
: generates two calls to AssignXi+1
. The function has one parameter for each clause. The first call simulates setting variable Xi to true by passing a “true” value in all parameters that represent clauses that have variable Xi represented positively. The second call simulates setting variable Xi to false by passing a “true” value in all parameters that represent clauses that have variable Xi returning negatively. In all other cases, the function passes on the ci parameter it was given.
AssignXn(c1..cm)
: once we reach the end of the variables, we have to stop. This function calls the “Check
” function we’ll be defining in a minute twice, once reflecting setting variable Xn to true, one reflecting setting it to false.
Truej(cj+1..cm):
There is one “true” function for each clause, each one has a parameter for all clauses with larger numbers. The paper writes this function a little weirdly, but I think a good definition is:
if(cj+1 is true){
Truej+1(cj+2..cm);
else
Falsej+1(cj+2...cm);
}
So, as long as the parameters are true, we’ll continue calling down through the true functions to the end. The last True function is what will make us formally recursive:
Truem()
: Calls Assign1
(False, False, ...False)
. Our main program will begin with a call to Assign
1 with these exact parameters, so if we can get here, we will have found our recursive call.
The False functions end a call chain:
Falsej(cj+1..cm){
// do nothing
}
The Check function’s job is to start the appropriate call to True or False:
Check(c1..cm){
if(c1 is true)
True1(c2..cm);
else
False1(c2..cm);
}
Our main program is just a call to Assign1(False, False..False)
. It’ll go through all of the various AssignXi
funtions trying to assign variables (and thus clauses) to true. Each assignment will be checked, and each check will either hit a False function (meaning a clause wasn’t satisfied, and so we will backtrack and try an alternate assignment) or the final True function, which will generate our recursive call. So this program has a recursive call chain if and only if the formula was satisfiable.
Notice that while the run of this program might take exponential time, that’s ok because reductions are concerned with the time it takes to create the new problem instance, and there are “just” 2m+n+1 functions to create.
Difficulty: 6. This is a neat problem and reduction- I think the “write a backtracking program to try all combinations” is pretty gettable. The hard part is the check and true/false functions at the end. We can’t really use loops because loops make programs undecidable (you can’t show the problem is in NP by going down d+1 calls if you might have an infinite loop someplace and won’t get through all of those calls). So we have to build a chain of recursive calls instead, with dead-ends to force the backtracking.
Protected: Non-Containment for Free B-Schemes
Enter your password to view comments.
Posted in Appendix- Program Optimization
Tagged 3SAT, Difficulty 7, Non-Containment for Free B-Schemes, PO18
Protected: Inequivalence of Loop Programs Without Nesting
Enter your password to view comments.
Posted in Appendix- Program Optimization
Tagged 3SAT, Difficulty 5, Inequivalence of Loop Programs Without Nesting, PO14
Protected: Inequivalence of Programs with Arrays, Inequivalence of Programs with Assignments
Enter your password to view comments.
Posted in Appendix- Program Optimization
Tagged 3SAT, Difficulty 6, Inequivalence of Programs with Arrays, Inequivalence of Programs with Assignments, PO11, PO12
Protected: Code Generation With Unfixed Variable Locations
Enter your password to view comments.
Posted in Appendix- Program Optimization
Tagged 3SAT, Code Generation With Unfixed Variable Locations, Difficulty 7, PO8
Protected: Code Generation on a One-Register Machine
Enter your password to view comments.
Posted in Appendix- Program Optimization
Tagged 3SAT, Code Generation on a One-Register Machine, Difficulty 6, Feedback Vertex Set, PO4
Protected: Tree Transducer Language Membership
Enter your password to view comments.
Posted in Appendix- Automata and Language Theory
Tagged 3SAT, AL21, Difficulty 8, Tree Transducer Language Membership
Protected: ETOL Language Membership
Enter your password to view comments.
Posted in Appendix- Automata and Language Theory
Tagged 3SAT, AL19, Difficulty 6, ETOL Language Membership
Protected: Regular Expression Inequivalence on Single Character Alphabets
Enter your password to view comments.
Posted in Uncategorized
Tagged 3SAT, Difficulty 8, Not in Appendix, Regular Expression Inequivalence on Single Character Alphabets