Investigation of Efficient Heuristics for a
State-Based Satisfiability Solver

Shikha Goyal, Anne Cross, John Franco
Department of Computer Science
University of Cincinnati, Ohio, USA

Supported by a grant from the
Computer Research Association
Committee on the Status of Women in Computing Research
and the
National Science Foundation

Meeting Notes

28 August 2006 in Rhodes 821, time: 12:00-2:30
Attendees: J. Franco and S. Goyal.
    The plan is to have both Cross and Goyal compile SBSAT on their laptop computers. This will make it convenient for them and J. Franco when discussing code and experimenting with new ideas. Right now, the best environment for compiling and running SBSAT is unix. For laptops, the best unix environment is currently linux.

The attempt to get Linux on Goyal's laptop during this meeting failed. The necessary step of repartitioning Goyal's hard drive failed because Goyal's laptop was unable to read the Partition Magic disk. Several disks were tried. J. Franco believes the laptop is too old and unwieldy to be of adequate service in this project and that it will have to be replaced if Goyal is to continue work on her laptop.

As a stopgap, Goyal will use a unix account on a university computer called Oz. SBSAT source was uploaded to Oz but we have not been able to compile it for mysterious reasons. All of the above took over an hour. We decided to complete this task at or before our next meeting with the help of the code's author who is better acquainted with this than anyone else on the project. It is up to Goyal whether to replace the laptop using CRA-W funds or continue on Oz. However, CRA-W funds will not be available for some time so we have no choice but to continue on Oz for the near future anyway.

The remainder of the meeting was spent discussing the Satisfiability problem (the class of problems that SBSAT is designed to solve). This included a brief introduction to Conjunctive Normal Form (CNF) Boolean expressions which Goyal understood completely. This was followed by a discussion of the input format SBSAT expects. The example used was Sudoku puzzles which SBSAT solves in the bat of an eyelash. Goyal understood the selection and meaning of Boolean variables as representations of integer variables and the construction of some of the clause constraints needed by Sudoku such as ensuring that exactly one of nine Boolean variables takes value 1 and all the other eight variables take the value 0. We did not attempt to formulate all the constraints for Sudoku but we did note that over 700 variables and 10000 CNF constraints were needed for every Sudoku puzzle and the only difference between puzzles is the addition of perhaps 30 single variable clauses. We also briefly discussed how search is used (for example, by Davis-Putnam-Loveland-Logemann algorithms) to find solutions or certificates of non-solutions and how a heuristic can have a dramatic effect on the size of the search space.

The SBSAT user manual, source code, and many examples were sent to Goyal and Cross in earlier emails.

The next meeting is expected to be around 17 September 2006 with Anne Cross and Sean Weaver and hopefully Michal Kouril (authors).

20 September 2006 in Rhodes 821, time: 2:30-4:00
Attendees: J. Franco, S. Weaver, S. Goyal., and A. Cross
    The purpose of the meeting is to acquaint Cross and Goyal with CNF Satisfiability, the Davis-Putnam-Loveland-Logemann procedure, and Binary Decision Diagrams. The concept of search space was discussed. It was shown how choice of variable and value during search can greatly affect the size of the search space. Examples from circuit testing were introduced. It was shown that a natural way to express circuit problems is to use functions of the form x = func(a,b,c..) instead of clauses. It was explained how important it is to reducing search space size to know which variables are independent and which are dependent. It was shown how independent variables are easy to determine using the functions above and harder if the input is translated to clauses.

Both Goyal and Cross have successfully compiled sbsat on their laptop computers. For next week they will try solving some "slider" problems using various preprocessing and heuristic options available in sbsat (switches on the command line). They will make a note of switch settings that result in the best performance on the slider benchmarks.

27 September 2006 in Rhodes 821, time: 2:30-4:00
Attendees: J. Franco, S. Weaver, S. Goyal., and A. Cross
    The purpose of the meeting is to continue discussion of SAT concepts and tools from last week. In addition several concrete examples were run on SBSAT. Attention was focused on various algorithms for preprocessing the BDD-based input structure. For example, branch-pruning, strengthening, existential quantification were discussed. Inputs were examined for patterns of variables in components to show some examples of exploitable input structures. We showed how preprocessing can recognize some input patterns and is able to reconstruct the original functionality of the problem using those patterns. This is especially true for the slider benchmarks mentioned above.

Goyal and Cross have yet to submit the results of experiments that were proposed last week. We asked them to do so when they get a chance. We asked them also to further consider using switches of sbsat in solving some problems with structure. Problems suggested in an AI book were discussed and Goyal and Cross were asked to solve them using SBSAT.

04 October 2006 in Rhodes 821, time: 2:30-4:00
Attendees: J. Franco (in part), S. Weaver, S. Goyal., and A. Cross
    We discussed building logic constraints for the game of Sudoku. In particular, we showed how to translate integer constraints to Boolean constraints. We considered more general logic formulations of various problems including how to detect a stuck-at-zero node in a logic circuit.

11 October 2006 near Rhodes 821, time: 2:30-3:00
Attendees: S. Weaver and A. Cross
    J. Franco and S. Goyal were unavailable for this meeting and A. Cross was able to spare only 30 minutes before leaving for a special event. The time was used to determine whether the students were gaining traction on the project.

S. Weaver told Anne that she needs to be communicating with Weaver, Franco, and Shikha more. He explained the assignments we give them are not like homework. Rather we expect the students to use the assignments as a springboard to developing important insights that will come in handy later. The experiments should be designed to target specific questions and conclusions reached, where possible. Weaver reminded Cross to stay in communication with the rest of the group, to email us, or to stop by whenever she has questions. Cross says she feels lost right now and Weaver suspects she may subconciously be trying to slip through a crack. He said contact of more and 1 hour a week is needed to get Cross unlost.

18 October 2006 in Rhodes 821, time: 2:30-4:00
Attendees: S. Weaver, J. Franco, M. Kouril, S. Goyal, and A. Cross
    Goyal and Cross expressed frustration at not knowing what they should be looking for. Weaver, Franco, and Kouril explained they could be looking for a hard "core" of slider problems. That is, a relatively small piece of a slider problem that is about as hard to solve as the original. The idea is to eliminate the "noise" of components not contributing to hardness so we can see what the hard structures look like. Weaver walked Goyal and Cross through thinking processes that would lead to finding hard cores. This was done using the SBSAT tool. As a byproduct, Goyal and Cross were shown how to set up a search heuristic manually by manipulating recognizable directives in the input file. It is my (Franco) personal opinion that this session was by far the most successful in leading the students toward meaningful results thanks to the clarity and thoughtfulness of Weaver's presentation. I sense Goyal and Cross are finally are track now. We eagerly await, with great expectation, the results of student experiments scheduled to be discussed next week.

25 October 2006 in Rhodes 821, time: 2:30-4:00
Attendees: S. Weaver, J. Franco, M. Kouril, S. Goyal, and A. Cross
    We discussed the results of experiments done to satisfy queries made last week. Suggestions were made to design better experiments and to better present results. Results obtained so far were inconclusive. However, this is to be expected and hopefully suggestions for improvement will lead to significant progress in future weeks.

In addition, we heavily discussed what the SBSAT preprocessor does and how to make use of it to help solve problems efficiently. This includes a complete discussion of all the command line options available to the user of SBSAT.

1 November 2006 in Rhodes 821, time: 2:30-4:00
Attendees: S. Weaver, J. Franco, S. Goyal, and A. Cross
    We changed the notion of hard "core" to represent a collection of variables which, when set to particular values, results in an easy formula. With this notion Weaver spent a considerable amount of time showing Goyal and Cross how to use SBSAT to locate a hard core for slider problems. Many experiments were suggested and some were tried. However, hard cores remained illusive. In any case, Goyal and Cross have a much clearer understanding of how to use SBSAT as a research tool to answer this question. We expect they will continue these and propose new experiments in the next week. At least, by next week they will tell us the best "top" variable to branch on for a 40 variable slider problem. Hopefully, we can get results for the best 2 or 3 "top" variables to branch. Depending on how these experiments turn out, we may have to augment the tool to allow dynamic reordering of "top" variables to help locate a core. This is just a thought for the future. Right now we are going to see how much mileage we can get out of the tool as it currently exists.

8 November 2006 in Rhodes 821, time: 2:30-4:00
Attendees: S. Weaver, S. Goyal, and A. Cross
    To be written.

15 November 2006 in Rhodes 821, time: 2:30-3:00
Attendees: J. Franco, S. Goyal, and A. Cross
    Progress as reported is slow but steady. Cross has developed some control scripts for generating numerous runs of SBSAT and has used those scripts to determine best initial variables. By next week the outcome of these experiments should provide more insight into the structure of the core as described in the meeting of November 1. At this time we also divided the task into two clear directions: continuing with finding cores as above and to return to finding clause subsets that are cores as well. The second task was assigned to Goyal.

22 November 2006 in Rhodes 821, time: 2:30-3:30
Attendees: S. Weaver, J. Franco, S. Goyal, and A. Cross
    Cross described the results of experiments indicated in the November 15 meeting. The results sounded really great in that it will now be possible to compare decisions made by the current SBSAT heuristic with decisions that would lead to the shortest search space for small sliders at least. More time will be needed to process the results. These will be posted when ready. This aspect of the research sppears to be quite satisfactory at this time. Goyal still needs some help in getting results on her half of the project. Weaver continued earlier tutorials on ways to eliminate variables from expressions, for example by using existential quantification. We look forward to Goyals results next week.

11 January 2007 in Rhodes 821, time: 3:30-4:00
Attendees: S. Weaver, J. Franco, S. Goyal, and A. Cross
    Cross had compiled data on search space size for various runs of SBSAT with a 60 variable slider as input after carefully considering and selecting choices for the first few choicepoints. During the last week Cross analyzed the data attempting to discover patterns that will help us extend the experiments to increased numbers of selected variables. The longer term goal is to identify "hard cores" of subexpression for sliders. The idea is to select a few variables at the beginning of search to eliminate the "hard core." When the core is eliminated, the search space should be a small fraction of its unaltered (original) size. Although all of Cross's runs produced search space sizes that were not markedly different, Weaver observed that in some cases one or more search subspaces were small. We decided to use those small subspaces as a hint to finding additional selected variables that will make the other search subspaces smaller. Thus, when a small search subspace is found, the sequence of variables and assignments leading to that subspace will remain fixed and other subspaces will be attacked using other variables. Cross's assignment for next week is to run such experiments, identifying small search subspaces, and hopefully expanding the number of small subspaces based on that information.

Prior to the meeting Cross sent a pdf file showing all the handwritten notes she has generated from previous experiments. Those are available at http://gauss.ececs.uc.edu/CRA_SBSAT/cross_11.01.07.pdf. Cross also sent an accounting of time spent on the project during the last week. This is as follow:

   Date  Times   Hours         Activities                    Results
   ---- -------- ----- ----------------------------- ----------------------
    1/6 12-13:30  1.5  compiled results of running   Decided to keep going 
                       SBSAT on the several "worst"  with the worst to 4 vars
                       "worst" variables (for 2
                       variables). 
   ---- -------- ----- ----------------------------- ----------------------
    1/9  12-17     5   ran/compiled results for      bad! (increase in 
                       "worst" to 4 variables &      choicepoints from 3550
                       went thru results looking     to 16097), decided to
                       at best/worst choosing        try alternating best/worst
                       worst at each level           and choosing worst-of-best
                                                     because 30 as first var
                                                     has produced best tree so 
                                                     far.
   ---- -------- ----- ----------------------------- ----------------------
   1/10  23-2:30  3.5  ran/compiled results to       Not sure if these trees
                       complete trees i decided to   (worst, worst-best, etc.)
                       try last time                 are very useful.  Decided
                                                     to look at variable
                                                     position in slider to see 
                                                     if that seems related and 
                                                     see what happens when 
                                                     choosing only best var
                                                     farther down in tree.
   ---- -------- ----- ----------------------------- ----------------------
Goyal was supposed to report on similar experiments. Instead, the following email was received from Goyal:
     Hi Franco,

     Unfortunately I haven't really had any progress since the last
     time we met.  I finally got a feel for how this quarter is gonna
     be and I have made a schedule so that I can get in everything.
     With that said, I will be having a lot of time to devote to this 
     research project.  I apologize for any disappointment I am
     causing, but now that I'm caught up with all my classes and I 
     created a schedule, I have set times for when I will be working
     on research.

     I'll have results by Tuesday, so if you would like we could meet 
     separately as well that way I can discuss my results with you
     before our next Thursday meeting.

     I guess today we will learn some new material and go over Anne's 
     results?

     I really appreciate your patience with me.

     Shikha
Goyal was shown the time accounting of Cross and told to provide something similar from now on. Goyal was also reminded that this project is a great opportunity that she really needs to take advantage of. We will see what happens at the next weekly meeting which is scheduled for January 18.

18 January 2007 in Rhodes 821, time: 12:15-1:30
Attendees: S. Weaver, J. Franco, S. Goyal, and A. Cross
    Discussion was about results over the past week and direction for next week based on those observations. What follows are reports directly from the students:

Goyal:
    Obtaining data after commenting out one line at a time from the slider, the results that were abnormal from the rest of the results were used as starting points. Although the amount of data is little to make significant conclusions, it is a starting point that will be used to generate patterns based on all the results as a whole. Therefore using the lines that were abnormal, patterns between variable positions and variable occurence will be made. Using this analysis, to further attack the problem, clauses and lines will be removed to see which ones produce several solutions. The greater the number of solutions, the more significance they have in relation to the core. Using this information the exist command will be used to eliminate variables and see which variables in the line are part of the core.

Weekly Log:

Date       Time              Tasks                    To do:
------------------------------------------------------------------------------
1/15/07  12:00-4:00  Reacquainted myself with   Eliminate variables
                     clauses.  Set up format    Comment out more than one line 
                     of data.  Commented out    Eliminate variables based on analysis 
                     each line and put in       Create research binder
                     tabular format. Started    Work on more sliders
                     commenting on.             Make a script
------------------------------------------------------------------------------

Cross:
    Report contained in the detailed weekly log.
date     time     hrs        activities                        results
-------------------------------------------------------------------------------
1/15  19:00-20:00  1   Looked at past results (trees)  Chose 3 trees to compile
                       to figure out which ones are    data for once scripts
                       most lopsided and look like     finished.
                       the most promising to try to
                       do one-sidedly, changed and
                       ran script.
-------------------------------------------------------------------------------
1/16  12:00-15:00  3   Compiled data and looked at     Discovered some
                       results, tried to find best     combinations of 3 vars
                       variables for the small branch  that result in one brnch
                       of trees, then looked through   with 0 choicepoints; 
                       all previous data for other     decided to search for
                       instances where one branch was  combinations of 2 vars
                       zero.                           that give 0 choicepts
                                                       as a more systematic
                                                       way of creating a 
                                                       lopsided tree.
-------------------------------------------------------------------------------
1/16  20:30-1:00  4.5  Ran/compiled results of all     Discovered that for all 
                       combos of 2 variables & since   cases that I had already
                       none gave a zero, rewrote       found, the 3 vars
                       script and started it for 3     occurred together in an
                       vars; examined the structure    add_state1 in pos:1,2,6.
                       of the slider and locations of  Need to wait for script
                       the variables in the combos of  to finish to determine
                       3 that had resulted in a 0      if this is the case for
                       branch to try to find           all combos of 3 vars
                       similarities or patterns.       that result in 0 branch/
                                                       if all combos of 3 vars
                                                       that fall in those pos
                                                       result in a 0 branch.
-------------------------------------------------------------------------------
1/17  18:30-20:30   2  Restarted script for 3 vars     Discovered that when
                       since it had ended due to       when choosing worst 
                       computer error, looked at       vars, the var at the
                       slider structure more.          top does not appear
                                                       in same function as 
                                                       those at next level nor 
                                                       do the variables that 
                                                       are in the function
                                                       with the top level one, 
                                                       Noticed that all var 
                                                       assignments resulting in
                                                       0 choicepoints so far 
                                                       have form (+,-,?,?,?,-) 
                                                       need to wait for script
                                                       to finish for results of
                                                       combos of 3 variables 
                                                       and to run further tests
-------------------------------------------------------------------------------

25 January 2007 in Rhodes 821, time: 12:15-1:30
Attendees: S. Weaver, J. Franco, S. Goyal, and A. Cross
    Discussion was about results over the past week and direction for next week based on those observations.

Goyal:
    Goyal has identified some possible functions (lines) of Slider 40 that are in the hard core by observing changes in the number of solutions as they are individually taken out of the Slider. For next week, these functions, as a collection, will be tested for hardness. If hard, we will have a major advance. However, our expectation is that the group of functions alone will have far too many solutions to be deemed a hard core. In that case, Goyal has been encouraged to do a number of other things such as 1) instead of choosing functions based on increases in the number of solutions, choose them based on another criterion such as no increase; 2) attempt to find a small number of functions not in the group that can be added to the group to bring down the number of solutions. Franco believes 1 or 2 is necessary since there were a significant number of variables occurring one time in the set of functions that Goyal selected.

Weekly Log:

Date       Time              Tasks                   
------------------------------------------------------------------------------
1/23/07  9:30-11:00  - Started analyzing variable patterns.
        ----------------------------------------------------------------------
         2:30-3:30   - Started analyzing the variables.
        ----------------------------------------------------------------------
         5:30-6:00   - Isolated lines of file and figured out which lines
                       to attack.
                     - Looked at variable position on the lines and variables 
                       I was analyzing.
                     - Next step is to eliminate the clauses and find which
                       clauses are part of the core, then the variables using 
                       exist command in sbsat.
        ----------------------------------------------------------------------
         6:40-8:05   - Meeting with Anne.  
                     - Updated each other and explained what we have done
                     - Correlated each others data	gave some variables to 
                       look at.
                     - Anne ran some tests on those variables.
                     - Found error in my data, need to rerun the three lines
                     - Anne found that position of variable produces 0
                       choicepoints (unsatisfiable) for both sliders
                     - Compared analysis of variables from both results
------------------------------------------------------------------------------

Cross:
    Report contained in the detailed weekly log.
date     time     hrs        activities                        results
-------------------------------------------------------------------------------
1/22  19:00-21:00  2   Compiling results of run-     I need to finish 
                       ning all combos of three      compiling the results.
                       variables.							  
-------------------------------------------------------------------------------
1/23  15:00-17:30 2.5  Compiling results of run-     I need to finish
                       ning all combos of three      compiling the results
                       variables.                    in order to analyze them
-------------------------------------------------------------------------------
1/23  18:45-20:00 1.25 Meeting with Shikha.          Discovered similar 
                       Discussed what we have been   patterns in Slider 40
                       doing.  Compared results to   and Slider 60 for
                       try to find similarities, ran combos of 3 vars and
                       ran some tests on Slider 40.  noticed that some of
                                                     Shika's significant
                                                     vars are significant
                                                     for me too (low choice-
                                                     points).
-------------------------------------------------------------------------------
1/24  19:00-00:00  5   Finished compiling results,   Was unable to get a tree
                       looked through results for    with an entire side of 0
                       zeros until it became clear   choicepoints due to lmtd
                       that none of them deviated    availability of positive
                       from the pattern I had prev   vars that can be set to
                       noticed, played with drawing  result in 0 choicepoints,
                       trees to try to see if I      but it seems that vars
                       could get one with 0 choice-  13-30 are the most useful
                       points on one side of search  in attempting this because
                       node using these combs.       they all appear in the
                                                     combos of 3 vars as both
                                                     positive and negative.
                                                     When making these trees 
                                                     the total # choicepoints
                                                     did not decrease but was
                                                     dispersed into more branches
                                                     with fewer choicepoints,
                                                     not fewer branches with
                                                     more choicepoints.
-------------------------------------------------------------------------------

1 February 2007 in Rhodes 821, time: 12:15-3:00
Attendees: S. Weaver, A. Cross
    Discussion was about results over the past week and direction for next week based on those observations.

Goyal:
    Goyal's results are unspecified. The following is a log:

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
1/30   8:30-9:00  0.5   Anne informed me of her progress.
----------------------------------------------------------------------------------------

Cross:
    This meeting saw really good progress that will hopefully lead to the breakthrough we are looking for. In pursuit of heavy-tail search spaces, Cross, during the past week, noticed, from experiments on the 60 variable slider, that variable 30 can be inferred true in at least five ways: for example, by setting variable 1 to true and variable 13 to false or by setting variables 18, 32, and 47 to false and variable 34 to true. In other words, Cross discovered a way in which at least two functions interact with each other, and how to find, in some sense, multi-function conflicts: in doing so, she found a "zero" in the search tree that needs two functions to be realized. Since slider problems have the property that similar functions are replicated in many of a slider's functions, we expect this observation to lead to an efficient way to uncover numerous inferences. Cross will be trying to do this over the next week.

Cross's detailed description of progress follows:
    I started off by choosing three different trees that had many more choicepoints on one side than on the other from my results the week before. With those trees, I tried to continue to decrease the number of choicepoints on the smallest branch, and with two of the trees, I ended up with a branch with zero choicepoints after just three variables. Finding these branches with zero choicepoints reminded me that I had previously seen cases like this, so I went back through all of my previous data and found them. In all cases, the zero had resulted from a combination of three variables. At this point I had five cases where the result was zero choicepoints: {+30 -42 -59}, {-30 +18 -47}, {-13 +1 -30}, {-13 -30 +1}, {-58 -41 +29}. I decided to run sbsat on all combinations of two variables in order to see whether there were any assignments of just two variables that would result in zero choicepoints; there weren't. I also looked at the positions of the variables in each three-variable combination in the slider and noticed that for each of the cases, the variables would appear together in one of the add_state1 functions in positions 1, 2, and 6 (e.g., the starred positions in this: add_state1(*1, *13, 15, 17, 24, *30)). In addition, the true/false assignment for the variables in those positions was always the same: T in position 1, F in position 2, and F in position 6 (e.g., add_state1(T,F,?,?,?,F)). I am now waiting for the results of running sbsat on all combinations of three variables to see if the same pattern holds for all combinations of three variable assignments that result in zero choicepoints. I will then try to use the combinations of three variables to create a tree with all the weight on one side in order to try to find the core.

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
1/25  13-15:00     2    Ran and analyzed results of combos   plan to compare to shikha's
                        of 2 variables for slider 40         results later
----------------------------------------------------------------------------------------
1/26  15-15:30    0.5   Discussed my results of the prev-    I plan to compare my slider40
                        ious 2 hours with Shikha, we dis-    results with Shikha's results
                        cussed what we are planning to work  to see how the variables in the
                        on for the rest of the week          lines she chooses fall in any of
                                                             the combinations of two variables
                                                             that had very high or low numbers
                                                             of choicepoints, or whether that
                                                             seems to have any significance
                                                             at all
----------------------------------------------------------------------------------------
1/26   21-23:00    2    Tried to find combos of 4 variables  Decided to run a script on combos
                        resulting in zero choicepoints but   of 4 variables for a few hours to
                        was confused when the F branch of    see if I could find the pattern
                        the tree that printed when using     and figure out what was going on
                        print_tree seemed to give choice-    with the print_tree choicepoints.
                        points when I subsequently set 
                        those variables.
----------------------------------------------------------------------------------------
1/27   14-16:30   2.5   Compiled and analyzed results of     Found some combinations that
                        script on 4 variables.               resulted in zero choicepoints
                                                             but noticed that all contained
                                                             the combinations of three choice-
                                                             points, so decided to look at
                                                             equations in the slider to see
                                                             if I can figure out the combin-
                                                             ations that way and revisit the
                                                             print_tree method.
----------------------------------------------------------------------------------------
1/28   17-18:30   1.5   Looked at equations in slider and    Decided I need to look at the
                        found combinations of 6 variables    trees printed by sbsat again to
                        that result in zero choicepoints     try to determine combos of 4
                        for each of add_state1, add_state2,  variables.
                        and add_state3.
----------------------------------------------------------------------------------------                        
1/28  20:30-23:00 2.5   Figured out that the reason I was    I wasn't able to create a tree
                        getting choicepoints when plugging   with one zero side, although I
                        in the variables in the tree that    got closer than before. I'm not
                        led to F was that I hadn't removed   sure if it will be possible due
                        the print_tree statement from the    to the required T/F assignments
                        slider before setting variables,     to the variables.
                        so I now have combos of 4 variables. 
                        Tried to create trees with zero CPs
                        on one side from the combos of 3 
                        and 4 variables. Found  pattern for
                        combos of 5 variables resulting in
                        0 CPs, so I now have patterns for
                        all combos of variables resulting
                        in 0 CPs.  Attempted to create trees
                        from all of this info.
----------------------------------------------------------------------------------------

8 February 2007 in Rhodes 805C, time: 12:15-3:00
Attendees: S. Weaver, A. Cross
    Discussion was about results over the past week and direction for next week based on those observations.

Goyal:
    Goyal's results are unspecified. The following is a log:

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
2/6   12:40-1:50   1    Created new slider from original 
                        slider and unusual results.
                        Commented out each line and put
                        in tabular form.
----------------------------------------------------------------------------------------
2/6   3:00-5:05    2    Created new sliders for each set      Results from this day ended
                        of equations in the original slider   up being error
                        40.  Commented each line and put in 
                        tabular format.
----------------------------------------------------------------------------------------
2/8   12:45-2:00  1.25  Updated the group.  Found error in    <none recorded>
                        results for sliders created depen-
                        dent on defined equations.  Dis-
                        cussed Anne's results.
----------------------------------------------------------------------------------------

Cross:
    Cross's detailed description of progress follows:
    This week, I first decided to compare the results I got last week from running all combinations of two variables on slider 40 with the results Shikha had previously to see if there was any overlap. I noticed that the only overlap came where my results had given significantly low choicepoints (lower than 320). Several of these cases overlapped with the variables contained in the lines of the slider that Shikha had flagged as being possibly significant due to either high numbers of choicepoints or high numbers of solutions. Lines 12 and 29 each overlapped with two different combinations of two variables that I ran. None of my results that had given significantly high (higher than 700) choicepoints overlapped with Shikha's results, although this was mostly because those combinations of variables didn't tend to occur in the same line in the slider, so it was hard to tell if they actually would overlap when only one line of the slider was commented out.

Next, I spent some time looking at the slider (slider 60) and at my previous results to try to see if I could come up with anything new that I should look at in addition to the combinations of variables that were in more than one line of the slider and that would create conflicts when the variables were set appropriately. I wasn't able to think of any other good ideas, so I started going through the slider along with my results from before to try to come up with more combinations that conflicted. I was able to find several of these combinations, which I then tested to make sure I hadn't made any errors and to see what would happen when changing the truth assignments of the variables. Since so many variables were involved, I wondered if any of them would turn out to be unnecessary, but as expected, when the truth assignments were changed, the number of choicepoints rose above zero.

After finding these new combinations of 6 or more variables, I decided to use this along with my results from last week to try creating trees again. At first, I didn't seem to be having much luck, but then I decided to try working backwards to create a tree, and was able to create a large section of a tree that was all zeros. Unfortunately, the non-zero section of the tree seemed to grow faster than the zero section of the tree, so I don't think this is necessarily going to be useful. I had hoped that the variables that appeared in the tree would begin to overlap at some point so that I would no longer need to add new variables to create a new zero, but then I realized that if that were to happen, then the slider would be unsatisfiable. I plan to try this again, choosing different variables to start with, to see if I get the same variables each time in the zero section of the tree. I suspect that all of the variables will be more or less interchangeable in that they will all be capable of appearing in the zero section of the tree, in which case I don't know if this will be useful in finding the core. If the same variables continue to appear in the zero section of the tree, however, I think it will be useful.

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
2/5   18-20:00     2    Compared results of my test on all   I found six cases where a combo 
                        combos of 2 variables for slider     of 2 variables that I had flagged
                        40 with Shikha's results from        as being significant due to 
                        commenting out one line at a time    number of choicepoints overlapped 
                        to see if there was any overlap.     with a line that Shikha had flagged
                                                             as being significant due to either 
                                                             number of choicepoints or number of 
                                                             solutions. All of the overlapping 
                                                             variables were ones that had given 
                                                             low number of choicepoints in my 
                                                             results matched with lines that had
                                                             given either high number of choice-
                                                             points or high number of solutions
                                                             in Shikha's.  None of the variables
                                                             from my results that had given a 
                                                             high number of CPs overlapped. I am
                                                             not sure what this means other than
                                                             that those lines somehow seem to be
                                                             significant and would like to perhaps
                                                             compare again to Shikha's future results.
----------------------------------------------------------------------------------------
2/6   13-16:30    3.5   Looked at slider to try to look      I came up with several combinations
                        for more combinations of variables   of variables that appeared in 2 
                        that appear in more than one line    lines of the slider and that when 
                        of the slider and that could be used set appropriately resulted in zero 
                        to create conflicts/zero choice-     choicepoints. Changing the T/F
                        points or to see if I could come up  assignment of the variables resulted
                        with anything else that would be     in the number of choicepoints being 
                        useful to look at, then ran tests    higher than zero, so it worked for
                        on these combinations of variables   each case.  Next I will see if I
                        that gave 0 CPs to check, also       can use these results to create 
                        tested changing truth assignment     trees along with my previous results.
                        of the variables to see what happen.
----------------------------------------------------------------------------------------
2/7   19:30-23    3.5   Reviewed yesterday's and previous    I was able to create a tree that 
                        week's results hoping for some new   has zeros up to a point by working 
                        insights, tried to draw trees using  backwards. I had hoped that by doing 
                        the combinations of 3,4,5, and 6     this the variables required to get
                        variables from before along with     zero choicepoints would eventually
                        the new combinations of 6+ vars      start repeating so they were all
                        that result in zero choicepoints     in the tree already, but this 
                        those variables.                     doesn't seem to be the case. 
                                                             The parts of the tree without 
                                                             zeros seemed to grow faster than 
                                                             that with zeros, so either this 
                                                             won't work or I need to start with 
                                                             a different variable/use a different 
                                                             system for choosing combinations to use.
----------------------------------------------------------------------------------------

15 February 2007 in Rhodes 821, time: 12:15-1:00
Attendees: S. Weaver, J. Franco, S. Goyal, A. Cross
    In discussing results of the past week we hit upon an interesting idea that we wish not to reveal in public at this time but, if it works, will allow us to anticipate learned information reliably and therefore make a hard problem easier - potentially a lot easier. It is our task for next week to try this idea out.

Otherwise, the following summarize results over the previous week.

Goyal:
    Three meetings ago Goyal was given the task of checking to see whether the lines of Slider 40 that she identified as possibly being in the hard core actually seemed to comprise a large portion of the core. The test ended in an answer of NO because too many satisfying assignments resulted. It was determined that the reasons are: 1) many variables only appeared in one function; 2) some variables did not show up in the selected set at all. Goyal will modify how candidate functions are selected and tey again.

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
2/12   6:20-7:15   1    Reformatted research notes
                        Vocabulary section started
----------------------------------------------------------------------------------------
2/15   4:20-5:10   1    Made new sliders excluding add_states
----------------------------------------------------------------------------------------

Cross:
    Cross's detailed description of progress follows:
    I decided to focus on the second half of the slider (add_state2 and add_state3) this week since I had mostly been looking at the first half of the slider prevously. I started out by finding all of the zeros for the entire slider. Once I had those, I looked at them to try to see if there were any lines of the slider that had fewer zeros than the others or anything similar. I didn't find any. Then I looked at the T/F assignments for each of the zeros to see if there was anything in common between the zeros of each add_state function, or between the different functions, and as far as I could tell, there didn't seem to be anything. Then I began drawing trees for these zeros.

First, I drew a tree using the zeros from the first add_state2 line, starting with variable 30. Then I drew it again, choosing a different variable (the first given variable, 1) to start with. I noticed that there were patterns in the way the variables showed up in the tree. Then, I drew a tree using the zeros from the first add_state3 line starting with the first variable that was given, 13. I noticed patterns in this tree as well. The pattern that showed up in this tree was the same as the pattern that showed up in the add_state2 tree when I had chosen 30 to start. Then I tried to use the two add_state functions together to see if I could get one side to zero out completely. I was unsuccessful, but I did notice that the same pattern that was in the original add_state2 tree continued in the tree once I added variables from add_state3. I then decided to try adding zeros from add_state1 onto my add_state2 tree to see if that would work. It didn't, but the same patterns in the tree continued.

Then I decided to try creating a tree from the add_state1 zeros using the same method as I had for add_state2 and add_state3, which was just going line by line in my results for the combinations of variables that gave zero choicepoints. I thought this might help me create a more useful tree than my previous method of choosing whichever combination of variables seemed to create the next zero most quickly. Using this method, the tree for add_state1 did show some patterns, like for the other two, although they weren't as regular. Then I tried to rearrange some of the variables in the tree to try to get the patterns to be more regular, but I only succeeded in creating new patterns in the rearranged variables, not patterns that matched pre-existing patterns.

I started to wonder how different ordering of variables would change the patterns in the tree, so I started drawing trees with different variables. I have drawn trees for add_state2 starting with 3 different variables so far, and two of them have the same patterns.

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
2/12    19-21     2     Found all zeros for second part of    There are a lot of different T/F
                        slider (add_state2 and add_state3),   assignments that give zero choicepoints
                        looked at results for patterns or     for add_state2 and add_state3.
                        anything else useful.                 No zeros appeared that required
                                                              variables from more than one line to
                                                              be set simultaneously.
----------------------------------------------------------------------------------------
2/13  19-19:30   0.5    Looked at zeros some more, started    Laptop battery died and power was out,
                        to draw tree	                      had to wait for the power to come back
                                                              on to continue.
----------------------------------------------------------------------------------------
2/14    20-2      6     Continued drawing trees using just    I found patterns in the trees--the
                        variables from each add_state         same combinations of variables with
                        function individually and then        the same T/F assignments showed up
                        combined, compared the patterns in    multiple times in the same tree, and
                        the trees, tried to create more       continued to show up if variables from
                        patterns in the trees by selecting    a different line were added to try to
                        variables differently                 zero out the parts that weren't zero
                                                              from the variables in the first line. 
                                                              Similar patterns occurred when I tried
                                                              to use the zeros from the first half of
                                                              the slider (the add_state1 lines) to zero
                                                              out some of the branches. When creating a 
                                                              tree from the add_state1 variables only
                                                              using the same system (going through the
                                                              zero combinations for one set of variables
                                                              line by line), the tree didn't show as much
                                                              of an obvious pattern as did the other two
                                                              functions.  I was able to create more
                                                              patterns in the add_state1 tree by
                                                              rearranging variables, but they didn't 
                                                              occur as often as did the patterns in the
                                                              add_state2 and add_state3 trees.
----------------------------------------------------------------------------------------

22 February 2007 in Rhodes 821, time: 12:15-1:30
Attendees: S. Weaver, J. Franco, S. Goyal, A. Cross
    Goyal:
    Goyal has shown a desire to restart. We set out the following plan for recovery. Every day for the next week she will work on the project for 1/2 hour and then email franco what she did. Doing so will establish a routine that will hope will lead to 10 hours of work per week in 1 month. There are two tasks that Goyal will work on: 1) her original idea of identifying "odd" functions, based on performance relative to sbsat with the functions removed, for "hard-core" candidacy; 2) the idea we had hoped she would be working on from last week. Goyal has spent no time on the project this week.

Cross:
    Cross's detailed description of progress follows:
    On Monday, I met with Sean and we discussed how we would go about sliding lemmas, as well as which part I would work on and which part he would work on. After our meeting, I worked on writing out some pseudocode to try to figure out how I would do the actual sliding of the lemmas. Once I felt like I had the general algorithm more or less worked out, I began to write code and then continued to change other bits of my initial pseudocode and added things as necessary. I initially got a kind of slow start because I hadn't written much of anything in C to speak of in the past couple of years and I had to remind myself of the syntax, etc. I met with Shikha on Wednesday and discussed my code with her. She gave me some input and some suggestions since she had just had a class that involved programming in C last quarter. Then I continued working on writing the function and I now think I have the majority of it done, with the exception of a couple places where I have questions about the data that I will have available and a couple places where I know my code isn't entirely correct but just haven't fixed yet.

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
2/19    14-16     2     Met with Sean, discussed how we    I will be writing the SlideLemma
                        will go about sliding the lemmas.  function to slide a lemma,
                                                           given a list of variables in
                                                           the lemma and a list of functions
                                                           involved in the lemma be set
                                                           simultaneously.
----------------------------------------------------------------------------------------
2/20    13-15     2    Started figuring out how the        Need to work out more details
                       function will work, wrote out       of some of it, then implement
                       pseudocode generally, then
                       started getting more detailed.

        23-01     2    Worked out details in psuedocode.
                       Started to implement.
----------------------------------------------------------------------------------------
2/21    17-18     1    Fixed some errors, continued        Need to work out how to do the
                       implementing.                       parts I am still questioning,
                                                           figure out exactly where the
                                                           confusion comes from.
      18:30-19   0.5   Met with Shikha, discussed the      I noticed some things that aren't
                       code I am writing, Shikha gave      correct and I need to change,
                       me some suggestions since she       will work on that later.
                       has written C code more recently
                       than I have.

        21-23     2    Still working on SlideLemma.        Not done.  Need to continue
                                                           and figure out what I need to
                                                           know that I do not already know
----------------------------------------------------------------------------------------
2/22  0:30-2:30   2    Worked more on SlideLemma,          Need to check code/structs/etc.
                       clarified some questions that       on questions, fix some parts that
                       I have about existing               I know are incorrect and the
                                                           finish parts that are still only
                                                           pseudocode.
----------------------------------------------------------------------------------------

01 March 2007 in Rhodes 821, time: 12:15-1:00
Attendees: S. Weaver, J. Franco, A. Cross
    Goyal:
    Goyal feels she is unable to restart and has resigned from the project.

Cross:
    Cross's detailed description of progress follows:
    At last week's meeting I realized that the way I had gone about comparing the sets of functions to the set of functions in the lemma was not the best way to do so, so this week I rewrote the code to use a different method. I started out writing pseudocode again, and then I began changing the code that I had written. I got the code mostly done, I was almost able to compile it, although I just realized this morning that the reason for one of my errors was that one of the global variables I was using didn't actually exist, but rather I had just made it up while writing pseudocode since I didn't know if it existed. I need to find out if that variable exists. I also realized this morning that I had forgotten to account for the fact that the smurfs referenced might occupy more than one LemmaBlock, so that is something that I will need to go back and change.

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
2/26    21-23     2    Started reworking the algorithm     I am almost done with that, then
                                                           I need to rewrite the section of code
----------------------------------------------------------------------------------------
2/27    14-18     4    Finished up with the algorithm      
                       Started fixing up code that is 
                       still broken.  Started to check
                       some things in C to see how to
                       do them.
----------------------------------------------------------------------------------------
2/28    21-23     2    Continued working on code, fixed    I have a couple more things to fix
                       some errors, found some more.       but my code almost compiled and
                                                           I feel like other than the two things
                                                           I know of that need changing, it is done.
----------------------------------------------------------------------------------------
2/29     9-10     1    Fixed some more errors, realized    I need to change the code to
                       I had forgotten that the smurfs     account for that.
                       referenced might make up more
                       than one Lemma block.
----------------------------------------------------------------------------------------

02 May 2007 in Rhodes 821, time: 12:15-1:00
Attendees: S. Weaver, J. Franco, A. Cross
Cross:
    Cross's detailed description of progress follows:
    I have been working on implementing the VSIDS heuristic. First, I reviewed the code for the other heuristics to try to understand how things are done within SBSAT. Then I began implementing VSIDS. I had a lot of trouble getting SBSAT to compile at first, but once I found out my copy hadn't updated properly, I was able to get it running. I was then able to implement the VSIDS heuristic without much trouble. I got it running, and I believe that it works correctly.

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
4/18   19-20     1    Played around with the sbsat graphs 
                      some more to try to understand them 
----------------------------------------------------------------------------------------
4/23   16-19     3    Reviewed code for the existing        I need to look at the code more
                      search heuristics.  Reviewed the      before implementing the heuristic
                      VSIDS heuristic.
----------------------------------------------------------------------------------------
4/26   20-21     1    Looking at code for other heuristics  Will begin implementing next
                      to try to understand the code before  
                      implementing VSIDS.                   
----------------------------------------------------------------------------------------
4/30   21-1      4    Trying to figure out why sbsat will   I am still having trouble
                      not compile, implementing VSIDS.      even though I have the most
                                                            recent version of sbsat and
                                                            followed the instructions for
                                                            adding the heuristic for the things
                                                            that were not already there
----------------------------------------------------------------------------------------
5/1    21-23     3    Implementing VSIDS.                   It compiles and runs.
                      not compile, implementing VSIDS.      I think it is correct.
----------------------------------------------------------------------------------------

09 May 2007 in Rhodes 821, time: 12:15-1:00
Attendees: J. Franco, A. Cross
Cross:
    Cross's detailed description of progress follows:
    This week I fixed an error in the VSIDS heuristic I implemented last week, and then tried to check to see if it is working correctly, which I believe it is. I then started implementing the BerkMin heuristic and I am almost done although I still need to have it select the next branching variable from among those found in the current top clause if it is a lemma rather than the variable with the highest count, as it does in the other case.

date     time     hrs        activities                           results
----------------------------------------------------------------------------------------
5/7    21-23     2    Fixed error in VSIDS implement-      Will begin implementing 
                      ation.  Reread Berkmin heuristic     Berkmin soon
----------------------------------------------------------------------------------------
5/8    10-13     3    Implementing Berkmin.  Trying to     The basic part of the heuristic
                      find out how to "current top         is done but I am still working on
                      clause" in SBSAT.                    the important part of choosing
                                                           the branching variable based on
                                                           the current top clause.
----------------------------------------------------------------------------------------
5/8    18-19     1    Implementing Berkmin                 I still need check the "current top
                                                           clause" to see if it's a lemma and v
                                                           if so, choose variables from it.
----------------------------------------------------------------------------------------
5/9  9:30-11:30  2    looking through heuristic code       I think I figured it out so I
                      to try to understand how I can       will change my code next.
                      determine if the most recently
                      added was a lemma/what lemma.
----------------------------------------------------------------------------------------