I've spent so much time for pointless reformatting. With Springer LNCS it's often that you have to work really hard to cram everything into the page limit. Then Springer does some editing in the bibliography, and the article then often overflows by one or two bibliography entries and is published like that, making the effort of meeting the page limit a complete waste time
I used to teach formal methods at university, including a course with a lot of SAT examples. We tried to make it as practical as possible, with many examples and exercises in Java (where you just generate your formulas and call a solve method). Thing is, most students seemed to hate it passionately, just like with reductions to SAT in complexity theory.
I wrote a bespoke backtracking solver for a specific class of problems. Would love to use Z3 or something, but frankly, I wouldn't know how to systematically translate problem instances to solver constraints. It's essentially a kind of very complex job-shop scheduling problem with lots of dynamic inter-dependencies. Many of the problems are hard to even solve without dead-locking, while we also naturally strive to minimize overall processing time. Where would I find ressources to help me get a grip on my specific problem [1]? Could I reasonably hope that Z3 or another general solver might be faster than a moderately well designed bespoke solver in a compiled language? (My solver combines a bunch of greedy heuristics with a backtracker in case it runs into a dead-lock, which is often.)
[1] Rough problem outline: Input goods must be transformed through a complex series of assembly/machining/processing lines to output goods; each line transforms one or two inputs into an (intermediary or end-) product; an assembly line produces it's product in a fixed number of time units and cannot be stopped or delayed; finished intermediary products arrive at the end of an assembly line, which must be cleared by then; there are a limited number of temporary storage spaces where intermediary products can be moved to/from in a fixed number of time units; some assembly lines must wait for two intermediary products to be completed to start a job combining them into another intermediary or end product; end products must then be moved to their destinations.
The pdf linked on this site is the biggest collection of SMT examples I know of: https://sat-smt.codes/
I’m no SMT expert, but the way I’ve done it is to make some representation in Python Z3, and then write some function or class that generates those. I was solving MLB eliminations (more complex than it sounds) and I think I used arrays of ints for number of wins. So I’d pull MLB data, turn that into schedule objects which turned themselves into z3 constraints.
This type of problem is more the domain of Constraint Programming (a related field). Job-scheduling problems are pretty much the main focus. I would look up MiniZinc (it even comes with a nice IDE) and see if you can grok it.
- Bridge crossing: Missionaries and cannibals, 17 minute bridge crossing (I need a computer to solve this anyway)
- Concurrency: finding bug in mutual exclusion algorithm (Peterson algorithm with a bug)
- Graphs: coloring a map, finding a Hamilton path
- Sorting: Finding bugs in a sorting network
For many students it was difficult to encode problems in SAT. They seemed to understand given example encodings, but then found it difficult to vary them. There is a lot of freedom in how one may encode things and it's hard at first to debug at first when things don't work in the way you're expecting. If there is no solution, then one needs to investigate where there are unwanted constraints or errors in the encoding. If there are unwanted solutions, one needs to identify the missing constraints. It was hard to get across how to do this and it's probably frustrating for beginners.
Yeah, but then you have: It seems like every week or two this year, another crisis presented itself, each manageable in isolation.
I've had this happen and it really grinds you down when you work full-out for months and, just when you think you've contained all the crises, the next one drops.
> But the professor said he'd never do it again because 30 minutes * 30ish students was too much work.
The old German Diplom system (replaced by BSc/MSc about 15 years ago) was based on oral exams. The way this worked there was that there were much fewer exams. For example, in Computer Science I had my first oral exams two years into the degree, and there were only five of them: one in Mathematics, one in each of Theoretical, Practical and Applied, Computer Science, and one for the second subject. Each of these oral exam was 30 minutes but covered the content of four semesters. There was a second round of such exams at the end of the degree and that was it.
To be admitted to an oral exam, one needed to pass the courses that the exam was going to be about. Lecturer were free to set the passing requirements. It was often just something like a coursework threshold of 60%.
There exist only two kinds of modern mathematics books: ones which you cannot read beyond the first page and ones which you cannot read beyond the first sentence. -- Chen Ning Yang
https://de.wikipedia.org/wiki/Visual_Basic_for_Applications?...
https://news.ycombinator.com/item?id=21352796