[stub for offtopicness]
Backtracking is not a fast SAT solver.
OTOH, you can't write a Boolean SAT solver without backtracking.
Accidentally writing a SAT solver
31–40 of 41 posts
Re: Accidentally writing a SAT solver
#32Earlier quoted context omitted.
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.
> Add to this that propositional logic (the language in which we express SAT) is a versatile language to code problems in
is it though? You can't express some basic loop in propositional logic, right?
Re: Accidentally writing a SAT solver
#33Earlier quoted context omitted.
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.
> Add to this that propositional logic (the language in which we express SAT) is a versatile language to code problems in is it though? You can't express some basic loop in propositional logic, right?
Loops are part of a coded solution, not the problem. With SAT you encode the problem / solution space itself.
Re: Accidentally writing a SAT solver
#34On a related note, anyone have any advice for getting started with something like Z3?
If you want to use Z3 with a .NET language, there is also this very useful file with examples of how to use the bindings:
https://github.com/Z3Prover/z3/blob/master/examples/dotnet/P...
The examples are in C#, but easy to adapt to other languages. I found them quite useful to write a program for symbolic execution in F# that calls Z3 to simplify conditionals, here is its interface to Z3:
https://github.com/constructum/asm-symbolic-execution/blob/m...
The bindings are perhaps a bit cumbersome, but rather easy to understand and work very well. Once you appropriately wrap what you need, you can forget about the bindings as well as avoiding SMT-LIB completely.
Re: Accidentally writing a SAT solver
#35Interesting 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…
Ok, we've taken the fast bit out of the title above. It's still a good post!
Re: Accidentally writing a SAT solver
#36[stub for offtopicness]
sorry this is not fast
Re: Accidentally writing a SAT solver
#37[stub for offtopicness]
Backtracking is not a fast SAT solver.
Re: Accidentally writing a SAT solver
#38[stub for offtopicness]
Re: Accidentally writing a SAT solver
#39Earlier quoted context omitted.
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.
It's a public university, donors are not a significant source of funding, and government funding has not increased commensurately with the number of students, which has gone up dramatically in recent years (mainly due to relative cost of living, so no guarantee it will last).
Re: Accidentally writing a SAT solver
#40Huh. As a UMD grad who faced this same problem, it's an interesting post. What I'll say is that their ECE (which CS does not fall into, idk how they do it) department advisors gave us updated 4 year plans every semester or so. It meant I never had to worry about not having the right classes to graduate. And we had to get permission for every class which while annoying meant my advisor looked over every major-specific class. I can't even count how many people I know or know who know that wasted upwards of years on classes that didn't count. None of that for me.
On the other hand, I remember for my acceptance (which wasn't too the ECE program) I had to pick classes before I could confirm going to UMD? I don't remember why but I remember panicking because here I am, a high schooler still, picking college classes that would set my next 4 years. I was even more terrified when my first ever class not only was I late because it was in the back of a basement, but the instructor made some comment about it not being the right class for engineers or something. It was, though. You fix this and other problems: 1. I started using the UMD provided schedule planner and some 3rd party ones, with multiple backups for when they'd fill up 2. I made an app that showed most buildings' floor plans completely offline. No more wandering around during stressful times. 3. I did try and make a tree of classes using prerequisite days scraped from the SoC, but it wasn't a regular expression so I gave up immediately.
The blogger like CMSC430 and I agree it was a good class though I had a different professor.