Tech Talk

SoC Wrap-up

2010-08-07T18:38:00.000-04:00

Supercharging SymPy's Assumptions -- that was the task for my SoC project this year. So how far has it come? Well there were three substantial pushes I'll outline here:

Removal of Old Assumptions

By a decent margin, this was the most time consuming task, and likely the one that will see the least contribution to SymPy's code-base. The conversation as to how best strip out SymPy's old assumptions continues, and my foray into the mess can be found in [these] [two] branches (the latter being the most recent and promising).

Despite the possibility of this code not making it into the trunk, this task served as a vital in-depth introduction to the SymPy system as a whole, and gave me a far greater understanding of SymPy in general than I could have hoped by simply browsing the code-base. It also brought some of the issues with the assumption system to the forefront for discussion, which will hopefully continue beyond the bounds of the SoC timeline.

SAT Solver

Probably the most effective use of my skills, I implemented a new SAT Solver from the ground up for SymPy. It's got an effective heuristic, the ground work for clause learning, and advanced SAT solver data structures. I've spent a fair bit talking about this on the blog already, so I won't go into further detail here. But [this] is the branch, and here's how it stacks up against the old DPLL solver (note that the y-axis is log scale):

Knowledge Compilation

  This here is a fuzzy term used to describe pre-computation that helps in online queries. There's a large body of research when considering queries in boolean logic, and I've had some experience dealing with such things. In fact, [this line] in SymPy could be considered something along the lines of knowledge compilation for the assumption system -- it pre-computes the CNF of the known rules so that queries to the ask function don't need to compile them every time for the logical inference.

  Well we can take this a step further. And that's precisely what [this] branch does. One thing it does is [explicitly store] the CNF so it's not computed at import time. This is accomplished by copying the output of [this function] to the ask.py file. So now we have a simple CNF ready to go whenever the SAT solver is invoked to answer an ask query.

  Beyond this simple compilation, there is more we can do to completely avoid calling the SAT solver -- if we can answer the query quickly, there's no sense in calling the full DPLL algorithm. This is accomplished by pre-computing all of the implications from single assumptions -- see [this dictionary]. An entry such as 'Q.imaginary: set([Q.complex, Q.imaginary])' should be read as, "If we know it's imaginary, then we know it must be complex and it must be imaginary".

  Simple, I know, but it saves us from calling a sat solver simply to find out that a variable is imaginary if we assume it's imaginary ;). Well maybe that would be captured by [this line], but successive implications are all compiled down, so this does save you a fair bit. How much? Well running 'bin/test sympy/assumptions' on the trunk calls the SAT Solver 811 times while this branch cuts it down to a mere 258. Granted we now have a faster SAT solver, but why use such a big hammer when the query is simple?

  The method also captures things like ask(x, Q.imaginary, Assume(x, Q.complex, False)) -- if Q.imaginary was true, then Q.complex must be true (because of the lookup we pre-compiled), and since we know this isn't the case, we can conclude that x is not imaginary as well. How are these facts compiled? Well we do the exhaustive checks with the SAT solver ([this line]), and dump the results just like the pre-computed CNF.

So these were the dives into SymPy this summer. As I mentioned earlier, the first may not see the light of day (in the SymPy trunk), but the second two have been merged to a unified branch, [here]. It's been rebased on top of the current SymPy trunk, and is ready to go for testing / tampering. I'll be sending it around to the sympy-patches list, and putting notes of it up on the relevant issues. Hopefully by the firm pencil down date (August 16th), it'll be in shape for inclusion to the SymPy core. So please play with it, and let me know what you think.

???

The concern of caching everything (in the presence of assumptions) came up for the removal of old assumptions. One thought was to disable caching altogether, but it seems vital for the efficiency in some of the more advanced features of SymPy (integral calculation, etc). But would happen if we enable the cache as soon as a SymPy call is made, and disable / flush it when the computation is done? This would allow things to be cached within a single computation, but since assumptions don't change mid-way, we would avoid any bad-cache hits.
Do [these rules] all make sense? They look good to me, but like anything pre-compiled they should have some more eyes on them ;).
Assume(x > 1) is a missing puzzle piece thus far. Since ask can be called with any arbitrary expression (which is subsequently decomposed), this becomes increasingly more difficult to figure out. At a high level we want to be able to compute all of the primitive assumptions (ie. Predicates) for an expression, given a more complex expression. So for ask(x, Q.whatever, Assume(x > 0)), we would ask the Gt class to answer things such as, "is x Q.positive?" which would return True iff "0 is nonnegative". But this is just a specific case, and like I mentioned things get complicated with complex assumptions on more than one variable. How do we get from here to there?

(Note: This wasn't really part of the SoC plan, but I don't intend on stopping work on the assumptions after next week.)

Who's Watching the Watch Literals?

2010-08-07T00:25:00.000-04:00

**Yes, I just made a bad Watchmen joke, and no I haven't seen the movie yet ;).**

  So far we have seen how the general DPLL procedure works, along with clause learning and a fancy heuristic. If we were to profile the solver, we'd find that most of the time at this point is spent doing unit propagation -- especially when we start adding clauses, unit prop triggers constantly. So that is precisely what watch literals are used to speed up.

  The concept of watch literals was born out of a realization as to when exactly a clause is unit-prop'd -- this happens when every literal but one in a clause is set the wrong way. For a while solvers tried just counting the number of literals left to be set in a clause that isn't satisfied, and whenever this went from 2 to 1, you know it's time for unit propagation. Well since we only really care about that specific point (going from two unset literals to one), we will explicitly keep track of those two -- they are our watch literals.

  Every clause that remains to be satisfied will have two watch literals associated with it. But the clause doesn't store this information, those literals do. So instead of keeping track of which clauses are yet to be satisfied, we keep a list of clauses for each literal such that the literal is one of the two watch literals assigned to that clause. And what happens when we set a variable? Well we only need to look at the clauses that the literal's negation is watching, and pick a new watch literal for that clause. An example:

Say we have the clause (x | y | z) and x / y are being watched.
If z was set (regardless of direction), we don't need to do anything for this clause -- not even consider whether or not we should do anything (since updating clauses is done by enumerating z's watch literals).
Say on the other hand that we set y = False instead of z. Well this clause has y as a watch literal so we would find a new watch literal to replace y -- namely z. After storing a pointer to this clause in the watch literal list for z, we continue with the search.
Now assume z was set to False. Again, we would check out this clause since z was a watch literal, but this time find that we can no longer find an alternative -- this triggers unit propagation.

  So now the clause is satisfied, but what happens to our watch literals? This is the beautiful part -- nothing. Sure, if x is set False later on, we'll check the clause again, but we only update watch literals when the clause isn't satisfied (quick linear time check to see if a clause is satisfied).

  But what happens when we backtrack past the decisions for y and z? This is the /really/ beautiful part -- nothing again. The clause will go from being satisfied to unsatisfied (but we aren't keeping a flag for this anymore -- remember that satisfiability of a clause is a linear time check), but we still have two watch literals set (x and z). Sure, these are different watch literals than what we started with (namely x and y), but that's perfectly ok, and it's unbelievably fast -- all because backtracking doesn't need to update any of the watch literals.

  So that's basically it. Implementing things to work properly isn't the easiest (I've failed a few times before taking up the SoC project this year), but boy oh boy does it ever pay off (see the latter part of this post). So have watch literals gone in to SymPy yet? You bet.

That wraps up the series of SAT solving tutorials. I haven't covered everything that went into this branch, but I did touch on all the important points. I haven't come close to covering everything that goes into modern SAT solvers, but if you're interested, the Conference on Satisfiability would be a great place to start ;). Thanks for following along, and stay tuned for some further Assumption tweaks.

Clause Learning Flunk

2010-07-27T17:26:00.000-04:00

A few days back, I was on my way to write up a blog post detailing how impressive the new system is (and it /does/ have some great speedups in there). To be thorough, I wanted to show results for different parameters being disabled, but to my surprise I discovered clause learning was hurting. This flies in the face of everything we know about SAT solving, so the hunt for reasoning commenced.

Well long story short, the hunt continues but a likely reason is the lack of impact that the simple clause learning scheme actually has. Monitoring the clauses that cause unit propagation (a measure of how useful a clause is) reveals that the learned clauses aren't actually ever being used -- big-time bummer. It's because of this, I've disabled the conflict analysis in the latest version.

But results are still be be had. First off, how much better are we than the original DPLL solver, and how bad does the clause learning actually hurt? Well the answers are (roughly) pretty good, and not much ;). Here's a graph plotting the run-time for the three approaches (-CA means clause learning was disabled):

Note that the y-axis is on a log scale, so the differences are actually more drastic than they appear. Take-away: the new sat-solver is doing great, and the clause learning doesn't hurt that much...just doesn't help like we'd expect.

Next up is the impact of watch literals. I'll have a blog post in a day or two for the final installment of "what goes into a SAT solver", and the focus will be on watch literals. The introduction of this data structure hack heralded in a wave of killer SAT solvers, and they helped out here too. The following is a comparison (with clause learning disabled) between using watch literals and not using them:

Oh, and it should be noted that when points don't exist, it's because the solver just couldn't handle it in a reasonable amount of time.

So in the interest of actually letting SymPy users see these enhancements, I'm going to wrap up this week with that final post, and post-pone the clause learning investigation until more time is available. Next up is investigating how a truth maintenance system can be used to smartly cache queries to the assumption framework. If we can avoid repeated SAT queries (no matter how beefy the solver is), that's a win.

One final note, there will likely be an incorporation of an industrial SAT-solver interface for those who really want the power. This will be through the Numberjack Library, and be optional if you happen to have it installed. The start of it is in this branch, but we'll need to wait until the next version of Numberjack is released due to limitations it currently has.

That's all for now. Cheers.

Clause Learning and Heuristics

2010-07-23T14:34:00.000-04:00

Clause Learning

  Everyone should learn from their mistakes, right? Of course ;). Well SAT solvers are no different. If the solver discovers that the problem has no solution when a subset of the variables are set a certain way, then that is useful knowledge -- this knowledge is captured in the form of new clauses that are added to the theory.

  Now you may think that since we're doing a systematic search, we won't ever need that information again: for example if x=True / y=True / z=False led to an inconsistency and we backtracked to try other values of z, y and x, will we ever use the fact that (!x | !y | z) must hold? When using a static variable ordering, the answer is no. This is because if we backtrack, we will never see the same setting of variables again that led to the inconsistency. However static variable orderings are brutal :p.

  Let's expand on our example to see clause learning in a little more detail. Imagine the SAT solver went as follows:

Set x = True
From unit propagation set v1 = True and v2 = False
Set y = True
From unit propagation set v3 = False, v4 = True, v5 = False
Set z = False
From unit propagation we get the empty clause !!conflict!!

So what do we know? Well right off the bat x = v1 = y = v4 = True and v2 = v3 = v5 = z = False is enough to make the theory unsatisfiable (so solution exists with those settings). But remember that unit propagation is a sound procedure -- the variables v1 - v5 are all implied by setting x and y to True [0]. So really just the settings to x, y, and z are enough to cause the problem. How could we have avoided it? Well what if we had the clause (!x | !y | z)? Note that this is just say at least one of the variables was set different. If we had that clause to begin with, our search would have looked like this:

Set x = True
From unit propagation set v1 = True and v2 = False
Set y = True
From unit propagation set v3 = False, v4 = True, v5 = False, z = True
...

  So what we do is add the clause, (!x | !y | z), to our database of clauses and continue the search. Since we're backtracking, we'll set z=True anyways (the clause wasn't really needed), but in the future (say if we backtrack higher and go down another branch, we may face the same decisions. This is when the clause really becomes useful.

  Now the method I just described uses a very simple technique to figure out the clause it should create / add -- it picks the negation of all the decisions you've made so far. However there are far more complex schemes that are ongoing research. I may incorporate these into SymPy some day, but for now the default works great ;).

  Another common concern (which I'll avoid dealing with for now) is how to detect useless clauses -- eventually learned clauses are no longer triggering and just taking up precious cycles in the solving process (and memory too). Elaborate cache flushing schemes have been proposed (and still are being actively researched), but SymPy likely won't be getting to the point where that would be necessary.

  So that's all for clause learning. It's extremely helpful in the context of SAT solving, and is finally in our SymPy solver.

[0]: I won't go into detail here, but you get the same result if you set a number of variables and then do unit prop as if you interleaved unit prop with each variable setting.

VSIDS Heuristic

So behind any reasonable SAT solver is a great heuristic. Variable State Independent Decaying Sum (VSIDS) is one such heuristic. What does a heuristic do? Well at each node in the search tree, it should tell you what variable to set, and what to set it to.

VSIDS works by three main steps:

First it assigns a score to every literal (or variable setting if you will) matching the number of clauses that the literal appears in. So if a literal is in a large number of clauses, it will be picked before one that isn't.
Every time a clause is added, the literals in that clause get their score bumped up (by 1). Every time a clause is deleted, the scores get reduced (by 1).
At regular intervals, /every/ literal has their score reduced by a constant factor (divide by two is typical).

So what does this accomplish? Well at a high level it prefers variable settings that will satisfy the majority of clauses, and over time (through steps 2 and 3) it will prefer literals that will satisfy a large number of learned clauses. This has the effect of avoiding bad parts of the search space where a solution is unlikely to exist.

The SymPy solver now has VSIDS driving the search, with the one step of #3 missing (coming soon ;)). The beauty of VSIDS is how nicely it plays with the clause-learning of the SAT solver to make things exceptionally fast.

That's all for now. I'll have another post soon showing some recent results, and one more within the following week to describe the data structures that make all this possible.

Davis Putnam Logemann Loveland

2010-07-18T22:12:00.000-04:00

  Last post we saw what the problem of Satisfiability was, and specifically the form of input that we're concerned with handling -- CNF. In this post I'll describe the primary method of solving this problem that almost every modern SAT solver uses (and there are quite a few out there) -- DPLL (named after the authors).

  Before I get into the DPLL details, however, I should mention local search. There has indeed been some success over the years with local search algorithms when applied to the Satisfiability problem. The idea with these algorithms is to fix all of the variables (your candidate solution) and explore the neighborhood of candidate solutions found by flipping the value of a single variable. This is not what SymPy uses, nor will it, but it's worth mentioning for the sake of completeness.

  So...on to DPLL. This can be broken down into three main parts: the DP algorithm (which was out there before Logemann and Loveland came along), unit propagation, and the pure literal rule.

  The DP part of the DPLL algorithm is a systematic search through the variable assignments that follow from a few (somewhat obvious) facts about the boolean theory in CNF. At each stage in the search, the algorithm must 1. Pick a variable it is going to set next and 2. Decide what that variable should be set to. Why can we do this? Well any variable must be set either True or False in any full assignment.

  So say we've selected the variable x and decided to set it to True. Any clause that has the literal x is now guaranteed to be satisfied, so we throw it away for the next part of the search. Any clause that had the literal !x, on the other hand, must rely on one of the other literals in the clause -- hence we throw out the literal !x before going forward. After this, we now have a new theory that says nothing about x, and is simpler than the original one. We recursively call the DP algorithm for this theory, and if that fails (I'll describe how in a sec), we throw all those clauses and literals back in, and try again with x=False. If both fail, we return fail, and if we're at the root of our search tree, there doesn't exist any solution to the set of clauses.

  So what's our base case? Well if we have an empty clause in the theory, none of the literals in that clause can be satisfied (obviously). It seems silly to have a CNF with an empty clause in it, and you wouldn't expect one to be given to a solver, but through the solving process I've just described, they certainly come up all the time -- otherwise the problem would be far too easy to solve ;).

  So that's the DP algorithm. Simply a systematic search through the variable assignments where each search node in the tree is a variable selection and the branches are on what value at variable should take.

Unit Propagation

If you have a boolean theory in CNF, and there's a clause that contains only a single literal (recall that every clause in CNF needs to hold), the we know for certain that the literal must be set to True (if it's x, then set x to True / if it's !x, then set x to False). This is the premise behind unit propagation. It can be extremely powerful when doing SAT solving since it sets so many other variables after making a single decision (most of the time).

Essentially unit prop works by setting variables according to the unit clauses they appear in when any unit clause exists. Some unit propagation can cause other clauses to become unit, so the process continues to a fix-point. If the empty clause is ever generated, then you've found an inconsistency and you backtrack. When used with the DPLL algorithm, these variable settings found with unit propagation are considered implications of the last decision the search made. So when it comes time to backtrack, you don't go and try every opposite setting of a unit prop'd variable -- it would just be wasting time.

Pure literals

If you have a theory in CNF and a variable appears only a certain way, say positively, then if any solution exists we can be sure one exists with the variable set to True. This is the intuition behind the purer literal rule. A literal is pure, with respect to a boolean theory, if it's negation doesn't appear in the theory at all. When this happens, we can safely set the variable, and continue. If no solution is found, then we know that no solution would be found with the variable set in the opposite manner (since that would only make solving the problem harder by removing literals from clauses that still need to be satisfied).

The pure literal rule changes the theory, but it is sound in the sense that if any solution existed before, we're guaranteed at least one still exists. Despite this nice property, the pure literal rule is left out of most modern SAT solvers. It will be implemented in SymPy, but likely disabled by default. The reason for this is that the largest advancements (since the invention of DPLL in the 60's) to SAT solving are attributed to data structure improvements. Keeping around the info for efficient pure literal detection has proven to hurt more than help.

So that's the DPLL algorithm in a nut shell. Next time I'll describe clause learning and non-chronological backtracking -- another two significant advances for SAT solving that came in the 90's. After that, a little data structures talk, and the discussion (as far as what's going into SymPy) will be complete. Hopefully so will the solver for SymPy.

Cheers

SAT Solving -- The Basics

2010-07-17T00:09:00.000-04:00

So I've come to the realization that in order for anyone reading this to understand the concepts forthcoming, some level of SAT solving theory is going to be required. As such, I'll put up a few posts describing the basics from both the theoretical and empirical sides of things. So first up, the theory...

  I won't go into too much detail about the benefit of the problem of Satisfiability. It's the grand daddy of all generic problems that you can map some problem into (one of the original NP-Complete discoveries). It suffices to say that there's an absurd amount of "really difficult" problems in computer science that can be cast as a Satisfiability problem, and if you had an oracle that could solve these Satisfiability problems, you have an efficient means of solving all those difficult problems.

  So what is the problem of Satisfiability? Well you have a number of boolean variables to start with -- lets use x, y, and z to example -- and a well formed formula involving just those variables, negation (denoted by '!'), disjunctions (denoted by '|'), conjunctions (denoted by '&'), and brackets. Recall that a boolean variable can take on the value True or False. The disjunctions simply mean 'or', so (x | y) says that either x or y is True. The conjunctions simply mean 'and', so (x & y) says that both x and y is True. Further, we say that a literal is either a variable (eg. x), or it's negation (eg. !x).

  Once you have a big formula of these variables, and the symbols ! | &, the problem of Satisfiability is to find an assignment of those variables that satisfy the boolean formula. Some formulas can be quite simple, for example a solution to (x | y) would just require you to have either x = True or y = True. But some syntactic restriction on the formulas gives us something that most problems map easily to, but isn't so simple to solve -- the form most common for this is Conjunctive Normal Form.

  So we define a clause as a disjunction of literals -- for example (x | y | !z). A theory is in conjunctive normal form (or CNF) if it is a conjunction of clauses. This would be an example of a theory with one solution -- (x | y) & (!x | y) & (x | !y) -- both x and y have to be True, but that's not immediately evident from the formula. Note that if we add the clause (!x | !y) to the theory, then there exists no solution (ie. is is unsatisfiable or UNSAT).

  How might one go about figuring out the assignment of variables? Well one (foolish) way would be to try all 2**n combinations (where n is the number of variables) of truth assignments and see if any of them work out. This, however, is not practical for any reasonable size n. In fact, state of the art solvers today can solve problems with hundreds of thousands of variables and millions of clauses. In the next post I'll describe the classical algorithm that forms the foundation of almost all modern SAT solvers -- DPLL.

A quick update -- I've re-implemented the data structure used for the heuristic in the SAT solver. This results in about another 30%-50% speed up depending on the size of the problem (more pronounced on larger problems). By the end of next week I hope to have watch literals and clause learning both explained here in the blog, and implemented for the sympy solver.

???

My only question would be, does anyone have any questions? ;)

Day Delay

2010-07-09T17:13:00.000-04:00

This week has been quite crazy, and unproductive from a SoC standpoint. Well at least if that's measured in commits ;). I did manage to have a number of fruitful discussions with some SAT solving experts as to how the current approach can be approved, and I'll be writing a blog post about some of that tomorrow. And what's been keeping me busy? I'll be presenting my master's work (which is somewhat related to this summer's project) at a workshop on Monday. Stay tuned, the next few weeks should be lively.

Cheers

A Satisfying Week

2010-07-03T00:42:00.000-04:00

  Work switched up this week from the removal of the assumption system, to re-implementing a fast SAT solver. Granted, a good 11 commits went in to the removal of the assumption system to bring it to it's current state -- 7 failed / 9 exceptions over the entire project -- but these came early in the week, and the discussion on that branch continues on the SymPy list.

  The SAT-Solver re-implementation just barely made it to a workable state earlier this evening -- valid models are found for SAT theories and UNSAT ones are proven as such. The internal use of the SAT solver was switched to the new one, and all still runs fine (unit tests and whatnot). Beyond that, we need a way to measure progress, so I wrote a quick little script to benchmark SAT solving systems (and potentially heuristics within them if we'd like to compare those as well). The benchmark script can be found here. Basically it runs the systems against a number of random 3SAT theories created at the hardness threshold (about 4.25 clauses to every variable).

  So how does the new system compare? The following graph plots the original (dpll) against the new version (dpll2):

And where might the speedup be coming from? Well there are a few data structure improvements that save time at various parts of the algorithm, but the largest improvement is likely due to the inclusion of a heuristic. At the moment it is quite crude -- basically picking the literal that appears in the most number of clauses -- but it's enough to have a surprising impact. So far unit propagation is implemented, but the next step will be to incorporate clauses learning and watch literals. Both have been known to offer substantial savings for SAT solvers, and will likely do the same for SymPy.

One last thing to note -- the typical clause learning scheme in SAT solvers is 1UIP. However, AAAI is just around the corner and I'll be presenting some of my research there. Coincidentally there is some nifty new clause learning schemes being presented by some of the recent contenders in the yearly SAT solving contest, and I may take a stab at implementing their ideas if they are accessible enough.

???

Eventually things may be ported to cython. I've been trying to avoid anything /too/ pythonic (stick to using lists like arrays, simple sets, etc). Does there happen to be a set of "best practices" for programming in python with the intent of porting to cython at some point in the future?
What's some of the "hard core" assumption problems that the SAT solver in SymPy is actually the bottleneck for? I'd like to have some ultimate goal in mind rather than just trying to squeeze the speed out of the thing in random SAT theory comparisons.

Testing, testing, 1 - 2 - 3

2010-06-26T01:36:00.001-04:00

The SoC work this week consisted of a strong push to remove the assumptions, found in this branch. First step was to get the sympy core working, and that was achieved around this commit. From there I started picking off the surrounding systems one by one until today. I didn't get all the way, but I've fixed a number of substantial things along the way that the core tests just didn't cover.

Most of the intricate issues were raised not by disabling the assumptions used in testing, but modifying them to use the global_assumptions rather than local variable ones. Granted this did mean a large amount of re-write, and disabling of assumptions every time they were included, but a number of problems created by removing AssumeMeths have been brought to the forefront, and dealt with. Some were simple (for example saying that something finite is bounded), but others had me picking through winpdb hours on end to try and find infinite loops. As a result I've become much more intimate with the system, which I guess is a good thing ;).

As it stands, 1902 tests pass, 16 fail, and 41 throw an exception. Since I currently only have access to the netbook for testing (G20 is in town and the Uni is shut down), which takes 20-30min for a full run through testing, I won't be generating a commit-by-commit set of statistics this week. But needless to say, 57 issues is very low, and likely only a day or two worth of work at the pace I've been able to get to. Depending on what the mentors think, I may or may not continue pushing on this branch, but either way next week's post will focus on the SAT solver improvements ;).

So some major take-aways from what was done:

Assumption handling is now done and delegated mostly in the Expr class. Most things inherit from this, and so it is a logical place. In general when is_* is asked, we look for an assumption in the global_assumptions, then try an _eval_is_* function, and then possibly check sufficient conditions. Care was taken to avoid infinite loops, and many of the old assumption implications are present here.
At one point the cache was disabled, since certain expressions would be cached with assumptions, and then retrieved later during testing with a different set of assumptions (which is wrong -- it should be recomputed). This slowed things down horribly, but was still manageable until I hit the 'series' code earlier today. Countless objects are created and re-created in the gantz approach to calculating limits, and for the longest time I was looking for an infinite loop when in fact it was just deathly slow. This commit re-enables the cache, and flushes it out every time the global_assumptions are updated. A crude work-around, but quite effective since the number of assumption modifications is quite limited. The solution is still not ideal, but does the trick. In the future, it should only clear out the relevant parts of the cache when an assumption changes, and it will be a design decision as to whether or not calling Symbol('x') more than once should clear the cache of all expressions involving x or not.
When the caching is flushed or disabled, f(x) != f(x) where f and x are just symbols. The comparison is done on object hash's, and when a separate one is created because of cache issues they don't equal one another. This was a very ugly beast when trying to figure out why tests were failing.
AssumptionContext isn't all that smart. It now flushes the cache whenever an assumption is added or deleted, but at the very least it should avoid adding assumptions that are already there. Since AssumptionContext subclasses set, this should already be handled, so there's likely something funny going on with the Assume __eq__ operator.
The assumptions argument is still in the constructor of many objects. Gradually all parts of the code that use this are being changed to use global_assumptions, but the kwargs should still be brought in -- for example some objects look for an evaluate=True/False. In these cases, the **assumptions should be renamed to **options, and any code depending on specific assumptions should be stripped out.

???

Is there any way to use bin/test to get at a specific test case in a file? Some of the testing files take quite a while (on the netbook) to run through all the working tests to hit a failing one.
Whats the best practice (for sympy) on rebasing? I've neglected to do it thus far, and that may make things difficult come merge time. What's a typical recommended frequency?

Take Two

2010-06-19T01:29:00.000-04:00

So after struggling with the amalgamated attempt to merge assumption-rewrite attempts, it was decided that I should just restart from the single branch that's most recent -- Ondrej's removal attempt. To this end, and through subsequent discussion, the following is the game plan going forward:

Push forward as best I can to try and get my version of the branch down to a workable state with assumptions removed, with a deadline of next Friday.
Provide constant feedback on the state of the system throughout the week.
Move on to working on the new SAT solver next Friday -- regardless of the state of the branch.

So which me luck I guess ;). I'm unclear as to how far I'll get, but one thing for sure is that the next phase of SoC won't depend on the previous, and development on this assumption removal can happen concurrently since there is such a large disconnect.

Since I'll be trying to document the progress made, here's a list of the progress so far (since forking Ondrej's branch):

???

'git co HEAD~1' brings me back one revision. How do I go forward one?
In the current state, abs(Symbol('x')) returns x**(1/2)*conjugate(x)**(1/2). In a proper branch (eg. trunk), it returns abs(x). I can't seem to figure out what's going on here...assumptions shouldn't be involved, should they?

Plowing Forward

2010-06-11T17:47:00.000-04:00

This week I continued in my quest to remove the old assumptions. One key aspect of this process is removing it from the constructor of typical sympy objects -- under the new way of doing assumptions you should be creating an assumption context when anything out of the ordinary is being assumed.

As mentioned in last week's post, this week was spent pushing forward from the changes found [here]. As per a suggestion from Ondrej's last blog post, this is what the weeks commit history looks like:

Christian Muise (7):

Merge branch 'master' into disconnect-assumptions
Lots of fixes from this branch ( http://github.com/rlamy/sympy/commits/use-new-assump2 ) on the May 17th commits. Only those that mesh well with Ondrej's branch are used.
Changes from May 18th on this branch ( http://github.com/rlamy/sympy/commits/use-new-assump2 ).
Fixing some bugs with constructors that didn't allow the project to be installed / tested.
Minor import fix.
Removing the assumptions from the Pow object.
Trying to remove assumptions from the constructor of sympy objects, encountered an infinite loop some place.

Quite a decent summary ;). What isn't reflected there, is the loads of cherry-picking I managed to achieve. After getting a grasp of how to set up the local repos, and what sha1 I was actually looking for, I went through Ronan's commits one by one, and brought in those that made sense with the stuff from Ondrej's branch. Quite happy with how the whole thing works out, and in general it went off without a hitch.

To monitor the status of the branch, I've been keeping a tally of a few metrics from running a simple test (bin/test sympy/core): the number of tests passing, failing, errors thrown, and time. Together they give a rough indication of how things are progressing. I may write up a quick script that samples the history of the branch and plots those metrics -- might be a good way of monitoring progress.

Unfortunately the branch is currently in a hairy state with an infinite loop being caused (recursion depth on constructors). I think this may have been an issue that already existed with the changes put in for the 'Application' class (see this commit), and only revealed by fixing other problems in the code, but I can't be sure (see question 1 below).

So the removal of old assumptions seems to be taking longer than expected. This may require a rethinking of milestones, and hopefully I'll have a better handle on the projected time-to-completion by next week with the help of my mentor, and lurkers in the sympy channel.

???

The infinite loop actually occurs in a number of different ways during the testing (all related to the Application class I believe). An example of one such loop can be found [here]. A minimal script causing the problem would be to import re (from sympy), and try to execute that on an arbitrary symbol. I'm at a loss as to what's going wrong here...but hopefully someone with better sympy eyes can see the error with the narrowing down I've done.
Only one question this week -- it's a road-blocker for me...

Two steps forward, one step back...

2010-06-05T01:15:00.000-04:00

  So I finally got up and going this week with the code base according to last week's plan. It's been more of a learning experience than a productive one, but better now than later in the summer, eh?

  First off, the newly created branch you can track my changes on can be found [here]. The life of this branch will not extend to the knowledge compilation or SAT speedups, but simply for the disconnection of the old assumption system -- a task that's proving to be far more difficult than expected :p.

Two steps forward:
  The main thrust of the work done this week was to first branch the right spot from Ronan's work building off the predicate branch. Along with this, I merged in all of Ondrej's work, commit by commit [1].

  Second thing I did was to try and fix up some of the errors. Unfortunately my approach was way off base. After going through all the commits from Ondrej's work, I was under the impression that simple assumptions were things inherited from the Basic class (eg. is_Integer, etc), and these are overridden when appropriate (eg. in the Integer class). Commits such as this one gave me the impression that things like is_rational should have been is_Rational instead. Ditto with is_real --> is_Real. Because of this, I proceeded to include all of the basic assumptions (is_even, is_nonpositive, etc) in the Basic class, and fix all is_real to be is_Real.

One step back:
  Apparently the lowercase refers to assumptions that can be inferred through the assumption system / reasoning, while the uppercase refers to just a check for whether or not it matches the class. One step back.

Onwards?
  Well now that I've cleared up my misconception (props to Aaron for fielding the questions), I think the best next step will be to try and follow the history this branch takes. It naturally follows from the branch I forked in the first place, and doesn't stray so far from the changes introduced by Ondrej's work. Again, this will mainly serve to help me learn how the assumption framework is intertwined with the sympy core, and hopefully give a glimpse into how I can make the speedup this summer as seamless as possible.

???

With the removal of AssumeMeths (and Basic inheriting from it), the natural question is whether or not assumptions should even be passed in when creating symbols as is currently the case? If not, then should the .is_* be removed when * is even, real, nonpositive, etc?
It looks like the old assumptions did have some higher form of reasoning. Should that be mirrored in the new simple backend for the ask, refine, etc?

[1]: I know, I know -- why not use cherry-pick instead of manually applying changes? Well I wanted to make sure I knew what was going in, and I haven't fully figured out the cherry-pick command yet :p.

Assumptions: Out with the old, in with the new...

2010-05-25T22:30:00.000-04:00

Today marks the first day of coding for SoC '10, and to mark the date I thought it proper to post a summary of the community bonding period.

In general I've continued to hop my way through (multiple versions of) the SymPy code base. To document the progress, aim, and general process, I've started to piece things together on the wiki [ here ]. Sparse? Mostly...but by the end there should be a decent documentation on the inner workings of the assumption system on this page -- something that doesn't exist and could help substantially in the future.

That brings me back to understanding the assumptions. Historically the assumptions were done by initializing a number of primitive facts when a symbol was created (and possibly modified?). The new assumption system (a killer SoC project from 2009) changed the scene so that dynamic assumptions could be queried. This was done via 'ask' and 'refine' methods, but alas this process has proven to be a bit cumbersome (a problem my project aims to tackle).

However, before I can proceed to injecting some juice into the new assumption system, the old one needs to be phased out...gracefully. Now there has been no shortage of reasonable attempts to remove the old assumptions, and wading through them has been the main focus for me this month. It's still not crystal clear, but I'm getting close:

The old assumption system should be stripped out -- essentially the Basic class in SymPy should no longer inherit from AssumeMeths and the AssumeMeths should probably be removed altogether.
The same queries and usage should still work. This means explicitly handling things like is_integer and such on an on-demand basis and make sure that it isn't called by just creating an object.
Queries to 'ask' and 'refine' methods should use a static version of the old system that will (understandably) only work for a subset of the queries.
The 'ask' and 'refine' methods should have an argument 'use_new_system' (set as False by default) that can be enabled when we start to speed up the new assumption system.

Concurrently, there is a branch under review that introduces the notion of a Predicate -- a notion I'm very excited to see enter the SymPy mix since it brings things into language I'm more familiar with. My current direction is to wait for the Predicate system to enter the mix, and then start the old assumption strip by merging two of the techniques previously attempted. This direction, however, may change on a daily basis as I gain a better understanding of what's what.

As part of these weekly updates I hope to not only sum things up, but also raise some questions I'm currently facing. Maybe it will allow commenters to help clear things up, but at the very least it will help me figure out what questions I need to answer next.

???

With all of the branch hopping I'm doing, it's unclear to me how best I should bring commits together. I've dabbled in some mercurial project stuff (and lots of svn), but git repos with a large number of contributers is new to me. I have already figured out how to pull in and switch from branch to branch, but what I'm lacking is how to pinpoint certain specific commits (or range of commits) on one branch, and pull them into my own.
I'm trying to figure out a reasonable test suite to quickly get a gauge on the efficiency of the assumption system. This would help me measure the effectiveness (or the harm) that different changes have on the assumption system, but the question I'm faced with is where this test suite best fits. It doesn't really test functionality, but will simply serve to measure speed -- as such the default unit tests don't seem appropriate. If it belongs anywhere other than my local computer, where?

That's all for now. See you next week.

SoC 2010: Let the games begin

2010-04-27T14:29:00.000-04:00

I was accepted for a G. SoC position this year working with the SymPy project on something near and dear to my academic heart -- SAT solving and knowledge compilation. Needless to say, I'm pretty stoked and can't wait to bring my knowledge to speeding up the great library.

Feed for this summer's work (specifically) is [ here ] -- I'll be posting my progress on a weekly basis.

Cheers

Academic Genealogy

2009-11-20T10:59:00.000-05:00

Just ran my advisors through these two services and came up with this:

Twitter Trends

2009-10-07T09:47:00.002-04:00

Wow: http://trendsmap.com/

U of T Admissions

2009-07-21T10:13:00.000-04:00

On the topic of visualization, [this] just came across my feed reader this morning. The Toronto Star has someone doing a number of residential visualizations, and every once in a while something interesting like this pops up.

Reddit Visualization

2009-03-25T23:38:00.003-04:00

Just thought that anyone interested in visualization should give this [site] a gander. There are a number of different ideas implemented on the site, and all of them are really well done. Enjoy.

Scooping the Loop Snooper

2009-03-04T23:18:00.000-05:00

Found this nice little poetic proof on the internets a few days ago. This last semester I had the privilege of taking Computability and Logic with Stephen Cook and this just about sums up the punchline of the course:

(via this site)

SCOOPING THE LOOP SNOOPER
A proof that the Halting Problem is undecidable
Geoffrey K. Pullum
(School of Philosophy, Psychology and Language Sciences, University of Edinburgh)

No general procedure for bug checks succeeds.
Now, I won't just assert that, I'll show where it leads:
I will prove that although you might work till you drop,
you cannot tell if computation will stop.

For imagine we have a procedure called P
that for specified input permits you to see
whether specified source code, with all of its faults,
defines a routine that eventually halts.

You feed in your program, with suitable data,
and P gets to work, and a little while later
(in finite compute time) correctly infers
whether infinite looping behavior occurs.

If there will be no looping, then P prints out `Good.'
That means work on this input will halt, as it should.
But if it detects an unstoppable loop,
then P reports `Bad!' --- which means you're in the soup.

Well, the truth is that P cannot possibly be,
because if you wrote it and gave it to me,
I could use it to set up a logical bind
that would shatter your reason and scramble your mind.

Here's the trick that I'll use -- and it's simple to do.
I'll define a procedure, which I will call Q,
that will use P's predictions of halting success
to stir up a terrible logical mess.

For a specified program, say A, one supplies,
the first step of this program called Q I devise
is to find out from P what's the right thing to say
of the looping behavior of A run on A.

If P's answer is `Bad!', Q will suddenly stop.
But otherwise, Q will go back to the top,
and start off again, looping endlessly back,
till the universe dies and turns frozen and black.

And this program called Q wouldn't stay on the shelf;
I would ask it to forecast its run on itself.
When it reads its own source code, just what will it do?
What's the looping behavior of Q run on Q?

If P warns of infinite loops, Q will quit;
yet P is supposed to speak truly of it!
And if Q's going to quit, then P should say `Good'
--- which makes Q start to loop! (P denied that it would.)

No matter how P might perform, Q will scoop it:
Q uses P's output to make P look stupid.
Whatever P says, it cannot predict Q:
P is right when it's wrong, and is false when it's true!

I've created a paradox, neat as can be ---
and simply by using your putative P.
When you posited P you stepped into a snare;
Your assumption has led you right into my lair.

So where can this argument possibly go?
I don't have to tell you; I'm sure you must know.
By reductio, there cannot possibly be
a procedure that acts like the mythical P.

You can never find general mechanical means
for predicting the acts of computing machines.
It's something that cannot be done. So we users
must find our own bugs. Our computers are losers!

Graph of NP-Complete Problems

2009-02-22T15:59:00.002-05:00

Earlier today I found a neat visualization of the most common NP-Complete problems [here]. I don't quite enjoy the layout used for the graph, but the fact that the nodes / edges link to publications is a nice touch.

Master's Thesis

2009-02-10T13:36:00.025-05:00

The master's thesis is officially done. Final drafts have been reviewed, and all edits are made. I'm not going to make the whole thing public, but a fair bit of it may find its way into papers for future SAT conferences (with any luck).

I will, however, write a series of posts (to be cross-posted on a few blogs) that describes what I did: from the logic background needed to understand it, all the way to my final results. Before I get going on that, here's my master's paper as a wordle:

Yes, this is the new meme. I want to see all of your thesis' as a wordle. Same goes for anyone else who reads this with a thesis to share.

Cheers

The Springer GTM Test

2009-02-06T14:40:00.003-05:00

An update on my (oh-so-close-to-being-finished) master's thesis will be coming within a week or so. In the mean time, what Springer book are you?

If I were a Springer-Verlag Graduate Text in Mathematics, I would be David Eisenbud's Commutative Algebra with a view towards Algebraic Geometry.
I am an attempt to write on commutative algebra in a way that includes the geometric ideas that played a great role in its formation; with a view, in short, towards Algebraic Geometry. I cover the material that graduate students studying Algebraic Geometry - and in particular those studying the book Algebraic Geometry by Robin Hartshorne - should know. The reader should have had one year of basic graduate algebra.
Which Springer GTM would you be? The Springer GTM Test

Periodic Table of Visualization

2008-11-22T18:59:00.000-05:00

Quite a few of posts I write here have to do with my arbitrary quests to visualize things in my research. I still maintain that I don't want to focus on the task of visualization, but using it properly (and in innovative ways) is something I definitely will continue to strive for. Hopefully a publication or two will come out of it as well during my studies, but that'd just be a pretty perk.

  With that train of though in mind, I've been casually browsing through visualization projects for inspiration and a few weeks ago this came across my feed reader: A Periodic Table of Visualization Methods

  The site is actually a nice example of Metaphor Visualization, and its interactive nature makes browsing the different types quite accessible.

  Where's my visualization? Ya, ya its coming. Unfortunately there are some serious bugs with Ubigraph on 64-bit linux and whenever I try visualizing my search space with more than a few hundred nodes the thing freezes. I have an official bug ticket opened for the issue but I haven't heard anything from the devs in months. In the meantime I've been trying to think of how CodeSwarm can be used for visualizing 3-SAT solving properties. That'd be a fun one to see ;)

Palinode Thesis

2008-11-03T14:11:00.002-05:00

A friend of mine brought up a very interesting point on her blog: What if we had to write our thesis as a palinode?

palinode: A palinode or palinody is an ode in which the writer retracts a view or sentiment expressed in an earlier poem.

Now retracting any views within the same thesis is bound for failure, but it is an intriguing thought to try and figure out what your thesis would look like in poem form. The current state of mine as a haiku:

SAT problems are hard.
Dualization's an option -
I just can't prove it.

...and back to the thesis...

Learning From a Legend

2008-09-08T14:41:00.001-04:00

For my 5th and final course for my masters degree, I'm taking Computability and Logic with Stephen Cook. You might remember him from such theorem's as Cook's Theorem. :p

Essentially every person with a Computer Science degree has come across this nugget in one form or another (pioneering the great question of P = NP), and if you haven't then you don't have a real Computer Science degree.

Best part of the opening lecture - seeing the expression on Cook's face when asking the class what complexity class the problem of satisfiability is in. ;)