SAT shows up in a lot of problems. Im doing my PhD in multi-agent robotics after spending some time working on real life multirobot deployments. Ive been frustrated because most roboticists I talk to think SAT is a dead end, but we have been having insane advances in solver speeds over the years. I guess everyone is obsessed about the ML hypetrain right now, but where sat shines is when we need to orchestrate at a task level. I feel theres defintely work to be done to bridge both worlds.
Accidentally writing a SAT solver
21–30 of 41 posts
Re: Accidentally writing a SAT solver
#22Probably worth mentioning that there are well-known linear time algorithms to construct a solution for n-queen problem https://en.wikipedia.org/wiki/Eight_queens_puzzle#Existence_...
Re: Accidentally writing a SAT solver
#23SAT shows up in a lot of problems. Im doing my PhD in multi-agent robotics after spending some time working on real life multirobot deployments. Ive been frustrated because most roboticists I talk to think SAT is a dead end, but we have been having insane advances in solver speeds over the years. I guess everyone is obsessed about the ML hypetrain right now, but where sat shines is when we need to orchestrate at a ta…
Actually quadratic programming is all the rage these days since computers have gotten fast enough that you can run QP solvers in your control loop.
Re: Accidentally writing a SAT solver
#24Probably worth mentioning that there are well-known linear time algorithms to construct a solution for n-queen problem https://en.wikipedia.org/wiki/Eight_queens_puzzle#Existence_...
True, finding one solution is easy but finding all the solutions can be a fun little optimization challenge.
I made a repo many years ago with a bunch of grab bag solutions for comparisons [1]; from dumb brute force to DLX (Knuth's Dancing Links) and a multithreaded bitwise backtracking algorithm. And one where I just hardcoded the answers because all the counts up to 27 are known.
So I'm all for just jumping to the existing known solutions, but it seems like the OP is having fun while they learn a little bit. They seem to just be a college freshman.
Re: Accidentally writing a SAT solver
#25Interesting post, but I’m not sure this really speaks to what goes into actually writing what would be considered a “fast” SAT solver. It seems more like a post about how SAT pops up in a lot of places if you look at them right. For the state of the art in what constitutes fast solvers, the annual SAT competition papers are quite interesting to read if you’re interested in the techniques people come up with to make t…
One would assume there are some low-hanging fruits that make up the bulk of the speed-ups, but maybe it’s really a huge pile of small incremental improvements?
My impression is that going from a very simple case like this to a moderately fast solver involves bringing in a fair number of intuitive improvements like memoization of anti-patterns and heuristic reordering of the search.
But getting a really fast solver requires multiple strategies that don't work well together (so they have to work semi-independently). This leads to other problems related to managing shared resources like how much you should let different strategies cache information at the expense of how much other strategies can cache information. Tuning all of these trade-offs is exceedingly difficult to do well since it depends a lot on the types of problems that you need to solve.
Re: Accidentally writing a SAT solver
#26[stub for offtopicness]
"* SAT solver * is a computer program which aims to solve the Boolean satisfiability problem", has nothing to do with the SAT aptitude tests.
Re: Accidentally writing a SAT solver
#27Interesting post, but I’m not sure this really speaks to what goes into actually writing what would be considered a “fast” SAT solver. It seems more like a post about how SAT pops up in a lot of places if you look at them right. For the state of the art in what constitutes fast solvers, the annual SAT competition papers are quite interesting to read if you’re interested in the techniques people come up with to make t…
SAT turns up everywhere because it's almost universal kind of problem. Since it is NP complete, everything in NP can be transformed into an instance of SAT. Since P is a subset of NP, everything in P can be also be turned into an instance of SAT. Nobody knows if things in PSPACE can be, though.
Add to this that propositional logic (the language in which we express SAT) is a versatile language to code problems in. Finding cliques in a graph is also NP complete, but it is less natural to use it as a language to code other problems.
Re: Accidentally writing a SAT solver
#28On a related note, anyone have any advice for getting started with something like Z3?
It really helps to have a hard problem to solve in the first place. Try scheduling all the classes in a university timetable into available classrooms, subject to constraints like maximum seating and not double booking an instructor. Now try to add constraints like “art classes must be in a studio.” Then to make it really fun, “no more than one fourth of the Electrical Engineering classes may be taught outside of the…
And even better, consecutive tutorials must be in the same room or nearby rooms (tutors and teaching materials can't teleport), and there are two or three simultaneous sequences of tutorials in big courses (so consecutive tutorials actually can be in distant rooms if they're in different sequences), and the number of students requires that the university's rooms be in use 90% of the time, and medium to large lecture theatres must be in use 98% of the time.
This is an annual battle I engage in. The software sucks.
Re: Accidentally writing a SAT solver
#29Earlier quoted context omitted.
It really helps to have a hard problem to solve in the first place. Try scheduling all the classes in a university timetable into available classrooms, subject to constraints like maximum seating and not double booking an instructor. Now try to add constraints like “art classes must be in a studio.” Then to make it really fun, “no more than one fourth of the Electrical Engineering classes may be taught outside of the…
And even better, consecutive tutorials must be in the same room or nearby rooms (tutors and teaching materials can't teleport), and there are two or three simultaneous sequences of tutorials in big courses (so consecutive tutorials actually can be in distant rooms if they're in different sequences), and the number of students requires that the university's rooms be in use 90% of the time, and medium to large lecture…
It does, but better scheduling will only go so far at an institution that underinvests in classroom space. Between “looks fancy” and “meets instructional needs,” donors prefer to have their names on “looks fancy” every time.
Re: Accidentally writing a SAT solver
#30[dead]