
Investigation of Efficient Heuristics for a
StateBased 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:002: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 CRAW funds or
continue on Oz. However, CRAW 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
DavisPutnamLovelandLogemann algorithms) to find solutions or certificates
of nonsolutions 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:304: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 DavisPutnamLovelandLogemann 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:304: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
BDDbased input structure. For example, branchpruning, 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:304: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 stuckatzero node in a logic circuit.

11 October 2006 near Rhodes 821, time: 2:303: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:304: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:304: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:304: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:304:00
Attendees: S. Weaver, S. Goyal, and A. Cross
15 November 2006 in Rhodes 821, time: 2:303: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:303: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:304: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 1213: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 1217 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 worstofbest
because 30 as first var
has produced best tree so
far.
    
1/10 232:30 3.5 ran/compiled results to Not sure if these trees
complete trees i decided to (worst, worstbest, 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:151: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:004: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:0020: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 onesidedly, changed and
ran script.

1/16 12:0015: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:301: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:3020: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:151: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:3011:00  Started analyzing variable patterns.

2:303:30  Started analyzing the variables.

5:306: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:408: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:0021:00 2 Compiling results of run I need to finish
ning all combos of three compiling the results.
variables.

1/23 15:0017: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:4520: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:0000: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 1330 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:153: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:309: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 heavytail 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, multifunction 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 threevariable 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 1315:00 2 Ran and analyzed results of combos plan to compare to shikha's
of 2 variables for slider 40 results later

1/26 1515: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 2123: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 1416: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 1718: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:3023: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:153: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:401:50 1 Created new slider from original
slider and unusual results.
Commented out each line and put
in tabular form.

2/6 3:005: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:452: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 nonzero 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 1820: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 1316: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:3023 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:151: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:207:15 1 Reformatted research notes
Vocabulary section started

2/15 4:205: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
preexisting 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 1921 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 1919: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 202 6 Continued drawing trees using just I found patterns in the treesthe
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:151: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 "hardcore" 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 1416 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 1315 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.
2301 2 Worked out details in psuedocode.
Started to implement.

2/21 1718 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:3019 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.
2123 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:302: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:151: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 2123 2 Started reworking the algorithm I am almost done with that, then
I need to rewrite the section of code

2/27 1418 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 2123 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 910 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:151: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 1920 1 Played around with the sbsat graphs
some more to try to understand them

4/23 1619 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 2021 1 Looking at code for other heuristics Will begin implementing next
to try to understand the code before
implementing VSIDS.

4/30 211 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 2123 3 Implementing VSIDS. It compiles and runs.
not compile, implementing VSIDS. I think it is correct.


09 May 2007 in Rhodes 821, time: 12:151: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 2123 2 Fixed error in VSIDS implement Will begin implementing
ation. Reread Berkmin heuristic Berkmin soon

5/8 1013 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 1819 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:3011: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.

