funsat-0.5.1: todo.org

* Sat todo file

* TODO Group paired result.x files into their own graphs.	   :GraphResult:
This would make GraphResult generate n graphs when n benchmark results are
available from both timestamps.  This is just another dimension of generality
that isn't hard to support.


* TODO resTrace field of resolution trace in solver can go
Why do I even need the trace?  I just need the original clause ids and the
source map, right?

* DONE Export and document defaultConfig			       :release:
  CLOSED: [2008-06-07 Sat 14:29]

* DONE Release initial version to hackage
  CLOSED: [2008-06-06 Fri 10:49]

* DONE Derive resolution proof of UNSAT in order to aid debugging      :feature:
  CLOSED: [2008-06-07 Sat 20:32]
This feature essentially enables the following one, or vice versa.

+Add Writer capability to the Funsat monad+
Just put it in the state record.

** DONE Write quickCheck tests for checker
   CLOSED: [2008-07-07 Mon 20:05]
Use a generater that will always generate unsat problems, then check them, and
make sure unsat core is correct too.

*** TODO [#A] Resolution.check has a bug.  Find it.		   :bug:ARCHIVE:

** DONE Add unique ids to clauses
   CLOSED: [2008-06-07 Sat 20:32]

** DONE [#A] Add unsatisfiable core extraction			       :feature:
   CLOSED: [2008-06-07 Sat 14:23]

Algorithm from DATE_2003:

1. Each time learned clause generated, clause's ID is recorded, along with
   each encountered "reason".

   So I should be able to simply assign IDs to each original clause and
   learned clause.  When I do the conflict analysis, each reason (by the
   invariant) already has an ID.  I record all of these and generate a new ID
   for the learned clause.

2. When unsat is determined, record reason for conflicting variable
   assignment.  That is, the clause that propagated the conflicting variable
   assignment must have been false, so record its ID.  [Is this true?  Suppose
   at decision level 0 bcp propagates -1 and 1 is assigned.  It propagated -1
   because some clause was entirely false except it had -1.  But 1 is
   assigned.  So, it must have been the clause was entirely false.  Hence the
   reason for the propagation of the last conflicting clause is the ID we
   should record.  QED.]

3. Before returning Unsat from the solver, record all assigned variables
   (which by construction are all at decision level 0) and their values, and
   record the IDs of the "reason" for each variable.

It should be sufficient to start with a linear trace of IDs along with the
final variable assignments (produced in step 3).  In particular, we don't need
all the literals of each learned clause at recording time.

** Correctness
@recursive_build@ reconstructs the clause corresponding to the input id.
First we build the final conflicting clause.  This clause must be false under
the terminating assignment.  Call this clause X.

If the loop terminates and no errors, clearly we have a proper proof.

If the loop never terminates, then X is never the empty clause.  But if
resolve() finds a resolvent, cl is always "smaller".  Since there are only
finitely many variables & reasons, we will get the empty clause or find an
error.

*** In check_depth_first, can we resolve on any lit in clause & get a clause
that is false?

Proof:
Assume SAT solver is correct.  Let l be in the last clause.  The antecedent
for l propagated -l (*), and therefore contains -l.  Hence we can resolve and
still get a clause that is false.

Suppose X is the antecedent clause for l in a clause Z.  By induction
hypothesis, Z is false.  Since X is the antecedent for l, X propagated -l (*).
... Hence, we can resolve on l preserving.

If we cannot, SAT solver is incorrect.  In particular, the assumptions marked
(*) are the ones guaranteed by the correct operation of the solver.

*** In recursive_build
  * recursive_build first bottoms out when it hits an original clause.

**** Original clause
Suppose cl_id is an original clause.  Then it is already built (i.e. should be
supplied to checker).

If not, the clause we're constructing corresponds to a learned clause.
Construct clause CL of first source.  (*) Then construct clause of second
source.  Resolve them into X1.  Resolve X1 with build clause of next source of
cl_id.  Resolve into X2...Xn.  Build and return Xn.

    [Both of these clauses are either reasons used or the conflicting clause
    used when generating the learned clause.

    Suppose the conflict clause has only two sources.  Obviously both must
    mention the conflicting lit.  Otherwise they would not be present.]

*** Invariants
INVARIANT: every variable in the final assignment has an antecedent.  This is
true if the SAT solver is correct.

INVARIANT: every variable in an antecedent (reason) is assigned.  Also true if
the SAT solver is true.

INVARIANT: All reasons are non-empty.  Duh, otherwise they could not have
propagated.

Therefore, if any of these fails, there might be an error in the solver/trace
generation.  So they should be reported as ResolutionErrors.

* DONE Add -funbox-strict-fields to the ghc-options			 :bench:
  CLOSED: [2008-06-06 Fri 13:49]
and see how it affects performance.

Did this long ago.  Minus the "see how it affects performance" part.

* DONE [#A] Remove stupid command-line options			       :cleanup:
  CLOSED: [2008-06-06 Fri 11:47]

* TODO [#C] Initial state for dynamic variable ordering should be
based on the number of occurrences of literals in the clause database at the
beginning, or something.  Some heuristic that puts important variables first
at the beginning, instead of starting out all at zero.

* DONE [#A] Remove the monad stack from bcpLit
  CLOSED: [2008-06-05 Thu 20:14]
There are three monads there!  Can we just write a single monad data type on
top of ST that has errors and whatnot?

Did this long ago.
** Result ...

* TODO [#K] On some problems, select is a bottleneck, much	    :heuristics:
more than bcpLit.  Even so, reverting to a static ordering gives worse
runtime.  So ... if we had a faster way of selecting the min, it would be
nice.

* TODO There is a bug in mkConflGraph				       :ARCHIVE:
mkConflGraph' is the old code that seemed to work, but it's much slower.

* DONE Bug fixed
  CLOSED: [2008-05-08 Thu 22:17]
** decision list wasn't reset on restarts
** propQ wasn't reset on restarts

* TODO Problem simplification
** Whenever we restart, remove the negations of all unit facts from each clause.

* DONE [#A] Debug clause learning
  CLOSED: [2008-04-24 Thu 15:57]
Currently, bugs.

** There is a confusion between reasons and actual assigned variables
When asking for the level of a variable in the current assignment, the
conflict variable should be treated specially -- it's at the current level.
Otherwise, you can just ask for the level of the variable.

Say the conflicting literals is -20.  Then 20 is in the current assignment ---
that's why -20 conflicts.  Now, suppose you expand a literal `x' whose reason
contains -20 -- that is, since 20 is true, -20 was in a clause which became
unit, and propagated `x'.  Asking for the level of -20 is wrong -- when asking
for the level of a *reason*, we always want the level of the corresponding
variable, so that we don't confuse it with the conflicting literal.

* DONE VSIDS bumping should happen for each variable encountered
  CLOSED: [2008-06-05 Thu 20:15]
while generating the learnt clause.

* TODO [#K] Recursive learning/parallel stuff

* DONE Learned clause deletion
  CLOSED: [2008-04-03 Thu 12:18]

* DONE Make "bad" bag use bitset
  CLOSED: [2008-03-18 Tue 10:11]

* 29 Feb 2008 16:43:29
I had to re-install GHC 6.8.1 for a reason that is not important.  I was going
to install 6.8.2, which I had to compile myself.  While waiting for that, I
worked on DPLLSat with 6.8.1.  My tests run in 5 seconds, without
optimisations!  Last night I was waiting 10 minutes.  And this is user time!
I have no idea why.  I did change the unit propagation code today, but only
making it do more work!

I'm going to install 6.8.2, and then put 6.8.1 somewhere else so I can switch
between them easily, somehow.  Weird, weird.

This could be explained by a different test distribution ...

* DONE Make unit propagation propagate with learned clauses too.
  CLOSED: [2008-03-18 Tue 10:11]

* TODO [#K] Incorporate stupid frequency-based decision heuristic      :ARCHIVE:

* DONE Implement clause learning but only after
  CLOSED: [2008-03-18 Tue 10:11]
watched literals, otherwise the number of times we have to walk the set of
clauses will really kill the runtime.

* DONE Change watched literal imp so that we only propagate assignments
  CLOSED: [2008-02-22 Fri 11:37]
that have actually been made since the last iteration; this saves time.

So unitProp (maybe rename bcp?) should take a list of literals to propagate,
and compute until that list is emptied -- sounds like a worklist algorithm!

* TODO Implement SAT-MICRO annotated clauses and literals	       :ARCHIVE:
instead of using the current dl (decision list).

* TODO Probably don't need the cnf				       :ARCHIVE:
and wch fields of the state.  Probably can get away with some watcher.

* DONE [#A] Make watched literals work as follows:
  CLOSED: [2008-02-22 Fri 11:38]
-- watcherMap: Map Lit [((Lit, Lit), Clause)]

** When l first added to assignment (either decision or propagation):
if -l is watched, then for each clause associated with -l, look at -l's paired
literal, q.  If q is undefined under the assignment, then:

  -- If q is a unit literal of this clause, assign q.

  -- If q is *not* a unit literal of this clause, stop watching -l and
starting watching some other literal of the clause.  (Choose next by removing
everything in the assignment from the clause, then picking a random element.)

Write this in terms of a list of newly-assigned literals, so one can recurse
at the end.
  

* DONE [#A] Change assignment representation to O(1)
  CLOSED: [2008-02-13 Wed 21:59]
** DONE Lits to Int
   CLOSED: [2008-02-02 Sat 11:55]