OKlibrary
0.2.1.6

Picosat913
OKsolver_2002
SplittingViaOKsolver
Basic statistics for n=1132
Local search solvers
Upper bounds
Determining the best ubcsatalgorithm for palindromic problems
vdw_2^pd(6,6) = (567,1132)
Best local search solver
vdw_2(5,7) >= 260
Using SplittingViaOKsolver
vdw_2^pd(5,7) = (227,236)
vanderwaerden_2(6,7) > 1155
Best localsearch solver for palindromic problems
vdw_2^pd(6,7) >= (591,1156)
vanderwaerden_2(7,7) > 3703
Best localsearch solver for palindromic problems
vdw_2^pd(7,7) >= (1544,1547)
OKsolver_2002
march_pl
Picosat913
SplittingViaOKsolver
Local search
Best local search solver
vdw_2(5,8) > 330
Best complete solver for palindromic problems
Best localsearch solver for palindromic problems
vdw_2^pd(5,8) = (312,323)
Best localsearch solver for palindromic problems
vdw_2^pd(6,8) >= (655,1168)
Best localsearch solver for palindromic problems
vdw_2^pd(6,9) >= (943,1382)
Complete solvers
Parallelisation via SplittingViaOKsolver
Best ubcsatsolver
vanderwaerden_2(4,9) >= 309
vdw_2^pd(4,9) = (300,309)
vdw_2(5,9) > 472
Best complete solver for palindromic problems
Best localsearch solver for palindromic problems
vdw_2^pd(5,9) >= (446,473)
Problem specification
Using the canonical box translation
Using the 1base box translation
Using the "minimum" box translation
Overview
Using the canonical translation for the Sbox (6to4)
Using the 1base translation for the Sboxes (6to4)
Using the canonical+ translation for the Sboxes (6to4)
Using the canonical CNF translation for the Sboxes (6to4)
Using the "minimum" translation for the Sboxes (6to4)
vanderwaerden_2(4,10) > 328
vdw_2^pd(4,10) = (320,329)
vanderwaerden_2(5,10) > 668
Best complete solver for palindromic problems
Best localsearch solver for palindromic problems
vdw_2^pd(5,10) >= (595,612)
Overview
Using the canonical translation
Problem specification
Using the canonical box translation
Using the "minimum" box translation
Using the 1base box translation
Problem specification
Using the canonical box translation
Using the "minimum" box translation
Best ubcsatsolver
vanderwaerden_2(4,11) > 358
vdw_2^pd(4,11) = (343,348)
vanderwaerden_2(5,11) > 766
Best complete solver for palindromic problems
Best localsearch solver for palindromic problems
vdw_2^pd(5,11) >= (748,767)
vanderwaerden_2(5,12) > 962
Best localsearch solver for palindromic problems
vdw_2^pd(5,12) >= (950,963)
Best ubcsatsolver
vanderwaerden_2(4,12) > 401
vdw_2^pd(4,12) = (387,394)
vanderwaerden_2(4,13) > 569
vdw_2^pd(4,13) >= (519,538)
vanderwaerden_2(5,13) > 1204
Best localsearch solver for palindromic problems
vdw_2^pd(5,13) >= (1176,1205)
OKsolver
satz215
SplittingViaOKsolver
Palindromic numbers
vanderwaerden_2(4,14) > 681
vdw_2^pd(4,14) >= (617,682)
Problem specification
Using the canonical box translation
Using the "minimum" box translation
OKsolver
satz215
Splitting via OKsolver
vdw_2^pd(3,15) = (200,205)
Best ubcsatsolver
vanderwaerden_2(4,15) > 747
vdw_2^pd(4,15) >= (724,727)
OKsolver
satz215
minisat2
Splitting via OKsolver
vdw_2^pd(3,16) = (232,237)
Best ubcsatsolver
vanderwaerden_2(4,16) > 871
vdw_2^pd(4,16) >= (824,839)
vanderwaerden_2(3,17) >= 279
Palindromic numbers
Best ubcsatsolver
vanderwaerden_2(4,17) > 1112
vdw_2^pd(4,17) >= (855,1076)
vanderwaerden_2(3,18) >= 312
Palindromic numbers
vanderwaerden_2(3,19) >= 349
Palindromic numbers
Overview
Using the canonical box translation
Problem specification
Using the canonical box translation
Using the "minimum" box translation
Using the 1base box translation
Problem specification
Using the canonical box translation
Problem specification
Using the canonical box translation
Problem specification
Using the canonical box translation
Problem specification
Using the canonical box translation
Using the 1base box translation
Problem specification
Using the canonical box translation
vanderwaerden_2(3,20) >= 389
Palindromic numbers
Overview
Comparison of box translations
Using the 1base box translation
Using the minimum box translation
Using the canonical box translation
Using the canonical CNF box translation
Problem specification
Using the canonical box translation
Problem specification
Using the 1base box translation
Using the minimum box translation
Using the canonical box translation
Using the canonical CNF box translation
Problem specification
Using the canonical core round box translation
Using the canonical box translation
vanderwaerden_2(3,21) >= 416
Palindromic numbers
vanderwaerden_2(3,22) >= 464
Palindromic numbers
vanderwaerden_2(3,23) >= 516
vdw_2^pd(3,23) = (506,507)
vanderwaerden_2(3,24) >= 593
vdw_2^pd(3,24) = (568,593)
vanderwaerden_2(3,25) > 655
vdw_2^pd(3,25) = (586,607)
vanderwaerden_2(3,26) >= 727
vdw_2^pd(3,26) = (634, 643)
vanderwaerden_2(3,27) >= 770
vdw_2^pd(3,27) = (664, 699)
vanderwaerden_2(3,28) >= 827
Palindromic numbers
vanderwaerden_2(3,29) >= 868
Palindromic numbers
Problem specification
Using the canonical box translation
Using the 1base box translation
Using the "minimum" translation
Using the canonical CNF translation
Problem specification
Using the canonical box translation <u>l Translation of aes(2,4,2,4):
Problem specification
Using the canonical box translation <ul Translation of aes(2,1,16,8):
Overview
Using the Massacci DES translator
Using the canonical translation for the Sboxes (6to4)
Using the 1base translation for the Sboxes (6to4)
Using the "minimum" translation for the Sboxes (6to4)
Using the canonical CNF translation for the Sboxes (6to4)
vanderwaerden_2(3,30) >= 903
vdw_2^pd(3,30) >= (844,855)
vanderwaerden_2(3,31) > 930
vdw_2^pd(3,31) >= (916,931)
vanderwaerden_2(3,32) > 1006
vdw_2^pd(3,32) >= (958,963)
vanderwaerden_2(3,33) > 1063
vdw_2^pd(3,33) >= (996,1005)
vanderwaerden_2(3,34) > 1143
vdw_2^pd(3,34) >= (1054,1081)
vanderwaerden_2(3,35) > 1204
vdw_2^pd(3,35) >= (1114,1155)
vanderwaerden_2(3,36) > 1257
vdw_2^pd(3,36) >= (1186,1213)
vanderwaerden_2(3,37) > 1338
vdw_2^pd(3,37) >= (1272,1295)
vanderwaerden_2(3,38) > 1378
vdw_2^pd(3,38) >= (1336,1369)
vanderwaerden_2(3,39) > 1418
vdw_2^pd(3,39) >= (1406,1411)
Problem specification
Using the canonical box translation
Overview
Using the Massacci DES translator
Using the canonical translation for the Sboxes (6to4)
Using the 1base translations for the Sboxes (6to4)
Using the "minimum" translation for the Sboxes (6to4)
Problem specification
Using the canonical box translation
Using the 1base box translation
Problem specification
Using the canonical box translation
Overview
Using the Massacci DES translator
Using the 1base translation for the Sboxes (6to4)
Using the "minimum" translation for the Sboxes (6to4)
Using the canonical translation for the Sboxes (6to4)
Applying SplittingViaOKsolver
Systematic investigation of SplittingViaOKsolver for 1baseinstances
Problem specification
Using the canonical box translation
Using the 1base box translation
Problem specification
Using the 1base box translation
Overview
Using the 1base translation for the Sboxes (6to4)
Using the "minimum" translation for the Sboxes (6to4)
Using the canonical translation for the Sboxes (6to4)
Links
Partitioning into active clauses
Active clauses for field operations
The following needs to be updated.
Dictionary: (The following is outdated! "clause" > "active clause" and "clauseset" > "active clauseset")
Update with Concepts/plans/ClauseSets.hpp (transferring ideas from there to here or the other way around (?!)).
Partial assignment (see Concepts/plans/PartialAssignments.hpp)
Evaluation
Implied literals
Support for local search
Causes of conflict
Autarkies: What is an appropriate notions of autarkies? Easiest is to refer to some underlying clausemodel ?!
For a "strong ACLS" all above operations are polytime in the number of variables, and are always complete (no "unknow" for evaluation, all implied literals and equivalences, the changed total assignment is satisfying). XXX This should be now "active clauses".
Should we have statistics for an underlying clausemodel? XXX This seems to be the point of speaking of "active clausesets".
CNF versus DNF
Connections
Some further considerations
Finding the first arithmetic progression
The conjecture from [Granville 2006]
The first arithmetic progression allowing a missing number
Provide function for generating AES term
Standardise data types and documentation
Requirements
Add todos.
Use messages.
Complete input checking.
These classes should go into a number theory module.
Using a static member for the modulus in Zmodn is very crude.
Connections
Selecting the best algorithm
Finding best UBCSAT algorithm for Ramsey problems
Understanding local search algorithms
Finish implementation of InjectivityConstraints::TrivialAllDifferent<p>What is the concept for TrivialAllDifferent<PASS> ?
See also Concepts/plans/Variables.hpp and Concepts/plans/Literals.hpp. (Perhaps the value_type should always be ordercomparable?)
Test InjectivityConstraints::TrivialAllDifferent<p>Move the relevant parts from InjectivityConstraints/plans/general.hpp to here.
Old implementations: Perhaps the following tests can be reused?
AMO(L) (V is a set of boolean literals) as a (strong) active clauseset is very simple: As soon as one of the literals is set to true, all others must be set to false. This seems to be worth doing, and should be superior to other solutions. Of course, a problem is the interface for heuristics; easily boolean encodings can be simulated.
Overview on the different representations via clausesets:
Likely the ALOconstraint ("at least one") on boolean variables is not worth considering on its own?
Shall we abort this development?
Complete correct compilation:
Connections with other modules and parts
Design and implement class ComputeLargestAutarky (goes to Autarkies/Search/AnalyseTotalAssignment.hpp)
Design and implement class AutarkySearchUbcsat (goes to Autarkies/Search/AnalyseTotalAssignment.hpp)
AnalyseTotalAssignment.cpp
Including sourcefiles from external libraries: It seems reasonable to use e.g. include <ubcsat/reports.h>.
Complete autarky search
New file structure
Changing UBCSAT
Integrating/assimilating UBCSAT
Stylefiles
Partially moving repository Annotations:
Latex macros
Bibtexdatabase
Overview
minisat2.2.0
Addition
Subtraction
Multiplication
Division
Organisation
Generators for unsatisfiable uniform and variableregular hitting clausesets
Searching for ABD(n,k) (via SAT)
Rules for ABD(n,k)
Properties of ABDs
Connections
Estimating the factors in the infinite GrosswaldHagisproduct
DONE (providing proven intervals containing the true value) Controlling the error of C_gh_hp(k,max_p,decimal_digits)
Improving the GrosswaldHagis estimation
Arity
Refinement for iteration:
Precise formulation of ConstantSequence:
Once implemented, use Concepts::FullyConstructibleLo (two times) to express the concepts.
Requirements atomic conditions
Empty and full
Refinement for size: A refined version of AtomicConditions has
Changing atomic conditions: Removal and addition of single values seems to be basic (but not for bool).
Evaluation: Regarding evaluation of literals, for two conditions x, y the evaluation of x relativ to y is interesting, regarding y as specifying the domain: If y <= x, then return true, if y intersect x is empty, then return false, otherwise return indeterminate:
Write semantic tests.
ACL2
Prover 9
Maude
Firstorder theory of the reals
Vampire
Floors of logarithms
Positional (polyadic) representations of numbers
ext_integer_partitions
Unordered integer partitions
Install Axiom
Install OpenAxiom
FriCAS
Naming conventions
Aldor integration
Test system
Documenting the code
Input checking
Literature review : NEEDS UPDATE
Write first outlines
DONE Naming conventions
Graph concepts
Subgraph concepts
Naming conventions
DONE (Moved to ComputerAlgebra/Satisfiability/Lisp/Generators/plans/RandomClauseSets.hpp) Random boolean function
Notions and abbreviations for ringframes
Notions and abbreviations for modules and generalisations
The notion of a "latin square"
Properties of latin squares
Enumeration and classification
Counting
Connections
The notion of a biclique partition
Combinatorial matrices
Directed graphs
Abbreviations
The notion of a "biclique"
Abbreviations
Maximal biclique
Notions and notations
Partial groupoids, and extensions
Different forms of tests
Complete the tests
Organisation
Basic notions
Conversions
Symmetric matrices
Duality and polarity
Lists instead of sets
Naming conventions
Polar hypergraphs
Notions of "finite functions"
Representing boolean functions by their truth tables
Algebraic normal form
DONE (we just use full clausesets) Boolean functions represented by sets of satisfied/falsified inputs
resolvable versus resolvable_p
Renewal
DP
resolution_closure_cs
min_resolution_closure_cs : DONE
rt2lrt_il
Generating all binary trees
Catalan numbers
Random binary trees
Test the archetypes etc.
Write FullyConstructibleLt.
Write FullyConstructibleLo.
Use OKlib::Concepts::convertible_to_bool.
Write semantical tests.
Organisation
Class SetAlgorithms::Disjoint
Connections
Basic operations for boolean functions
OBDDs
Smurfs
Links
Prepare benchmarks for SAT 2011
Boolean functions representing binary addition
CNF and DNF representations of binary addition
Smallest prime CNFrepresentation
Smallest r_1based CNF representation
Smallest r_2based CNF representation
Concepts for bipartite graphs (with two vertex types), transferring as much as possible the concepts from the boost graph library. Related matrices: "reduced adjacency matrices".
Operations for changing bipartite graphs: Adding / deleting edges, and adding / deleting vertices (from both parts), and the corresponding undooperations.
Literalclause graphs and vertexhyperede graphs yield bipartite graphs; for the former we have special relations between the literals (via the underlying variable).
It seems, that the concept of bipartite graphs is (yet) most important as concept ("notion"), while models are provided only via hypergraphs and clausesets, where the bipartite graphs are directly "embedded" into the data structure.
Clarify the relations to module Graphs (see Graphs/plans/Graphs.hpp).
Clarify the relation to Hypergraphsconcepts (see Hypergraphs/concepts/plans/general.hpp).
Class BPass0
Computing the clashing variables in PassClashes
Partial assignment output adaptor
Adaptor ApplyPassAdaptor
DONE Application ApplyPass
Write application tests for ApplyPass
Random boolean functions
Random boolean functions in 10 variables with 64 true points
Random boolean functions in 16 variables with 256 true points
BDD's
Aiger
ABC
Translations to SAT
Boolean functions
Logic synthesis
Improve documentation for Espresso
Some errors when building 1_52_0
DONE (updated path to bjamsources) Update to version 1_48_0
Update Boost installation
Documentation
distance versus size
What kind of range exactly?
Notifying the boost email list about the missing functionality.
Should go to module GeneralInputOutput.
Purely local branches
Problems with branch rijndael:
Tutorial on branching : DONE (basic principle are understood; needs to be transferred to the documentationdocument)
On branching (in our situation) DONE (fixed a reasonable procedure; needs to be transferred to the general documentation))
Connections
The notion of "branching program" (BP)
Translations into (boolean circuits):
Improve locality
Setting userdir
Connections
Representing "cardinality constraints"
Direct realisations
Simplifications
Application of partial assignments
Atmostone as a CNF
Implement sequential counter by [Sinz 2005]
Allow repeating literals for unary_bb_crd2fcl
Improved understanding/implementation of BBmethod
Add statistics functions
Docus
Implement addercircuit translation
Cardinality constraints as active clauses
Implement other methods using unary representation
DONE Rename functions related to unary encoding
DONE Functions such as cardinality_totalizer_cl should take cardinality constraints
DONE Provide complete specifications (related to unary encoding)
DONE Change specification of variables in cardinality_cl etc.
Upper bounds
Lower bounds
Create milestones
Data
Perform analysis using additional variables
DONE The notion of a "certificate"
Implementation certificate_vdw_p(L,n,P)
Conversions
Analysing certificates
Verification of rresolution refutations:
Stronger proof systems:
Test script: We need some test system for the build system. Optimally, it would run like our normal test system; perhaps this is hard to achieve, but at least we need a list of manual checks, well specified, which cover all functions of the build system, and which is performed from time to time (manually). Then we can partially automate it.
Different environments
Basic decision problem
Encodings
Problem formulations
Active clauses?
Iterated finite functions
Planning: Discuss the relations to planning problems
Is there some C/C++ library for chessprogramming?
Generalised chess
Completeness of generalised chess
Connections
Boolean clauses, and more general clauses
Signed clauses as conditions
Sets of conditions? (Clausesets as special cases?) Big And resp. big Or ?!
Is usage of boost::distance effective?
Need "ReverseDimacs" application and clauseset adaptor
Document the basic concept CLSAdaptor
Discussing the basic concept CLSAdaptor
Write concept for InputOutput::Statistics class
Write tests!
CLSAdaptorFullStatistics
RawDimacsCLSAdaptor
Create "base class" for "raw adaptors"
Write generic tests for the concept (in module Concepts).
Write test for InputOutput::CLSAdaptorStatistics
Write test for InputOutput::RawDimacsCLSAdaptor
Write test for InputOutput::Statistics.
Update with
Shouldn't we differentiate between
Concepts for clausesets as collections of clauses, which are collections of literals, holding a reference to a domainassignment for the variables.
For an earlier attempt see OKsolver/Experimental/AllgKlassen200203/ClauseSets.hpp.
An important refinement is the concept of a "clauseset with history", which holds a reference to a structure consisting of a domainassignment together with a partial assignment refining it, and the state of the update process (how much of the partial assignment has been processed). Processed parts of the partial assignment may be transferred to the domain assignment. Clausesets with history support the reversal of the assignment process (controlled by the assignment structure).
Actually clausesets with history are only special cases of *virtual clausesets*, which support sat_status() (may return "unknown"), and which in general do not enable access to the clauses (which in general are "not there"). Active clausesets refine virtual clausesets by returning a partial assignment themselves (the set of unitclauses which the inference mechanism found; "strong active clausesets" infer all clauses of length <= 1). More generally for kactive clausesets sequences of derived clauses of length at most k are computed (so virtual clausesets are 0active clausesets).
Clausesets should allow efficient access to the related hypergraphs and graphs (so that we can use general hypergraph and graph algorithms; examples for graphs are the resolution graph and the resolutionsubsumption graph). This access should happen via simple wrapping of for example clauses or variables into node classes (the type of these node classes specifies the type of graph; no additional computations should be necessary).
The bipartite clauseliteral graph likely should be accessed through the hypergraphinterface. The two refinements "clausesets with history" and "clausesets with bipartite structure" should be independent of each other, and there should be a common refinement.
Clauseliteral graphs for clausesets should contain all possible literals; however for Pclausesets this is not sensible anymore, and so only occurring literals are mentioned, and they are connected to a new type of node, the value nodes (connected also with the variables).
An autarky for a Pclauseset is a partial assignment, such that for Pclauses which are not satisfied by the assignment no literal exists with a restricted set of satisfying values.
A virtual clauseset is like a dynamic constraint with the additional possibility of handling partial assignments; the sat_status must be 0 or 1 in case all variables have been fixed. But they have an underlying Pclauseset model, so that they can tell, whether the current partial assignment is an autarky or not, and so that they can perform statistical evaluations (the deduction mechanism must at least deliver what the underlying Pclauseset can (immediately) deliver, but might be (much) stronger).
An aliance of active clausesets owns the structure consisting of the domain assignment and the partial assignment (but this is controlled by external algorithms); by some strategy it processes (and potentially enhances) a given partial assignment (only when the partial assignment is completely processed by all active clausesets and no decision was reached, then the domain assignment finally gets updated). Learning (local or global) is controlled from the outside; in case of a "conflict" a resolvent may be computed (potentially compressed).
Links: See modules UnitClausePropagation and Learning for further thoughts on the concept of "active clausesets". And in SATAlgorithms/plans/GenericBacktracking.hpp the first prototype is being developed.
Sat status: For an active clauseset F,
Make the above concept definition more precise.
Write conceptcheck and conceptprototypes.
Write tests
Closures extended
Connections
Move todos from UnitClausePropagation/ClsAdaptorUCP.hpp here.
Relations to other modules
Reduction to graph isomorphisms
We also need the determination of the automorphism group of a clauseset, either explicitely listing all elements or giving a more compact representation (using some group theory software).
Applications
Connections to other modules
Greedy colouring
Relations to other modules
Organisation
Translations to SAT problems
Colouring by transversals
Generalised colouring problems
Greedy colouring
Positional games
Achievement and avoidance game
Improve design
Improve implementations
Generic translation
See "Iteration through lexicographical order" in ComputerAlgebra/Combinatorics/Lisp/Enumeration/plans/Subsets.hpp.
The implementation is not very efficient; improve it.
The design should be perhaps be iteratorbased.
The implementation is not very efficient; improve it.
The design should be perhaps be iteratorbased.
When transferring to OKlib:
With C++09 stdint.h likely is to be replaced by cstdint.
Testing CommonPart
Documenting CommonPart
Complexity measurements
Complexity functions in dependency on n
Usage of ProgramOptions.
Classes PrintStandard and PrintLatex should inherit from some common base class.
The output should contain a legend, and the date and time of the evaluation (and also the versioninformation of this program).
The common output facilities for ComputeScores and ComputeLexicographicalEvaluation should go into a separate submodule (and then used in these two programs).
Using the new module ProgramOptions (together with Messages).
General systems
Computational commutative algebra
Vicinity of computational group theory
Polyeders, matroids etc. PORTA and SMAPO at http://www.iwr.uniheidelberg.de/iwr/comopt/soft Code for [Bokowski, Computational Oriented Matroids] at http://juergen.bokowski.de, and other software.
The output should also contain date and time of the computation; and information about the program which produced the output (we need a general convention of how to make information about the compilation available to the program, so that via "version" we obtain as much information as possible).
The output should contain a legend.
See ComputeLexicographicalEvaluation.cpp for common functionality.
Using the new module ProgramOptions (together with Messages).
Perhaps the structure Scoring_from_file (in this file) should be generalised (it can be shared at least with ComputeAnalysis.cpp); and also the option handling could be shared.
The filedocumentation should contain some general explanations about the roles of the supplied metafunctions.
Transfer the tests to the new testsystem.
Perhaps a metafunction computing the concepttagclass from a concept class would be useful?
Should tr1/type_traits completely replace boost/type_traits.hpp?
Connections
0,1 versus false,true
Notions, names and abbreviations
snbl2cdn
Notions and notations
The basic "consensus" operation
Maximisation functions
The consensus iteration
Handling general graphs
Improving the implementations
Compute all maximal bicliques
constraint_backtracking
Heuristics
Further propagators
General idea
Data types and concepts
Naming conventions
Example
Move AES box translations into separate file
Update specifications
Remove hardcoding of multiplication by 01 in smallscale MixColumn
Rearranging linear components of Sbox and MixColumns
Write tests
Products
DONE Complex composition
Representations of the basic logical operations
Gluing operations
Improve Coq installation
Improve ocaml installation
all_irr_cores_bydef
sample_irr_cores
Finding an irredundant core of minimum size
Organisation : DONE
"Adaptive core search"
Exploiting the duality between MAXSAT and MUSAT
Connections
The distribution of arithmetic progressions amongst primes
The GrosswaldHagisformula
Computing the GrosswaldHagis coefficients C_k
Using curvefitting
k=3
k=4
k=5
k=6
k=7
k=8
Create submodule
Cryptographic properties of AES
Keys for which AES encrypts P to P
Connections
Terminology
New library (replacing Mhash)
Grain of salt
Create documentation
Argo DES instances
Kreuzer DES instances
DES generator
Overview
Constraint modelling languages
Sugar
Gecode
Minion
Mistral
Choco
Mozart
Eclipse
N Queens
Sudoku (only "big Sudoku", of arbitrary dimensions)
TAILOR
Local search
General content
Title
Journal
Structure
Create milestones
run_ubcsat as shell script
Input checking
Bad output should not be incorporated into the dataframe
Bad documentation of run_ubcsat
Better output of run_ubcsat
Add newubcsatokl as an option for run_ubcsat
Make run_ubcsat interruptible
Parallelisation
Elementary statistics
Only computing the transversal numbers
Elementary statistics for k=12
Only computing the transversal numbers
Elementary statistics for k=13
Only computing the transversal numbers
Elementary statistics for k=14
Only computing the transversal numbers
Elementary statistics for k=15
Only computing the transversal numbers
Elementary statistics for k=16
Only computing the transversal numbers
Elementary statistics for k=17
Only computing the transversal numbers
Elementary statistics for k=18
Only computing the transversal numbers
Elementary statistics for k=19
Only computing the transversal numbers
Elementary statistics for k=20
Only computing the transversal numbers
Elementary statistics for k=21
Only computing the transversal numbers
Elementary statistics for k=22
Only computing the transversal numbers
Elementary statistics
Only computing the transversal numbers
Local search
Elementary statistics
Only computing the transversal numbers
Predictions
Local search
Detailed investigations of Tr(ap(3,n_0)) for small n_0
Elementary statistics
Only computing the transversal numbers
Elementary statistics for k=4
Predictions
Elementary statistics
Only computing the transversal numbers
Elementary statistics for k=5
Predictions
Elementary statistics
Only computing the transversal numbers
Elementary statistics
Only computing the transversal numbers
Elementary statistics
Only computing the transversal numbers
Elementary statistics
Only computing the transversal numbers
Decision algorithms
Tree representations
Pebbling contradictions
Small variabledegrees in MU(1)
The heuristical function remlitocc_greedy
Creating marginal elements of MU(1)
Creating saturated elements of MU(1)
Creating all F in MU(1) with var(F) = V
Testing
Usage of demangle.h
Linkage
The outputfile should go somewhere in system_directories, like a subdirectory "data"; buildsystem support is needed here.
It seems that only because function OKlib::Parallelism::write_number is an inline function the program works? (If write_number would be a function, then we would have conflicting calls?? Or not  there is no static data?) (If inline were needed, then it should be a functorclass.)
What does yield really accomplish? Just giving time to the child (which was already start), or starting the child(ren)?
Later this should go the a subdirectory demos. Or to a subdirectory "examples" ? (It is not a demo for our library, but for another library?!)
It seems that boost::read_graphviz handles vertex names always as strings, and thus the dynamic property map needs to contain at least the map node_id?
Print out the vertex names.
The doxygenoutput of structure "process" is complete nonsense.
Complete the doxygendocumentation.
Write docus.
Write demos.
Connections to other modules
DONE (at least from a practical point of view the problem doesn't exist) What happens if the integers from the file are too big?
It must be tested, whether the integers can be safely negated
Improve class InputOutput::StandardDIMACSInput
Use Messages for messages.
Exceptions
Improving class InputOutput::LiteralReadingExtended
Error handling
ListTransfer
Write extended Dimacsparser for clausesets with nonboolean variables
Write Dimacsparser for weighted (partial) MaxSAT formats
Write higher level modules
Concepts
Implementation
Connections
Organisation
Heuristics, distances etc.
Concepts for heuristics
Write tests
Concept of a "domain association"
Hardness of primeextremal satisfiable general Horn clausesets
3 different representations of HIT(1)
Update to 12.12.1
Update to 12.2.1 : DONE (now outdated)
Update to 11.1.1.2
Update to 11.1.1 : DONE
Documentation
GraphDecomposition::Treewidth_by_enumerating_elimination_sequences
GraphDecomposition::Width_elimination_sequence
Greedy strategy
Boxdimension p=3 with direct encoding and three standard translations
Boxdimension p=4 with direct encoding and three standard translations
Boxdimension p=5 with direct encoding and three standard translations
Boxdimension p=6 with direct encoding and three standard translations
Direct encoding, weakpl translation
Direct encoding, weakpb translation
Direct encoding, dualweakpl translation
Direct encoding, dualweakpb translation
Summary
Overview
Encryption
Decryption
Update instructions
Connections
Complete the implementation
All isomorphism types of small groupoids
Enumeration and classification
Random generation of quasigroups and unital quasigroups
Trivial SAT algorithm
Improving the trivial algorithm
Variations
Measures
Design
Frameworks for genetic algorithms
Applications
The basic algorithm
Exact transversal hypergraphs (that is, Tr(G) = ETr(G))
Generalisation to boolean CNF
Exact covers
Base class
Exceptions module
A general standard for the messages of the exceptions is needed
By moving to the new test system it must become possible to find out exactly when the assertion in the failing test happens.
Describe what the tests test.
Links
Investigating dimensions
Open problems
Update experiment script
Move experiment data to investigationreports
Solvers to be used for experimentation
DONE (individual issues moved to separate todos) Prepare experiments for the SAT 2012 paper
Write application tests
Write docus
Connections
Update and extension : DONE
Better output for InputOutput/ExtendedDimacsStatistics.cpp : DONE
More convenient input
Improving efficiency
Generalising the computation
Using Messages
Improving output : DONE
Sat solvers on xxtended PHP clausesets
Hardness
Analysis of blocking structure
Parameter handling
Extended Dimacs format
Permutations
Complete doxygendocumentation
Write docus
Use Messages
Use ProgramOptions
Organisation
Write the following algorithm which systematically searches for an extension of an input hitting clauseset F: The input is enriched with Tr(F) (see (currently) HypergraphTransversals/DirectTransversalEnumeration.hpp), so that easily all interesting extensions by one clause can be considered by a visitor; of these only the nonisomorphic ones (that is, where the extended clausesets are nonisomorphic) are considered, and then recursively the algorithm tries to extend the clauseset further, until the visitor is "satisfied" (or no suitable extension exists). Either only the first solution is output, or all.
The first application of the previous algorithm is to find for k >= 1 boolean hitting clausesets with constant clauselength k and 2^k clauses, which have as many variables as possible. Interesting also the structure of the extremal clausesets (for example regarding symmetry). Instead of maximising the number of variables one can minimise the maximal variable occurrence. Also the total number of finally obtained clausesets is of interest (without removing isomorphic ones) in the context of determining precise probabilities for satisfiability of random formulas.
An interesting question is also how to extend 1regular hitting clausesets  here not just satisfying assignments are sought, but "exactly satisfying assignments". See HypergraphTransversals/plans/ExactTransversals.hpp.
Links
Boostdocumentation
GCCdocumentation
Further documentation
Literature review
Interesting good constraint representations
Comments in output
Create doxygendocumentation.
Use an CLSAdaptor for output
Write docus
Tools
Symmetries
Alternative translations
Generalisations
Add XOR translations for field multiplications
Move experimental todos to investigations
Generate good CNF hitting clausesets for the AES Field Operations
Prime implicate representations from hittingclsrepresentations
Find the symmetries of the AES Field Operations
Determine *all* prime implicates (for the purpose of analysis)
Test class FileIdentification.
Provide other languages with FileIdentification.
Add application tests
Weak implementation
Move CLSAdaptorFilter
Move to Ringframes/Fields.
Write tests for all functions provided
Complete docus
Demos
Maxima bugs
Missing functionality
Replacement of "makelist" by "create_list"
Basic concepts
Using Maxima expressions
Detailed examination of Peres33PointConfiguration.cnf
Testing realisability
Minimal configuration
Collaborating modules
Problems building 4.6.4
Incorrect .texifiles
DONE (not reproducible, taken as caused by some strange state of the computer) Failure building gcc412/gcc due to internal compiler error
Gcj
Providing gcc 4.1.2
Install GCC 4.5.3 : DONE
Loopoptimisation
DONE (gccbuilding provided first a corrected version, which was then removed) texi2dvi (texinfo 1.13a) fails to build gcc.texi on some systems
DONE (moved files into Programming/Specifics/Gcc/412) Putting "configure" under our version control
DONE (solved now  with build 4.1.2 only for C,C++) GCC 4.1.2 will not build on systems without GMP with MPFR support
DONE (we go directly to 4.5.2, to minimise problems with additional libraries) Install GCC 4.2.4
DONE (we go directly to 4.5.2, to minimise problems with additional libraries) Install GCC 4.3.5
DONE (we go directly to 4.5.2, to minimise problems with additional libraries) Install GCC 4.4.5
Installation in general
Connections
Update namespaces.
Update milestones.
Update todos.
Whatever remains of module DPv shall move here
The basic problems
Write docus
A Resolventclass
Relations to other modules
A general framework
Examing search landscapes
Theoretical random walk algorithms
Update namespaces.
Besides groupoids (see plans/Groupoids.hpp), what other algebraic structures are amenable for (generalised) SAT ? One would think of semirings (but associativity could be a stumbling block here), or structures related to finite geometries.
Connections
The notion of a "linear constraint"
Connections
Create milestones
Generalising positional games to SAT
Create milestones
Connections to other modules
General plans
Quadratic functions
Horn functions
Finite functions with full application of partial assignments
Andinverter graphs (AIGs)
File formats
Relations to other modules
Update plans:
Redesign
MaxSAT, weighted MaxSAT, and partial MaxSAT
Clauselists instead of clausesets
Better general naming conventions
Develop combinations of lookahead with conflictdriven solvers
Proof systems
Finding out "all properties" of an instance
Survey and belief propagation
Converting CNFs to DNFs
Organisation
Notions
Connections / Relations
Create milestones.
Extract the methods related to splitting trees
Shortest dual representations
Computations of all prime clauses for full clausesets
The notion of a "pseudoboolean constraint"
Application of partial assignments
Pseudoboolean constraints as active clauses
Add milestones
Create milestones
Create tests
Connections to other modules
Overview on generators for MUSAT
Create milestones.
Simplifications
Create milestones
Connections to other modules
Basic concepts
Basic backtracking algorithms
Representing solutions by finite functions
Perhaps only considering the simplest case
Write tests
Write docus
Bounded resolution
Create milestones : DONE
Create milestones
Organisation
Relations to other modules
Notions for symmetries
Bruteforce algorithms
Reduction to graph isomorphisms
is_isomorphic_btr_cs
Exploring symmetries
Homomorphisms
How to calibrate floatingpoint efficiency
Create milestones.
DONE Improving assert
Outline of the test system
Testing the demos
Improving the test system
Handling floating and bigfloating numbers
Create milestones
Write tests
Write docus
Relations to other modules
SAT translations
Create milestones.
Reorganisation
Concepts and abbreviations
Tree drawing (output as Latex code)
Graph drawing (output as Latex code)
Move special concepts to their new local places
Cannibalise the approach from 200203: Transfer if appropriate concepts from OKsolver/Experimental/AllgKlassen200203/ConceptDefinitions.hpp, and once finished, mark this file to be obsolete.
Develop concepts:
Develop a general strategy for creating generic tests:
Warnings: Eliminate all warnings.
Tests: Move to the new test system.
Technical problems when formulating concepts:
Complete the concepts and tests belonging to the standard:
Update namespaces
Update namespaceusage
General update
New test system
Update namespaces.
Concept design "Rooted trees with ordered children"
In a module GraphTrees rooted trees as Boostgraphs with one distinguished vertex establishing, while Parentgraphtrees additionally are equipped for every vertex with a property yielding the parent vertex (which in case of the root is the root itself).
Connections
Functions should not cache return values
Generating defaults constant for small scale
Generating polynomial representations of field operations
Sbox and multiplication boolean 6xm functions
Translating the constraintsystem into SAT, CSP, ...
Evaluating AES "constraints"
Rewrite translation functions using ss_field_op_fulldnf_gen_fcl etc
Update namespaces
Update
Concepts
SET ("SAT Evaluation Toolkit")
New tests Transfer to the new test system
Messages Use Messages.
Iteration
Connections
Basic overview
Update namespaces.
First the most important notions of frequency assignments have to be captured and formulated as generalised satisfiability problems. A good entry seems to be provided by
The above technical report mentions several benchmark collections; we need parsers. Perhaps the problem structures presented here are more important to us than those basic theoretical forms of FAP's (since we generalise them anyway).
MOFAP: (G, D, c, T, K)
MSFAP: We MOFAP, but the third condition (the constraint on K) is replaced by:
Are there competitions on the subject? (We look only at the decision side; likely most activities in this field concentrate on optimisation?!)
General databases
Documentation
make
Other files
Update namespaces
Organisation
Simple script for monitoring remote processes
Transfer
Improve naming and documentation of rows2column_df
Working again
Necessary extensions (improvements) of the old experimentsystem
Launching and monitoring
Tests
Handling changing solver output
Testing solver extraction scripts
Running experiments
Better summary statistics
Extraction tools
Add monitoring for all other solvers
Connections
Minimum CNF/DNF representations
Connections
Hardness of boolean function representations
Propagation hardness of 2CNF
Hardness of canonical translation of positive DNF
Hardness of Sudoku problems
Update namespace
Write milestones
Travelling salesman problem
Fast computation of prime implicates/implicants
Algebraic normal form
Boolean function representations
All essential computations of analyse_random_permutations at C++ level
Write "analyse_all_permutations"
Add milestones
Links
Satisfiability of products
Generalities
What to investigate for these boolean functions
Isomorphism types
Trivial cases
The case n=2
The case n=3
The case n=8
Prime implicates of simple permutations
Sampling random permutations
First considerations of random permutation
Update namespaces
DES
RSA
MD4, MD5
Connections
Links
DONE (removed directory and integrated milestones with higher level) Merge SAT2011 plans with module one level higher
SAT 2012
Notions for AES operation
Determining a "good" local search algorithm to use on AES instances
Explain how to replace various AES boxes with identity or random boxes
Separate keyschedule and blockcipher
Using SBSAT
Investigating conditions and their representations
Summary of previous experimental results
DONE Add milestones
DONE (misplaced scripts moved; todos added for improvement of others) Just an unstructured morass of scripts
DONE (moved to "Improve minimisation scripts" in Satisfiability/Optimisation/plans/general.hpp) Update scripts
DONE Replace "merge_cnf.sh" with "AppendDimacs"
Connections
Graph colouring benchmarks
Searching for small hard planar graphs
Update namespace.
Create milestones.
Literature review
Organisation
Different perspectives:
Different formulations
Active clausesets for the movescondition
The challenge of counting
Problem specification
Overview
Remove linear diffusion from translation
Translations
Minisat2.2.0
precosat236
precosat570.1
OKsolver_2002
march_pl
satz
Problem specification
Overview
Translations
Minisat2.2.0
precosat236
OKsolver_2002
march_pl
satz
Update namespace.
Create milestones.
Empirical study
Alternative formulations
Special algorithms
Generalisation for arbitrary graphs
Update namespaces.
Create milestones.
Given a graph G, the alliance expressing the Hamiltonian path (cycle) property has variables v_1, ..., v_n for n = V(G) with domains V(G), and two active clausesets:
One could add "opportunistically" some elements of the bijectivity constraint to the adjacency constraint; for example if there are v_i and v_j such that the minimal distance between their possible values in G is larger than the distance between i and j, then the current partial assignment is unsatisfiable (an extreme case here is given by a disconnected G)  this inconsistency cannot be anticipated by any of the two active clausesets alone (but must be realised by the alliance). Is there a general method behind that, leading to a meaningfully strengthened adjacency constraint?! Perhaps it is better (this might also be true in general) to create new active clausesets capturing these constraints (for example a "distance constraint", maintaining that the minimal distance in G of the possible values of any two vertices v_i and v_j is not larger than the distance of i and j).
Creating a catalogue with Hamiltonian graphs and nonHamiltonian graphs (for creating benchmarks).
Are there competitions on the subject?
The Hamiltonian Path/Cycle problem is a special case of the graph embedding problem: The adjacency constraint just has to consider a general graph G_0 with vertices v_1, ..., v_n instead of the path resp. cycle on v_1, ..., v_n. One needs good data structures for the adjacency constraint.
The graph isomorphism problem (see module Isomorphisms) is a special case of the graph embedding problem: How do graph embedding algorithms perform on graph isomorphism problems?
TSP
Problem specification
Translations
Minisat2.2.0
Overview
Problem specification
Translations
Minisat2.2.0
The 1base box translation
The "minimum" box translation
Problem specification
Instance characteristics
Translations
Analysing the data
Comparison of runtimes for the three translations
Minisat2.2.0
Problem specification
Overview
Translations
Minisat2.2.0
Update namespaces.
Create milestones.
Update namespace usage.
Connections
Update namespaces.
Create milestones.
What other games are interesting?
"Problem solver"
Tools for translations
Problem specification
Overview
Translations
Minisat2.2.0
Overview
Problem specification
The canonical box translation (bidirectional MixColumns)
The canonical box translation (forward MixColumns)
The 1base box translation (bidirectional Mixcolumns)
The 1base box translation (forward Mixcolumns)
The "minimum" box translation (bidirectional MixColumns)
The "minimum" box translation (forward MixColumns)
Problem specification
Translations
Minisat2.2.0
Glucose2.0
Problem specification
Overview
Translations
Minisat2.2.0
Update namespaces.
Update milestones.
Update the following todos.
Review: Software and literature review.
Connections to other modules
Basic direct algorithms
Active clausesets
Completing partial latin squares
Strong hypergraph colouring
MOLS
Sizes
N(n)
Experiments
Pairs of orthogonal latin squares
The upper bounds for N(k)
Problem specification
Translations
Minisat2.2.0
Introduce namespacealias.
First the distinction between this part and part Satisfiability has to be cleared:
Create milestones
Update namespaces and their usage
Connections
Transformations
The natural operation of N
Semilattices
Show and explain sizes of minimumtranslations
Patterns
Explanations
Naming of translations
Links
Boundaries
Fast generation of AES translations
Handling of version numbers
Remove usage of xxx_targets_prefix_okl : DONE
Update to the new system
Software management
Configuration/ExternalSources/all.mak
Configuration/ExternalSources/tests.mak
Connections
Considering output bits on their own
Overview
Combining linear components
Scripts for generating statistics on random boxes
Find "best" solver(s) and local search algorithms for minimisation
Standard naming scheme for experiment files
kbased representations
The square of the Sbox
Understanding prime implicates after any partial assignment
Understanding DES
Generating satisfying DES assignments
DES benchmarks
Basic translation
Encryption and decryption
r_2bases of a round
Understanding the MassacciMarraro translation
More advanced treatments
Configuration include order
Configuration data overview
Configuration data format
Primary versus derived configurations
Variables for accessing external libraries (was system_definitions.mak):
Definitions for doxygen
Overview
Number of solutions for DES key discovery
Experiment scripts
Add information on specific Sbox translations to experiment instances
DONE Move into separate submodule
Links
Analysing the Sboxes
Analysing the 6to1 bit Sbox functions
Overview
Analysing the KeeLoq round function
Comparing translations and solvers
Translating stream ciphers using our translations
Create milestones.
Complete documentation
Patches
Enable local/global installation for all packages
Organisation of links
Installation of C/C++ tools
Supporting Java
SATapplications in evolutionary biology
Matrix libraries
Logic programming
Other sources:
Suspending running processes
Counting groupoids
Classifying groupoids
Counting semigroups
Classifying semigroups
Counting quasigroups and latin squares
Classifying quasigroups and latin squares
Strictly pandiagonal latin squares
Counting the number of njective relations
Isomorphismen
Downloading sources
Update
Interfaces via OKplatform/bin
Elaborated directory structure
Building documentation
Documenting changes of files outside of the OKplatform directory
General
Using CMake : DONE (we don't use cmake)
Complete Buildsystem/ExternalSources/docus/Internals.hpp
Finish docus for special builds
Tools
Further links on the Internetpage
Domain name
Connections
Translations to boolean CNFs based on the direct encoding
Finding hard instances for boxdimension 3
Finding hard instances for boxdimension >3
Tools for investigations with concrete Sudoku instances
Create milestones.
Computing the probability of a "contradictory input matrix"
Checking all links
Doxygen problems regarding stability of links
Better general documentation
Connections
Hitting proof systems
Understanding the recursion for nonMersenne numbers
Understanding S_2(k)
Maximal number of MUS's of a clauseset
Prime implicates
Applying partial assignments
MU structure
Update of pulling and pushing facilities
Markers instead of links
Improved makefiles
Further enhancements
Add file template generation option
Complete the information on customisation.
Once the move to the new test system has been completed, references to the old test system need to be removed.
Structure
Rerun timesensitive experiments WHAT IS THE STATUS OF THIS?
Experiment scripts
Satprobabilityapproximations
Experimental investigations on heuristics
Add section on AES experiments to be run WHAT IS THE STATUS OF THIS? SHOULD BE COMPLETED BY NOW!
Translations from CSP to SAT
SplittingViaOKsolver for random clausesets
Order principles
Basic notions
Best local search algorithms
Investigating the 16 x 16 case
Investigating the 16 x 17 case
Investigating the 17 x 17 case
Investigating the 18 x 18 case
Investigating the transversals
Prepare benchmarks for SAT 2011
Standardisation on notation : DONE
Trivial GreenTao numbers : DONE (handling this elsewhere)
greentao_2(3) = 23
DONE (the basic algorithm works not too bad now) Better creation of problems
Best local search solver : DONE (there is no general best algorithm)
Connecting different n
Phase transition
Faster generation of arithmetic progression of primes
Faster local search
Survey propagation
Literature
No "useful" programs!
Using the right tools (nearly) from the beginning!
Anticipated parts
Update namespace.
Create milestones.
Basic considerations
Investigating greentao_2(2,k)
Connections
Generation
Only products
The case k=1
hindman_2(2) = 39
hindman_3(2) > 80000
hindmani_2(2) = 252
Create milestones.
Connections
HalesJewett problems
Connections
Density versions
Link checking
General rules for htmlpages
Install configuration system
Search engines
Handling of paths
Creating styles
Problems with version 1.7.3
Move
The role of documents_dir
Doxygen error messages:
Doxygen problems
Doxygen general
Doxygen menu and main page review
Docus pages
Search engine
Other code
Connections to other parts
Simple Unix/Linux tools
Investigating existing tools for parsing and refactoring code
Update namespaces.
Update namespaceusage.
Update the doxygendocumentation, and create further plans(files).
Move Concepts/RefactoringIncludeHandling.hpp here.
Transfer the tests to the new test system.
Connections
Organisation of the module
Literature exploration
Duality
Compare with the SATgeneralisation
Connections
Generation of problem instances
How to handle experimental data?
Data sheets
Experiments to be run
Investigate introduction of cardinality constraints
ramsey_2^2(3)
ramsey_2^2(6)
Investigating the parameter tuple [[3,3],2]
Exploring the parameter space
Autarkies
Blocked clauses
Symmetry breaking
Representing solutions as graphs
Selfdual solutions
"Visualising" solutions
Statistics functions are needed to analyse counter examples
Better SAT solvers
Test system
Setting the paths to GCC and Boost link libraries
User control of system versions
General_options
Dependency files
Verbosity
Targets
Role of srcdir
Cleaning
Test cleaning
Error messages of gcc should be processed
Linking and options:
Force make
Compilation information
Nightly build
Complexity system
Measurements
New targets (needs update)
Overview
What is known
Main research questions
Enumerating all solutions
Palindromic problems
Modular form of Schur numbers
Overview
Estimation of run times for direct encoding
OKsolver_2002 for direct encoding
pdschur(5)
Forbidden elements for palindromic problems
pdwschur(5)
wmschur(5)
Overview
Statistics
Certificates
Create milestones
Write tests
Write docus
"Theoretical algorithms"
Evaluation mode for oklib
Making makevariables compatible with shellvariables:
Further renamings:
System documentation
Renaming module Buildsystem
Documentation (Examples and Concepts) OK : this needs to be discussed and updated
Modes of Usage
makefile_recursive
Source code directory structure
Full test
Integration testing:
Compiler versions
Version numbers
Direct encoding
Direct encoding with forbidden elements
Direct encoding with full symmetry breaking (ordinary and palindromic)
Logarithmic translation
Weak nested standard translation
Palindromic problems, direct encoding
Palindromic weak problems, direct encoding
Packages history : DONE
DONE (there is only a permanent release process via packages created every few days or so; to the outside world it matters which functionality is provided, which is regulated by the milestones, however this does not affect the release process; yet no experience with access to gitrepositories by users) Plansstructure review: The plansstructure in Buildsystem/ReleaseProcess/plans/ needs review.
"Prerequisites" for further development
Connections
Predictions of vdw_2(3,k)
Analysing certificates
SAT 2011 competition
Local search for the satisfiable instances
Predictions of pdvdw_2(3,k)
Literature overview
Why so hard?
Performance of OKsolver2002
Performance of satz215
Performance of march_pl
Performance of minisat
Performance of picosat
Precosat
Glucose
CryptoMiniSat, Grasp
Palindromic numbers for k <= 8
Literature overview
Best complete solver for vdw_2(5,k)
Best complete solver for palindromic problems
Best localsearch solver for palindromic problems
Update namespaces
Update namespaceusage
Transfer the todos
Update the doxygendocumentation.
Switch to the new test system
Move the iteratedrelated concepts from module Concepts here.
Literature overview
Best complete solver for palindromic problems
Best localsearch solver for palindromic problems
Update namespaces.
Create a development plan and milestones.
See module ComputerAlgebra/Enumeration.
Literature overview
Best complete solver for palindromic problems
Best localsearch solver for palindromic problems
Update namespaces.
Relations:
Connections
Prepare benchmarks for SAT 2011
Create milestones
DONE (as stated) Organisation
Boolean van der Waerden numbers
Translations for nonboolean problems
Palindromic diagonal problems
Symmetry breaking for van der Waerden numbers
Palindromic versions
Overview on performance of SAT solvers
Lower bounds
Best practices
Cleanup regarding shared repositories : DONE
Documentation : DONE (we don't provide Git ourselves anymore)
Spell checking
Cloning
Resetting the shared repository : DONE (moved to Github)
DONE (no longer relevant to us) Notificationemails
Remote access
Tagging
More advanced usage:
Combining different repositories
Change dates and revision numbers
Exploring usage patterns
Space usage:
Concepts
Investigate whether there is something usable in the following old files:
Collect
Input/Output
Update namespaces.
Connections
Plingeling
Cryptominisat
Parallelisation via OKsolver2002
Parallel Satz
Using Open MPI
Update Data
Verify vdw_2(4,9) = 309 (conjectured)
Verify vdw_2(5,7) = 260 (conjectured)
Naming the transversal hypergraph of arithprog_hg(k,n)
Relations to vanderwaerden_m(k_1, ..., k_m)
Studying the transversal hypergraph
Exploiting "selfsimilarity"
Connections
Experimentation tools
Saturated Horn clausesets
Saturated minimally unsatisfiable clausesets of deficiency 2
Further testcases
Update namespaces.
Relations
Connections
Overview
Connections
Exact transversals of hypergraphs of partitions
Scope of the catalogue
Connections
Integer sequences of interest
Deficiency = 3, n = 5
Primes
Update namespaceusage.
Module structure
Translations
Other implementations
Active clausesets
Investigate the problem of determining the chromatic number:
Property B
Square hypergraphs
Update namespaces.
Discussion
Update namespaces.
Relations
Update namespaces.
The general framework
General plans on evaluating solvers, algorithms, heuristics
Update namespaces.
Create milestones.
Update namespaces.
Literature and software review on matching algorithms
Concepts for bipartite graphs are needed.
Relations
First implementations
Injectivity constraints
Online: We need also "online"versions of these algorithms, allowing to remove some edges and recomputing the maximum matching respectively the set of unusable edges. Removing edges corresponds to applying some partial assignment; adding some edges then would correspond to backtracking steps.
Counting: We need (exact) algorithms for counting of perfect matchings
Surplus:
Correction: DONE Find the date in the cvslogs for Matchings/plans/milestones.hpp (originally the first version was 0.0.1, but this was changed to 0.0.2, since there were already some more plans there).
Update namespaces.
Basic revision
Improvements
Other tools
Update namespaces.
Create milestones.
First we need some system installed under ExternalSources.
Relations
Update namespaces.
Relations
Create milestones.
Using Prover9
Notations
Proving distributivity of union and intersection
Updating and extending axioms.bel
Create milestones.
Plans
Update namespaces.
Scope discussion
Update namespaces.
Module Computability
NPcompleteness
NPcompleteness 2
Update the namespaces : DONE
All submodules have milestones.
Clarify the relations
Update namespace usage.
Graph generators
Graph operations
Organisation
Update namespaces.
Create milestones.
Circuits
What else?
Move to Combinatorics/Graphs. DONE
Update namespaces. DONE
Move todos in TreeDecompositions/EliminationSequences.hpp to plans. DONE
Update namespace usage
Create milestones
Complete doxygen documentation.
Move to new test system.
Write tests.
Write a simple application.
Update namespaces.
Relations: We need to establish links to other modules.
Connections
Create milestones
Update namespaces.
Relations:
Which systems?
Usage discussion
Update namespaces.
Create milestones.
Generic algorithm
Special actions July/August 2011 (MG, OK)
"OKlib" instead of "Transitional" : DONE
Supermodules:
Handling of versionnumbers : DONE
Research submodules : DONE
Organisation of plansdirectories
Access to version numbers
Demos
Backups and archives
Upgrade the C++ code to gcc4.5.3
Promoting the OKlibrary
Ranking
Estimated time needed
Update namespaces.
Collect possible requirements on a hypergraph concept
Concept design in general
Move the related files from OKlib/Concepts here : DONE
The simplest form of hypergraphs
Update namespaces.
Transferring General/ErrorHandling.hpp. We should use Messages instead of strings.
Create milestones.
The Boost method seems reasonable, so we should transfer it. But better using own types (a base class for all exceptions thrown by the library).
Based on facilities in Messages/Utilities, there should be convenience macros for throwing exceptions (adding automatically all file information etc.).
We do NOT provide "cheap" message creators ("valuebased"): For every (new) message a class has to be written in an appropriate file in a meesagesubdirectory.
Compiler options for Programming/InputOutput/PathDifference.cpp
Update namespaces
Update namespaceusage
Complete doxygendocumentation
Update plans Write plans for all submodules and transfer all todo's:
Move Refactoring/BoostPathCorrected.hpp to here.
Write docus
Write demos
Transfer the tests to the new test system
Generic inserters and extractors
Update namespaces.
Create milestones.
Relations
Update namespaces. DONE
Input and output
Update namespaces
Update namespaceusage
The general concept of a "message": There need to be clear definitions and examples for what a "message" is:
Empty output
Internal use of messages
Demonstrations
Testing:
Memory management
Write documentation
Formalise concepts
Update namespace
Update namespace usage.
Identification services: We need further classes (and macros) for identification purposes:
Warning and error messages
Error handling
Testing
Umlaute
Update namespaces
Update namespace usage
Update the doxygen documentation
Update plans
Transfer tests to the new test system
Update namespaceusage.
Run through examples from [C++ Cookbook 2006, Chapter 12]
New test system
Investigate libraries for processes and threads
Decide, how to handle parallel computations for the OKlibrary.
Update namespaces
Update namespaceusage
Update the doxygendocumentation for this module.
Decide what to do with this module, and with parsing in general:
Transfer the tests to the new system (where are the current test functions used?)
Connections to other modules
Trivial algorithm for input G, k
An "eager, binary" variation of the (above) trivial algorithm
Enumerating all transversals T with T <= k
Application BoundedTransversals_bv
As generalisedSAT algorithms
Overview on more sophisticated algorithms
Update namespaces.
The OLD point of view
The NEW point of view
Three kind of parameters
Standard options
General assignments
Enumeration of parameter forms
The basic class
Short forms
Specification class
Analysing program options
Streams
Boost program options library
Old system
Update namespaces.
Relations
Move parts of General/Algorithms.hpp to here.
Should module Iterators be included here?
We do not use Boost here, but the test system  shouldn't then the test system not arrange for including the Boost library, not the user of the test library?
Update namespace.
Update milestones.
Write docus.
Create milestones
Iterators and ranges
Connections
Notions and notations
Homomorphisms
Cleaning up
Future plans
Update namespaces
Update namespaceusage
Create milestones.
Update namespaces : DONE
Update namespace usage
Write doxygen documentation
Write docus
Write demos.
Write tests (in the new system).
String comparison
Orbits and stabilisers
Centralisers
Update namespace : DONE
Write milestones
Update namespaces.
Write milestones.
First prototype
Create milestones
Connections to other modules
Overview on implementations
The lexicographical canonical numbering
Connections to other modules
Conversions
Associativity resp. group test
Update namespaces.
Update milestones.
Hypergraph transversals
Further milestones:
A general approach is to find an equivalent DNF by DPLL
Another approach is using OBDD's (this should likely go into its own module).
What is the relation to the counting problem?
Connections to other modules
Algorithms for the matching lean kernel
Finding matching autarkies
Implementation
Applications
Incremental
Connections to other modules
Lean kernel
Update namespace usage.
Link to ComputerAlgebra/Satisfiability/Lisp/Autarkies/plans/general.hpp
Write tests
Naming conventions
Forms of "constructive" groupoids
Straightline programs
Congruence relations
Update namespaces.
Connections to other modules
Update namespace usage.
Concepts
New milestones
Move the content of OKlib/SATAlgorithms here : DONE
Update namespaces : DONE
Connections
Notions and notations
Update namespaces.
Create milestones
Considering the following graphs for clauseset F with clauses as vertices, where clauses C, D in F, C != F, are joined iff
Considering the following graphs for clauseset F with variables as vertices, where variables v, w in var(F), v != w, are joined iff
Given a clauseset with bipartite structure, "construct" the above graphs as "virtual graphs" in the Boostsense. Algorithms needed for graphs:
Statistics for benchmark formulas :
Possible heuristics exploiting decompositions:
Classical tree decomposition algorithms and improvements
Develop the ideas
Framework
Semantical trees
A very attractive form of learning is "r_kcompressed learning"
Afterburner
Reworking the tree
"Intelligent backtracking"
Responsibility for learning
Managing the learned clauses
In general we do not care about the "source" of the learned clause:
Autarkies
Two general forms of preprocessing
Preprocessing by reduction
Preprocessing by local compilation
Preprocess a clauseset by local dualisation
Finding and exploiting functional dependencies
Abstract representation of structures
Modules
DONE (see above) Semirings, rings, fields
DONE Module UniversalAlgebra
DONE Modular arithmetic
DONE Actions and operations
Relations to other modules
Create further milestones (for 0.0.7)
Framework for the analysis of search space structures
Using Ubcsat as a library
Installation of UBCSAT completed
Contact the developers of Ubcsat
Update namespaces
Connections
Different levels of generalisation:
Concepts
Organisation
Write tests
Homomorphisms
Module "Operations"
Connections
The basic concept of a "partial assignment"
Development of the fundamental concept of a partial specification phi
How to do the updates in an alliance of active clausesets
Relation to the notion of clauses
Update namespace usage.
Old implementations
Evaluation
Design study for evaluation
Clausebased approach
Connections
Firstorder theory of the reals
Links to other modules
Planning
CLS(n)
CLS(n, c)
CLS(n, c, k)
Rename applications
Links and plans
Prime implicants and implicates
Minimisation
BDDs
Connections
Basic notions
Abbreviations
Concrete categories
Functors
Natural transformations
Connections to other modules
Other tools
Basic notions
Basic examples
Create further milestones
Using different algorithms for different parameter values
Relations to other modules
Organisation
Update the module according to OK's SATHandbook article
What are the relations to module "Projections"
Update namespaces : DONE
Move OKlib/Statistics/plans/TimeSeriesAnalysis.hpp to here : DONE
Create milestones
Connections
Adding distribution power to SplittingViaOKsolver
Organising distributed solving
Sampling tool
Distribution via splitting trees
Tests for error cases in scripts
Update output for application tests
Strange tool statistics_add_missing_clause_lengths.awk
Comprehensive statistics
Elementary filesurgery
Rewrite code for the new namespaces.
Update
See OKlib/Satisfiability/ProofSystems/DPv/Input_output.hpp
Write docus
Move to the new test system.
Complete the tests.
Write demos.
Complete the functionality.
Input and output of propositional formulas
Circuits
Convenience functions
Variable ordering and standardisation
Sbox boolean 6xm functions
Add variants with reduced number of rounds
Improve tests
Create constraint evaluation system
TripleDES
Links
Translating the constraintsystem into SAT, CSP, ...
DONE (see des_sbox_bit_fulldnf_cl) Add 6to1 bit Sbox functions
Update namespaces.
Improve minimisation scripts
Computing all minimum transversals one by one
Create module MinOnes (or "WeightedSAT" ?)
Create module MinSAT.
Create module MaxSat.
New supermodule on autarkies
New supermodule on CSP
Update:
First Concepts: Concept prototypes for injectivity, surjectivity and bijectivity constraints
Literature and software review
Basic implementations:
Exploiting matching algorithms; see Matchings/plans/Matchings.hpp
Complexity measures: The natural complexitymeasure for an injectivity constraint is the sum of the logarithms of the domain sizes of the variables involved. Also the measures for the simulating clausesets (boolean or not) can be easily computed. But in general these measures might not be very useful.
Autarkies: Autarkies for injectivity constraints (and the other types) are likely best understood by using the boolean CNFrepresentation.
Extraction: We should also investigate how to extract injectivity constraints (from ordinary clausesets for example, and in general from active clausesets).
For variables v, v' not only " v <> v' " is needed, but more general " f(v) <> f(v') " for some function f.
Update namespaces. DONE
Create milestones.
Update namespaces.
Given a boolean clauseset, the first problem is to extract the equivalences. The direct approach looks only at the clauses as given: We consider the equivalence relation ~ on F given by C_1 ~ C_2 iff var(C_1) = var(C_2). Then we examine an equivalence classes F'. All clauses in F' have size k; If c(F') < 2^{k1}, then F' doesn't contain an equivalence. Otherwise we consider the partioning of F' into F'_0 and F'_1 containing all clauses of parity 0 resp. 1 (regarding the number of negations). Now there are 0,1 or 2 equivalences in case F'_0 resp. F'_1 has size 2^{k1}. Stronger approaches find also "hidden equivalences".
Then we need an active clauseset representing systems of equations over ZZ_2: "Falsified" means that one equation is falsified by the current (partial) assignment, "satisfied" means that all equations are satisfied by the current assignment (for an equation to be falsified or satisfied, all variables must have assigned a value). "Unsatisfiability" means that the system has no solution, and finally the implied unit clauses are the derived equalities v=a for a variable v and constant a in {0,1}. Naturally also implications v=v' arise here (but they are better just kept "inside", as discussed in the next point). We need efficient algorithms ("online").
A fundamental problem arises here: How to handle equivalences v=v' in the context of an alliance of active clausesets? It seems most natural not to do anything special here, but just let the active clauseset managing equivalences handle this (if v is set to some value, then v' is set accordingly, and vice versa). So this is not a problem; but we have the problem for the heuristics to integrate from the various active clausesets their complexity measurements.
How to generalise the concept of equivalences to nonboolean variables? Systems of equations over ZZ_m ? More general handling of system of equations of fields ? Rings ??!
Connections
Implement WP (warning propagation)
Implement BP (belief propagation)
Implement SP (survey propgation)
Update namespaces.
Transferring (and updating): OKsolver/Experimental/Transformationen/LinInequal.
The relations to the module InjectivityConstraints have to be investigated.
The relations to the module SATModuloTheory have to be investigated.
Update namespaces.
Create milestones.
First the scope (the (informal) concept) has to be established, and the relation to module LinearInequalities.
Update
Standardising variable names
Sudoku
Bicliquetransformations
MUSAT
Matching formulas
Generators for finding incidence structures and designs
Extended resolution
From nonboolean clausesets
Pebbling formulas
Implement the general construction of Soeren Riis (especially interesting when we know that the formulas have short refutations).
Other SATrelated attacks
Decryption using iterative block ciphers
Other cryptosystems
Update namespaces: DONE
Create milestones
Connections
Organisation
Updates
Headtail clauses
Connections
General ideas
DONE (we have now Clauses::RClausesAsVectors and Clauses::RClausesAsSets) Clauses for unitclause propagation
Partial assignments
DONE Update namespaces.
Move the related concepts and plans from OKlib/Concepts here.
Update ProblemInstances/ClauseSets/ClauseSet.hpp, so that it becomes a very simple implementation of the generic concepts.
Move concepts from OKlib/Concepts here.
Update code w.r.t. new namespaces.
Further trivial atomic conditions
First prototype of general atomic condition
Improve key schedule tests
Specification
Add variants with reduced number of rounds
Find more test vectors
Notion of DES round
Links
TripleDES
Tidy todos and update milestones
Improving tests
natl vs nat_l
Notions and notations
Modularising the Rijndaelimplementation
Docus and Demos
Coding Standards
Design conditions more general than "atomic conditions"
Integration with computer algebra
Move the related concepts and plans from OKlib/Concepts here.
Boolean literals
Good definition
Add todos
Create milestones
Update namespaceusage
Prototypes
Write tests
Update namespaces. DONE
Create milestones. DONE
All existing components related to problem instances are moved here. DONE (handled already by another todo)
All submodules have milestones.
Create a docus page with an overview on the concepts and ideas.
Integration with computer algebra.
Move the related concepts and plans from OKlib/Concepts here.
Update namespaceusage.
Prototypes
Update
Old implementations
New test system
Conversion functions
New structure DONE
Create milestones. DONE
DONE Update namespaces.
Create further milestones
Stronger propositional proof systems than resolution
Systems related to extended resolution
Restructuring
See Applications/Cryptanalysis/plans/general.hpp
Write a general docusfile
Create milestones
DONE Move the helperfunctions from Cryptology here.
Create milestones.
Main challenge are the concepts.
What are the input formats?
Applications
Basic autarkies
Bounded maximal deficiency
Add application tests for RandomUcpBases
Connections
The notion of rbases
r_0base
Docus for RUcpGen
Basic notions
More general notions
First simple implementation
Transferring the implementation used in OKsolver_2002
Timestamp
Avoiding repetition
Local learning
Interface
Graph representation
Responsibility
2clauses
There is the recurrent theme of "local vs. global"
Double lookahead
DONE Update namespaces.
Connections
Create milestones.
DONE Update namespaces.
Preprocessing wrappers
DONE Update namespaces.
Update namespace usage
Connections
Update the plans.
Create milestones.
Implement trivial unitpropagation (quadratic time)
Implement generic standard lineartime algorithm for boolean clausesets
Implement initial UCP based on headtail clauses
Implementing the standard lineartime UCPalgorithm (based on the bipartite structure) for Powerclausesets.
Investigate how to specialise the general UCPalgorithm for clausesets and boolean clausesets.
The basic algorithm should assume an "active clauseset" and an "active partial assignment"
A clauseset F can be constructed with a binding to a partial assignment F.phi().
Regarding unitclausepropagation for an alliance of active clausesets
UCP for clausesets has the following interesting property
A variation point is whether we want to go also through the satisfied clauses or not (marking them as satisfied)
Connections
Document options
Control verbosity of output
Output of learned clauses
Output all information when aborted by SIGINT
Correcting includedirectives
Usage as library
Update namespaces.
Create milestones.
Trivial DLLsolver "DLLImplementations"
Directed graphs
Maximum bicliques
Translations to clausesets
The conjecture of [Galesi, Kullmann]
NPcompleteness of determining bcp
Create milestones
Newer versions
Links
Output learned clauses
DONE Improve patches
Update namespaces.
How to refer to the different versions of OKsolver ?
Combination of OKsolver with Minisat
Concepts
Exactly one common neighbour
More information on the current path
Splittingoutput in iCNF format
Differences
Improve the Dimacsoutput
Introduce errorcodes
Output to files
OUTPUTTREEDATAXML
Documentation problems
Language standards
Buildsystem (replacing Buildtools/UebersetzungOKs.plx)
Complete the help facilities of the OKsolver
Write docuspages
Add doxygendocumentation
Eliminate old history in code.
Create systematic application tests
Add asserts throughout
Investigate unittesting
Correct computation of basic statistics
Apply Valgrind
Apply code analysis tools (like Splint)
Improve statistics code
Declare variables as close to their first usage as possible
Use constqualification
Use restrictqualification
Elimination of compiletime options
Output of clausesets
Inefficiency on 64bit platforms
Extend statistics
Output intermediate results
More influence on heuristics
Improving the implementation
Start planning on evaluating and optimising heuristics
Apply timemeasurements
Optimising the code
Why so slow on easy instances?
Extension by cardinality constraints
Improved Delta(n)distance
Enable finding all solutions
External solvers
Special solvers
DONE Update namespaces.
Organisation
Complete tests
Redesign
Representing edge and vertex labellings
Lists instead of sets
Graphs as hypergraphs
Memoisation for general graphs and multigraphs
Maxima package "graphs"
Graph traversal
Treewidth
Primitive directed graphs etc.
Generalised matching problems
Graph drawing
Improve file output
Correct memory handling
Use signals as with OKsolver_2002
Provide application tests
Update to C99
Add Doxygen documentation
Create milestones
Provide information
Timing
Using the taufunction
Handle signals : DONE
Provide Doxygen documentation
Introduce macros : DONE
DONE Check number of variables and clauses
Version information : DONE
Improving the clausebitsets
Optimising weights
Concepts
Isomorphism testing
Spanning trees
Update namespaces.
Given a rooted tree, a corresponding SMUSAT_{delta=1} needs to to be constructed. Special cases for the full tree and the input tree. Perhaps this should go to a submodule RegularHittingClauseSets.
More generally, for an arbitrary rooted tree and a labelling of inner nodes with variables, such that no variable occurs twice on any path from the root to some leaf, construct the corresponding (tree)hitting clauseset.
Likely, in this module also multihitting clausesets should be considered (with nonboolean variables).
Update namespaces.
Create milestones.
Generatorplans mentioned elsewhere and relevant here should move to here.
SNSmatrices, Pfaffian graphs etc. (possibly this should go to its own module on combinatorial autarkies?)
Connections
Organisation
Statistics
Sudoku
Direct translations
Overview
Preprocessing
Good representations
Literature overview on boolean translations
Ladder logic standard
Input format
Output format
Iteration
Properties
Connections
Transfer
Testing
transversal_hg
Update namespaces : DONE
Create milestones : DONE
Update namespaceusage.
Travelling salesman
Connections
Organisation
The triangle of the three possibilities
ind_hg(G)
Overview on SMT
Overview on main types of constraints
How to translate these problems into our domain
Create new milestones
Update namespaces.
Create module on NaeSat.
Create module on XSat.
Module on counting
Concept for aesusage
Crypto++
OKgenerator
Update namespaces.
Create milestones
Update namespaceusage.
Tests
Create milestones
Write tests
Write docus
Indices
Algorithms for the hermitian rank
Boost:
The basic concept for big integers should (just) include:
First client: Most important is what module RandomGenerator needs (see RandomGenerator/plans/general.hpp).
Natural numbers: One design issue is how to handle natural numbers (NN_0 and NN). Likely we need different concepts (the free ring vs. the free semiring, each of dimension 1), where the concepts allow for conversions. (NN is the free semigroup with one generator, while NN_0 is also the free monoid with one generator.)
Basic concepts are needed for the basic algebraic structures:
What about generalisations/extensions of the integers? (Mostly numbertheoretical.)
Update the namespace.
Boost
See the concepts in Concepts/plans/BigIntegers.hpp. DONE
Basic notions
The main parameters
Polar and bipolar incidence structures
Create namespace
Create milestones
Update namespaces.
Organisation
Matrices
Representing partial boolean functions
Analysing the extensionlandscape
Generalisations
Create a milestones file.
First Maxima implementation:
Axiomatisation
Compute propagationhardness
DONE (function hardness_wpi_cs has been provided) Computing the hardness of a clauseset representation
Create milestones
Write docus
Update namespace
Update namespaceusage
Update doxygendocumentation
Update plans, transfer todos
Reorganisation
New test system
Write docus.
Write demos.
Introduce subsumption hypergraph generator
Update namespaces.
Timing the Maxima tests and the application tests
Designing the file structure
Designing the level system
Designing the makefile
Designing measurement classes
Precision of measurements
Designing measurement accumulation
Update namespace
Update the documentation
Documentation
Build system
Compiler warnings
Update namespaces.
Graphics library
Graph visualisation library
External libraries / programs:
Concepts
Applications
Conversions
Fundamental notions
Examples
Greedy algorithm
Rewrite hypergraph transversal functions in Maxima
Rewriting: All modules are to be redesigned and reimplemented in Maxima
Function "min_scanning" (ComputerAlgebra/Numerical/Lisp/Minimisation.mac)
Implement the "downhill simplex method in multidimensions" (according to Nelder and Mead).
Place of IndependentSets.mac
Write tests
Redesign
Write docus
Statistics
Special properties of hypergraphs
Intersecting hypergraphs
Helly property
Hypergraph automorphisms
Representing edge and vertex labellings
Palindromic versions
Connections
Translations to SAT
Using ILP
Exploiting known bounds
Architectures of the systems for showing/computing Ramseytype numbers
Handling bounds
How to annotate numbers with justifications?
Develop plans
Create milestones.
Blind search for backdoors of size k
2CNF backdoors
Horn backdoors
Backdoors w.r.t. clausesets of bounded deficiency
Create milestones
Write tests
Write docus
Balanced autarkies
Pure autarkies
Autarky search via running through all total assignments
Implement the translation of USAT to LEAN according to our article with Victor and Mirek
Basic functionality
Fundamental notions
Branching greedoids
Relations to other modules
Automorphisms of Ramsey hypergraphs
Automorphisms of Ramsey clausesets
Representing counterexamples
Relations to other modules
Fundamental notions
Categories of boolean functions
Connections to other modules
Handling of demos
Cleanup BranchingTuples/Basic.mac
Reimplement the remaining functionality from Mupad/tau.mup in Maxima
Trees
Details of computations
Optimisation
Investigations on approximations
Update output_pa
Create milestones
Write tests
Write docus
Notions for clauses, clausesets etc.
Organisation
Input and output
Create milestones
Write tests
Write docus
Conflict graph
Hermitian rank
Relations to other modules
mcind_cs, cind_cs:
Relations to other modules
Handling of duplicate entries for vdWnumbers
Lower bounds
Considering finite commutative groups G
Automorphisms of vanderWaerden hypergraphs
Automorphisms of vanderWaerden clausesets
Create milestones.
Write the direct algorithm (running through all total assignments)
Write a scheme which uses r_ksplitting trees
okltest_satprob
satprob_mcind
satprob_incexl_hitting
Connect to the countingmodule in part Satisfiability.
Sumproduct (belief propagation) and beyond
Sampling falsifying assignments
Add tests for parity generators
Update milestones
Accompanying statistics
Write basic docus
Variables
Floodit
SMUSAT(1) and tree hitting clausesets
Hard clausesets (for resolution and refinements)
Operations (new clausesets from old ones)
Hiding small unsatisfiable clausesets
DONE Split Generators/Generators.mac
Connections
Update names
More efficient implementations
Strengthen the tests
Use oracles
Generalisations of the Kneser graphs
Parameters of the Kneser graphs
Forms of complete graphs
Counting, enumeration and sampling
Evaluating the Maxima function random_tree
Evaluating uniform_randomtree_og
Write tests
Concept of a "propagator"
"n Queens"
Hitting clausesets
Class OKlib::SATAlgorithms::Backtracking
Intelligent backtracking and learning
Integration
Goal
Test OKlib::SATAlgorithms::Backtracking<p>More flexible splitting
Prerequisites
Asciidoc
Info and manpages
Git book
Installation process
General usage strategy : DONE (we only use Github, no own server)
Github terminology and features
Collaborative work on github
SourceForge
Application RankPrimes is slower with version 4.3.0/4.3.1
Improve installation of Mpfr
DONE (provided installation using current gcc) Installation of Mpfr
Design the concept of a wrapper for a bigintclass
Write tests for the concepts
Implementation of the basic wrappers: I guess, best based on the Cinterface.
Vertex invariants
Alliances
What about the graph embedding problem ? This should likely go to another module.
General C++ graph libraries
Graph isomorphism
Graph drawing
Treewidth
Travelling salesman
Graph colouring
Cliques
Hamiltonian cycles and paths
Implement the generic graph_traversal algorithm from the CS232 script (generic enough, and with enough eventpoints, so that protocolling and visualisation are possible).
Implement the main applications or graph_traversal from the CS232 script
Graph traversal is a basic technique for all forms of applications of graph theory to SAT; a general overview on algorithms and implementations is needed, and also on overview on the potential applications.
Basic concepts
Efficiency
Relations to other modules
Outsourcing
Class Greedy_colouring
Literature
How do these algorithms translate into SAT algorithms?
Local search for a good vertex ordering
Generalisation to hypergraphs
Use InputOutput::CLSAdaptorDIMACSOutput
Use Messages
Connections
Generator
Connections
Further information on arithmetic progressions in prime numbers
Connections and scope
The basic generators
Improving SAT translations
Improving GTTransversals
Improving GTTransversalsInc
Finding the best algorithm from ubcsat
greentao_2(3,6) >= 2072
OKsolver_2002
Minisat2
march_pl
Finding the best algorithm from ubcsat
Survey propagation
greentao_2(3,7) > 13800
Investigate greentao_2(3,k)
SAT 2011 competition
greentao_2(3,4) = 79
Predicting greentao_2(3,k)
Finding the best local search solver
greentao_2(4,5) > 4231
Survey propagation
greentao_2(5) > 33500
Survey propagation: greentao_2(5) > 34308
Conjecture: greentao_2(5) = 34309
greentao_3(3,3,4) >= 434
greentao_3(3,3,5) > 1989
Upper bounds
greentao_3(3,4,4) > 1662
greentao_3(3,4,5) > 8300
DONE (available now) Symmetry breaking:
adaptnovelty+
OKsolver_2002
march_pl
satz215
minisat2
picosat913
precosat236
Why is minisat2 so much faster than OKsolver_2002 ?
Best local search algorithm
Lower bounds: greentao_4(3,3,3,4) > 1052
Best local search algorithm
greentao_4(3,3,4,4) > 2750
Best local search algorithm
Lower bounds: greentao_4(3) > 384
Upper bounds
Minisat2 for n=377
Picosat913 for n=377
OKsolver for n=377
greentao_4(2,3,3,3) = 151
greentao_5(2,2,3,3,3) >= 154
greentao_4(2,3,3,4) >= 453
greentao_5(2,2,3,3,4) >= 472
General considerations
greentao_3(2,3,3) = 31
greentao_4(2,2,3,3) = 39
greentao_5(2,2,2,3,3) = 41
greentao_6(2,2,2,2,3,3) = 47
greentao_7(2,...,2,3,3) = 53
greentao_8(2,...,2,3,3) = 55
greentao_9(2,...,2,3,3) >= 60
greentao_10(2,...,2,3,3) >= 62
greentao_11(2,...,2,3,3) >= 67
greentao_12(2,...,2,3,3) >= 71
greentao_13(2,...,2,3,3) >= 73
greentao_14(2,...,2,3,3) >= 82
greentao_15(2,...,2,3,3) >= 83
greentao_16(2,...,2,3,3) >= 86
greentao_3(2,3,4) = 117
greentao_4(2,2,3,4) = 120
greentao_5(2,2,2,3,4) = 128
greentao_6(2,...,2,3,4) = 136
greentao_7(2,...,2,3,4) >= 142
greentao_8(2,...,2,3,4) >= 151
greentao_3(2,3,5) = 581
greentao_4(2,2,3,5) >= 582
greentao_5(2,2,2,3,5) >= 610
Improve implementation
Compare with specification
Provide other translations
Connections
Generator for GreenTao problems
Statistics on the number of arithmetic progressions
Computing minimum transversals
Connections
Standardisation
Statistics
Statistics output for GreenTao problems in the Dimacsfile
Symmetry breaking for GTproblems
Arithmetic progressions for prime numbers
Connections
Improved organisation
Improved usage
Information on convergence rate
Controlling the error in the computations
Write application tests
Enable parallelism
Alternative computation via logarithms
Handle several kvalues : DONE
DONE (when using time, then the output needs to be copied to a file) Potential bug
Encodings
Quasigroups
Literature surview
Discrete groupoids
Introduce memoise function wrapper
Using the Maxima "associative arrays"
New naming conventions
Concept of a settheoretical map
Improving the hashmaps
Improving the oklarrays
Implement iteratorforms
Implement general functionality (arbitrary k)
Implement "all products"
Connections
Write simple generator for boolean problems (r=2)
Improve generator names
The notion of a "Hindman parameter tuple"
Write tests
Organisation
Connections
Allowed parameter values
Constructions
max_var_hitting_def
Representations
Decomposing clausesets into hitting clausesets
Generators for unsatisfiable hitting clausesets
Generators for satisfiable hitting clausesets
derived_hitting_cs_pred_isoelim
Nonsingular unsatisfiable hitting clausesets of given deficiency
all_cld_uhit_minvd
Complete local home page
Improved logo
Meta tags : DONE
Organisation
Naming conventions
Isomorphisms
Transport via homotopies
Homotopisms
Induced congruence relation
Organisation
Bruteforce automorphism enumeration
Handling of automorphism groups
Visualising automorphisms
Deciding whether for given H there is a graph morphism G > H
Relate to ComputerAlgebra/Satisfiability/Lisp/Backdoors/plans/general.hpp.
Design for the algorithm "sbhorn" from [Nishimura, Ragde, Szeider; 2003, Detecting Backdoor Sets with Respect to Horn and Binary Clauses] (developers SS, MS, OK)
Relations to other modules
First prototypes
Organisation
Lazy combinatorial matrices
Implication graphs
Once we can use directory structures, likely classes should be seperated into files so that each file includes only one boost header file.
One should test, whether these constructions hamper runtime and runspace efficiency (with compiler optimisation turned on they should not).
Documentation
Dotformat
Reading graphs in dotformat
Maxima graphspackage
Other graphformats
Transfer the tests to the new test system.
Write concept InputStreamable (and related constructs).
Basic data
r_1bases : mincl_r1 <= 4200
Using weighted MaxSAT to compute small CNFs
Find the symmetries of the AES inversion DNF
Transfer from Orthogonal.mup
More intelligent iteration
Creation of random subsets:
We want three types of extensions:
All isomorphism types of extensions
Randomised extensions
Investigations
Isomorphism testing by backtracking
Connections to other modules
Invariants for matrix isomorphism
Invariants for square matrix isomorphism
Selfduality
Valued matrices and their homo and isomorphisms
The notion of isomorphism
Enumerating isomorphism types
Considering special boolean functions
Basic notions
Finding literature
The trivial algorithm
AES as an ics
Applications from railway safety
First the Boostiteratorconcepts need to be studied, and related to our efforts. (Are they now part of the new standard? hopefully there are concept definitions somewhere.)
Write concepts for
Translations
Overview
Transferring the Argosatdesgen example
Canonical+ translation for the Sbox (6to4)
Canonical translation for the Sbox (6to4)
Applying SplittingViaOKsolver
DONE Add todos
DONE Summarise results
Write tests (in the new test system).
OKlib::Messages::LanguageName just translates strings into the value given by the strings interpreted as constants  isn't there some Boost component for that?
Once available (and having tests in place), the std::map in class Messages::LanguageName should be replaced by a hash map.
Finally, one should use a specialised stringmatching algorithm (for realising the map in Messages::LanguageName).
Write tests (in the new test system).
fr_CA disabled due to an error in g++ (3.4.3  4.0.2, 4.1.0). Fixed in 4.0.3.
For Messages/messages/Languages.hpp:
Doxygen documentation Doxygen documents the macros OKLIB_QUOTE and OKLIB_QUOTED_SEQUENCE, although they are undefined  how to correct this?
Relations to other modules
Organisation
Different encodings
Further conditions
Update
Systematisation
Extensions
Generators for latin square completion problems
Lean kernel via variableelimination
Lean kernel via oracle for leannessdecision
Connections
basic_learning
Intelligent conflictanalysis
Write tests (in the new test system).
Doxygen documentation The explicit instantiation of Messages::S<Basic> is not listed  how to correct this?
Write a concept.
Write accompanying Test and Testobjects files.
Should the helperclasses for archetypedefinitions (like Concepts::convertible_to_bool) go into their own file?
Should boost/type_traits.hpp be replaced by the tr1components?
Perhaps the macros need some cleanup.
Transfer the tests to the new test system.
Connections
Affine bijections over ZZ_2
The complement of the diagonal matrix
Random sampling
Mathematical investigations
Connections
gen_2xor_fcl
Translating two xorclauses
Basic data
Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 48
Update function names
Complete LinInequal.cpp
Also handle ">=" and "=" (besides "<=")
Create Doxygen documentation
Restore old "assignmentapplication"
Improve VdWTransversals and VdWTransversalsInc
Write docus
Installing and using Sbcl
DONE (not possible, since binary is needed) Installing and using Cmucl
DONE (works now (but CLisp is very slow)) Update to CLisp version 2.49
Libffcall not installing on AB's 64bit Xeon machine
DONE (no longer in active development, and thus not considered anymore) Installing and using GCL
Installing other Lisp's
Generating list of elements 1 to n
Applyfunctionality
Correct implementation of some_s and every_s
Inplace modification
Improving sort_length
Improve partition_list_eq
Correct split_list and split_list_epo
Arity
Generalised literals:
Requirements literals
Hets
Proof assistants
Modal logic
Support for bounded arithmetic
Weka
Repositories
Book [Machine Learning, Tom Mitchell]
DONE Mailing lists
Instructions
User mailing list
Documentation
Future of this makefile:
Makepp
DONE (we don't use CMake ourselves, and let the Linux distribution provide it) CMake
Competition extraction tools
Create milestones
Data
Functional analysis
Relational analysis
Replace use of boostregex by the facility from the standard library.
Use module ProgramOption (once available).
Connections to other modules
Matching satisfiability
Deciding matching leanness
Finding matching autarkies
Computing the matchinglean kernel
Computing a quasimaximal matching autarky
Surplus
Why is Maxima file output so slow?
DONE (this was fixed in Maxima, after communication on the mailinglist) Stable sorting
DONE (transferred to docus) Restricted recursion for memoised functions
Memoised functions
Argumentlength restriction
How to use functionparameters reliably??
Problems with errcatch
What is "equalp" ?
Maxima/CLisp bug for larger datasets
General design: Lists *here* are more fundamental than sets
Plan the redesign
Recovering of partial results after long (unsuccessful) computations
Debugging
Documentation
Handling of demos
Monitoring
Contexts
Lisp integration
Collaboration with the Maxima community
Memory restrictions
External documentation
Installation of version 5.23.2 : DONE
Installation of version 5.22.1 : DONE
Install xgettext
Using other Lisps
Database of integer sequences
Additional packages
Systemwide installation
Handling of redefined loadfunction
DONE (now Eclmemorymanagement only loaded for Ecl) Using CLisp
What memorybounds?
Minimally unsatisfiable clausesets
Unsatisfiable nonsingular hitting clausesets
Minimal variabledegree of uniform minimally unsatisfiable clausesets
Pumping up binary clauses
Implementing [Hoory, Szeider, SIAM Discrete Mathematics, 2006]
Basic statistics
Conflictindependence number
Conflictpartition_number
Hermitian rank
Characteristic polynomial
Write tests (in the new test system).
Create a Messsagesconcept.
Overview
Connections
Tidy hittingclauseset todos and move method here
Add instructions for using Pseudoboolean SAT solvers for minimisation
Espresso
Minimising using hypergraph transversal tools
Minimisation using Iterative SAT methods
Maxima functions
R QCA package
Minimisation using Weighted MaxSAT
C++ QuineMcCluskey methods
Add todos.
Complete "From groupoids to groups" (MG)
Section "Actions and operations"
Create more todos.
Explain macros (MG) DONE
Overview
Differences between MG_PhDThesis.tex and 2011_SAT_MGOK.tex
Chapter 2  Boolean functions and Satisfiability
Throughout
Introduction
LaTeX corrections/improvements
Continuing with MHash ?
Computing the md5sumvalue of a directory
Bruteforce approach
Relation to hypergraph transversals
The basic algorithm
Using some DNF representation
Backtracking (DPLL)
Parameterisation
Tree pruning for the backtracking approach
Apply it to compute all MUS's, given all MSS's.
Low variabledegrees and high clauselengths
Unsatisfiable nonsingular hitting clausesets
Improve specification
Move to correct place
Improve specification
Move to correct place
Sizes (and structure)
Direct linear representation
Computation of r_kbases
16bit MixColumn operation (2x2 matrix)
Improving notations
Improving usage of Latex
Section "Category of literal structures"
Correction of errors
Transfer to part "Dissertation"
Model checking and variations
BAT
Basic data
r_1bases : mincl_r1 <= 1376
Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 66
Basic data
r_1bases : mincl_r1 <= 1040
Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 60
Basic data
r_1bases : mincl_r1 <= 1052
Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 56
Basic data
Minimising using hypergraph transversal tools : mincl_rinf = 20, num_mincl_rinf=102
r_1bases : mincl_r1 <= 22
Basic data
Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 36
r_1bases : mincl_r1 <= 80
Basic data
r_1bases : mincl_r1 <= 272
Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 42
Basic data
Generating all minimum representations via hypergraph transversals
Links
Basic data
Linear combination
Experimentation:
Strong form
The order of Horn clauses
The reduced forms
Connections to other modules
Add standardised translations
Generalised canonical translation
DONE Translating nonboolean clausesets into boolean clausesets
DONE Add translations for nonboolean clauselists with uniform domain
Connections to other modules
Update the numbersystem
Computation of initial sequences of transversal GTnumbers
Weak specifications
Write docus
Add known Ramsey bounds
Proofs of numbers
Ramsey numbers
Connections to other modules
General organisation
Improving exactf_tau_arithprog
Improving initial_sequence_vdWt
The LRCformula
Transversal and independence numbers
Write Factorial.
What about the generalisations discussed for Power?
Check the usage of boost::test_tools::close_at_tolerance.
Test of different floating point types and test of different return types
Test of characteristic properties (x real, k integer):
Numbers to be included
Improving SplittingViaOKsolver
Other SAT solvers
Targetjournal JSAT
General plans
DONE (now left/rightoverarrows are used, which look somewhat nicer) Is there a better symbol for the minvardegree?
First article
DONE (everything has been transferred resp. generalised) Transfer XSZ's original preprint
Transfer OK's notes
Incorporate XSZ new report (from SAT2009)
Create application tests.
Create unit tests.
Move to stratification submodule.
Add the concept tag (a special case of a "const collection with begin, end and size; not defaultconstructible, but copyable, assignable, equality comparable").
See class IteratorHandling::Arithmetical_progression in General/IteratorHandling.hpp
Complete implementation
To be tested
To be implemented
To be tested
Design of the concept
Update concepts
Write tests
Improve implementation
Create application tests.
Create unit tests.
Move to stratification submodule.
Move to stratification module.
Handling of order
Write tests
What is the meaning of typemembers "reference" and "const_reference" ?
What is the problem questioned in the comment below on "iterator type pointing to value_type" etc. (likely one must have a look into the standard).
Are there containerconcepts proposed at Boost, or for the new standard?
Write a weakening of concept Container which does not require the value type to be assignable (so that std::map and std::multimap are models of this concept).
Likely, for the archetype we should use some predefined constructs (is_convertible etc.).
Actually, it tests something different: For arbitrary objects, a, b, c it is checked that if among the 3 possible pairs two equalities hold, then also the third equality must hold. Is this a good design? The motiviation is, that this test is more general, and can be applied under all circumstances.
Should be an instance of a general transitivitytest.
"reference" and "pointer" are never explained in the standard, and the requirements on iterator concepts don't mention them, but they suddenly show up in the iterator traits (24.3.1) ?
Can expressions "a > m" be expressed ?
Create in TypeTraits.hpp a metafunction "is_derived_or_same", and use it for the definition of InputIterator and elsewhere. Stop  this is now in the new standard library.
Either the assumptions a ~ b and b ~ c become assertions, or the test should be applicable to all a, b, c (fully symmetrical).
Should be an instance of a general transitivity test (see also above).
To conform with the other tests here, it should be applicable under all circumstances?!?
Should be an instance of a general transitivitytest (see already above).
A more complete explanation is needed.
A strategy object should filter the paths (excluding some).
Handling of links needs to be customised (and documented).
Designing a concept; the domain of == allows comparison with the unique pasttheend iterator. The concept InputIterator should refine InputIteratorDefault and MultiPassInputIterator (???).
Using pathequality or pathequivalence ?
Instead of OKlib::Concepts::InputIterator we should require OKlib::Concepts::InputIteratorDefault and MultiPassInputIterator (???).
Testing should also cover the case of symbolic links.
Provide testing of star operator in private member function test_star_operator.
Provide testing of increment operator in private member function test_increment_operator.
Extend testing of equality and inequality operators to nontrivial cases.
For the outputjobs messageclasses should be employed.
Handling of extended Dimacsformat (with real variablenames) is needed:
Correction : DONE
Extensions : DONE
For the output better a messageclass is provided.
Create a concept
Extending the tests (not just checking whether the statistics are right).
Test with the archetype of a CLSAdaptor.
For the negative tests:
For the positive tests:
Test for errors where the numbers readin are too large to be represented.
Once we have fixed the concepts (a bit more), likely we should rename the parameter BijectivityConstraint.
More doxygendocumentation is needed.
TEST IT.
Write a concept.
Enquiry to the boost mailing list, why the matrix concept has no == and =!. (Emphasising that a generic library should exploit its generality, while apparently uBLAS has only numerical computations in mind, ignoring the use of matrices in combinatorics (where the entries are (potentially big) integers, and algebra (where for example matrices over finite fields are considered). It seems that there is no easy way for the user to extend the library so that == and != are available.
TEST IT.
Write a concept.
Here returning the isomorphism found would be very useful. Perhaps this could be done by providing an overload of operator() with three arguments, where the last two arguments are references for the permutations; before doing so a concept of "permutations" is required. Likely a policy is best here, which says what to do with the results, and which also allows to extract further information.
It would be useful to have "matrix expressions" (in uBLAS terminology ?), so that exactly the same as below would be done, but for suitable permutations pr and pc we would just write the test as OKlib::Matrices::is_equal(permutation(m, pr, pc), trans(m)) (as said, this should have the same complexity as the direct approach below).
Over time a great variety of algorithms and implementations for this basic problem should be developed. It arises the general problem, how to name all these different methods for doing the same thing? It would be good to develop a general scheme.
If the permutation generator delivers Graycodes, then an improved implementation should be able to exploit this.
Enquiry to the boost email list, whether somehow uBLAS can handle row and column permutations?
TEST IT.
Write a concept.
Here returning the isomorphism found would be very useful. See discussion above for Is_self_dual.
Having a matrix expression for permuting row and column indices simultaneously would be useful; see the discussion above for Is_self_dual.
TEST IT.
Write a concept.
A nice timing test would be to see whether the simple implementation return ::OKlib::Matrix::is_equal(m, trans(p)); would be just by a factor of 2 slower.
Enquiry to the boost email list why is_symmetric is not provided (see above).
How to generalise Power (and other similar functions), so that boost::mpl::long_ is no longer hardcoded? One problem is, that a corresponding template template parameter X should be defaultet to boost::mpl::long_, and so must come first, but the types of b and e need to be X::value_type ? Perhaps a helper construction is needed. Another problem is, whether we can introduce X as a template template parameter, and write nevertheless X::value_type ? This likely is not possible. Like the concept of a metafunction class, perhaps we should have X as a *class*, with a nested template "apply", which yields the "concrete value" ?! So X is a class with type member X::value_type, and X::template apply<n> yields the concrete value (type) ?! X would be a model of the concept IntegralConstantMetafunction. Power then would be template <class ICM, typename ICM::value_type b, unsigned e> struct Power : ICM::template apply<b * Power<ICM, b, e1>::value> {}; template <class ICM, typename ICM::value_type b> struct Power<ICM, b, (unsigned 0)> : ICM::template apply<1> {};
Code for the factorial function:
An alternative:
Document the class (what's the point of the strange design?).
Can assertions be made about member mutex?
Generalise to Ranges
Write tests
Create an informal concept.
Update the above explanation.
Create a formal concept.
Ask the boost mailing list to correct the wrong "add ..." in the documentation of boost::split. !!
Write two models for the strategy.
Write a convenience function for the type deduction.
A concept is needed.
Test inequality operator.
Extended explanation.
Yet we use a fixed ProgramRepresentationIncludes form (with fixed character type), ignoring the scanner type (the template parameter of the nested class definition). A more perfect solution would create a new parsefunction which then instantiates the IncludeParsingGrammar and ProgramRepresentationIncludes accordingly to the character type actually used.
A concept is needed.
Extended explanation should mention the other implementation.
Management of streamformatflagsresources should be handled by (RAII) object.
Write a test for it.
Create a concept.
Wrong template arguments.
Testing of all functionality (including exceptions thrown).
Add an extended description.
Testing of equality and inequality operators.
Reinstate testing of program strings which are not matched by the grammar.
Add an extended description.
Remove obsolete second test.
Here, as in Test_IncludeParsingGrammar, part of the test involves filling a ProgramRepresentationIncludes object with the include directive /context data from the TestData vector. Could this be extracted to a further test and the result made available to both tests?
Add an extended description.
Testing of equality and inequality operators.
New vector for negative tests.
Improve design so that only the necessary typedefs are public and the data is made available through public member functions.
Improve naming.
Enable access to the sets of SuperSeries, SpecSeries, Benchmark, Solver (via iterators to corresponding maps), and provide computation of the set of "complete" solvers (having solved at least one sat and one unsat instance).
A concept is needed.
Should there be an exception base class for OKlib ?
Actually, "LexicographicalEvaluation" is a misleading  this class provides access to aggregated series results for each solver. So we should rename this class here; LexicographicalEvaluationRandom then is really the lexicographical evaluation (which should be generalised for "Series_with_n" (where "n" should be read as "size")).
The nested typedef numerics_solver_on_series_type should become a freestanding class template with an associated linear order (we should not just have a typedef for a pairtype here, since for pairtypes we should always assume the natural definitions of == and <). A conversion to pair should be given. A concept is needed here (at least FullyConstructibleLinearOrder and the library basics).
Concepts for IndexedDatabase and SeriesPursePolicy are needed.
Make the implementation more efficient by storing intermediate results.
PROBLEM: When restricting to the SAT or to the UNSAT case (see objects rdb_sat and rdb_unsat), then it might happen that in case less then 5 but at least one of the benchmarks in the series has been solved, that we apply the rule for diminishing the series purse by the factor of three to the series, while actually the series had enough SAT resp. UNSAT instances in them.
Additional to the current computation for the SAT+UNSAT category, compute the scores when considering only "complete" solvers.
This class is a "blob"  many things are done here, which should be split over several classes.
Completing like Test_LexicographicalEvaluation.
Checking the average running times.
Checking the order details of the variations on lexicographical ordering.
Provide specification
Write unittests
Improve implementation
Write tests.
Would the use of smart pointers be appropriate?
Handle the rangerequirements correctly.
Provide the mappinginformation in the comments.
Complete the concept
Provide unittests
Complete sequencememberfunctions
Improve implementation
Complete implementation
Write unittests
Complete containerfunctionality
Write unittests.
Improve implementation
Use messages.
Separate the transfer from the unitclause propagation
Harmonise with KLevelForcedAssignments::CLSAdaptorKUcp
Complete specification
Complete implementation
Write unittests
Harmonise with UnitClausePropagation::CLSAdaptorUcp
In a new module Iterators a metafunktion InverseRange<Range> should be implemented (in submodule RangeAdaptors).
The lexicographical order on ranges should become independent (in module OrderRelations).
Add more natural functionality (for example ==, !=).
Create a concept (including providing appropriate container functionality).
More test data!
Test cases are needed where the elements of the associate prefix containers are more complex: Not just sequences of characters, but sequences of containers.
The test data is quite obscure; the reversal of order is very unnatural. The test cases here have nothing to do with the module Refactoring !!
No hierarchy; template parameter instead.
What is the meaning of the *two* vectors?
Static data member should need no constructor!!
Replace old tests.
Test for extensions, where no extension is possible.
More test cases.
Design an informal concept.
Once a concept has been created, test the syntax.
There should also exist another version which returns the function value as a copy.
Via an errorpolicy there should be the possibility to throw an exception in case of an argument not in the domain.
Improve implementation
Create the concept
Systematic tests of all 8 combinations for the tags.
Tests for all standard containers (vectors, lists, deques, sets, multisets) usable for sets.
Tests, where objects are dynamic, for example strings.
Tests using random sequences; so in Subsumption_Tests.hpp also some simple reference implementation should be provided.
Test also the concept.
Error reporting: Indices.
Test also the concept.
Error reporting: Indices.
Test also the concept.
Error reporting: Indices.
Should this class go to a general output facilities module?
Should this class go to a general output facilities module?
Complete it.
Doxygen documentation.
Improve the output (a more systematical approach for better structuring; and replacing the use of trivial messages).
DONE (outputting "NA" in case field does not exist) Handling splitting output
Write extraction tool
Rproblem with read_oksolver_mon
Objectoriented syntax
Function plot_oksolver_mon_nodes
Function summary_oksolver
Function hist_oksolver_mon_nodes
Differences to the original OKsolver2002
Annotated tree output
Improving the implementation
Tree pruning ("intelligent backtracking")
Local learning
Adding lookahead autarky clauses
Counting satisfying assignments
Once we are ready to start, a new submodule is needed
Update namespaces
First in computeralgebra
Create first milestones.
Create detailed milestones until completion
New planning
Once we are ready to start, a new submodule is needed.
Update namespaces
Planing: Set up milestones etc.
Goals
DONE (there are no alliances anymore in version 2, and also no need to distinguish between original and learned clauses, since learning is always accompanied by a restart (in a sense)) OKsolver_2 extends OKsolver_1 by using alliances of active clausesets with (at least) three members :
DONE (not done, since there are no active clausesets) Further subdivision of the instance
Afterburner for learning
Preprocessing
Reductions
DONE (this topic should be moved to version 3) Equivalence reasoning
Memory management
DONE (in the form as discussed no longer appropriate, since extracting learned clauses is now just a trivial extension of OKsolver2002, based on the set of variables used in the refutation (as shall be the extended autarky search), and there are no alliances of active clausesets anymore) Autarky search
Incomplete methods
Organising autarky search
Autarky extension
More autarky search
DONE (no longer appropriate here, since there is no "dynamic" clause learning (on the fly) anymore; the activitybased ideas could be considered for OKsolver version 3) Heuristics
Local search
DONE (the open questions now are about selfabortion and full restart, and that's a question of the timeprediction) Restart policy
DONE (the context changed now, but the basic principle is the same: consider a given total time as given, and if the prediction is more than that by a certain factor, one must restart, i.e., abort the process) Timeprediction
DONE If restarts don't yield clear benefits, then they are not incorporated into OKsolver_2_0, but the whole issue is thoroughly treated with OKsolver_3_0.
Monitoring the search process : needs UPDATE (relevance unclear)
Parameter settings
Once we are ready to start, a new submodule is needed.
Update namespaces
Parallelism
Distributed solving
Progress measurement
Module KLevelForcedAssignments is used, going (much) beyond r_2.
Methods based on graph splitting are used now.
Constraints
Hard examples
Autarkies
Belief propagation
Finally, OKsolver3.0 handles also quantifiers.
COINOR
Linear and integer programming
Local search
The following todo's are about the reusable components in QuantumPhysics/OrthogonalTriples.cpp, which should be moved to appropriate library files (where they are tested).
Output CNFs SAT_translation should use the components in InputOutput.
Input and output of graphs
Input and Output Use Messages and ProgramOptions.
Linear algebra Move the components
Hypergraphs In output_remaining_edges, output_hypergraph and extract_triangles a certain interface for hypergraphs is used  compare this with the concepts for hypergraphs (see Hypergraphs/concepts/plans/general.hpp).
Orthogonality relation The function orthogonality_relation should be generalised, so that an arbitrary binrary predicate can be used.
Extract triangles The function extract_triangles should go into the general graph/hypergraph module. Are there better algorithms?
Copying graphs Why does
We need a new function "completion", which, given a point configuration, adds the unique orthogonal direction to every pair which is not contained in a triple. For the Peres 33point configuration one then needs to check, whether the 24 pairs yield 24 new points (likely not). The completion happens via the vector product, and another function checks whether two directions given by two vectors are equal or not.
DONE Package directory structure
Providing update mechanisms for the packageclone
CreatePackage extensions
Connections
Boolean partial assignments
Exceptions
Improvements of InputOutput::ReadPass
Write unittests
How to use boost::filesystem better?
The functionality of this applications should go into its own component (so that this application just becomes a wrapper).
Document it precisely.
Write extensive tests.
Use InputOutput::CLSAdaptorDIMACSOutput
Use Messages
First concepts for permutations are needed.
Now we know what a permutation is, we need a standard way of enumerating permutations.
One should study the permutation generator from the C++ standard library (it is unclear whether this thing handles equivalent objects or not; I assume it does). Likely this generator must be relatively inefficient, since it must always compute the supporting structure from scratch; thus it's a kind of "nonintrusive" generator, while a more efficient generator would be "intrusive".
Implement lexicographic enumeration
Implement enumeration with only one neighbourswap to get to the next permutation. This is the equivalent to Graycodes (see GrayCodes.hpp), and similar considerations apply).
Standard variable ordering for extendedpigeonhole formulas
Update the phpfunctions
Extended Resolution clauses for the Pigeon Hole Principle
DONE Add tests for weak_php_ext_fcs
Connections
Finding the n where a problem series changes from SAT to UNSAT
Simpler strategies
Links
Scope
Definitions and probability calculations
Poker assistant
Missing pgsql/libpqfe.h
Improvements
Better error messages
Write application tests
Tests
Organisation
Best method for prime_clauses_cs
Improving min_extdp_cs
min_2resolution_closure_cs
Dualisation
Connections
Hitting clausesets
contained_prime_implicate
Connections
Enumerating prime numbers
count_primes
product_primes
The wider framework
Specifications for ProbabilityOfSuperiority.R
Write docus
Better stopping
More powerful processing options
DONE (available now with ProcessiCNF) Option for using only decision variables with ProcessSplitViaOKsolver
An extended explanation is needed.
A concept is needed.
Test inequality operator. (OK: ?? Always test equality and inequality together, applying the appropriate generic test facilities from the concept definitions.)
Swi Prolog
Gnu Prolog
php_ext_resl
Resolution trees
Resolution proofs
Readonce resolution proofs
Install pseudoboolean solvers
Tools for PB > SAT translation
minisat+ input format
borgpb
clasp:
SAT4J:
BoolVar/PB
Finding sources
Duaffle
MiniQbf
Connections
Specify the order of the outputclauses
Understanding the costs of the current implementation
Running only through the levels
Quine/McCluskey in general
Make QuineMcCluskey read from standard input
Various versions for different values of NUMBER_VARIABLES
Docus
Application tests
Maxima level
Input and output
Performance analysis and code analysis
Fixed number of variables
Extend unit tests
pow3 should be replaced by an array computed at compiletime
Improvements of the implementation
Parallelisation
Precise definitions, and basic types
Specification
Tests for statistics levels
Preparations for computing optimum representations
Improving efficiency
DONE (see QuineMcCluskeySubsumptionHypergraphWithFullStatistics.cpp and QuineMcCluskeySubsumptionHypergraphFullStatistics.cpp) Add option to generate statistics files
DONE Write application tests
DONE Standardise name of prime implicates file
Failing tests
DONE (installed 2.14.0) Installing 2.12.1
DONE (building now with current gcc, that is, version 4.5.2, which has Gmp and Mpfr statically linked) Local installation of gfortran
Packages
Improving the docuspage
Building dvi,pdf,infodocumentation
Connections
Basic functionality
Checking regularity
Known Rado numbers
Ramsey hypergraphs
Generalised Ramsey hypergraphs
Strengthen connection to Maxima/Lisp level
Move todos to this file
Write unit tests
Add generator to generate general Ramsey problems
See ComputerAlgebra/Hypergraphs/Lisp/Generators/plans/Ramsey.hpp
Update the underlying notion of "hypergraph"
General information
Using DPLL and Conflict driven solvers
General information
Using DPLL and conflictdriven solvers
General information
Using DPLL and Conflict driven solvers
General information
Using DPLL and Conflict driven solvers
Using UBCSAT
MG must completely update this file!
Create a systematic naming scheme
Implement the general (i.e., nondiagonal) boolean case
Provide specification for all the functions
Extend Ramsey symmetry breaking generators to generate Extended Dimacs
Relations to other modules
Extreme cases
Improve docus
More efficient computation
Symmetry breaking by using symmetries of the solution space
Symmetry breaking by using Ramseysymmetries of the clauseset
Symmetry breaking by recursive application of pigeonhole principle
Considering only labellings with bounded number of particular colours
Reimplement "Symmetry breaking by using %Ramseysymmetries of the clauseset"
Generators for all standard Ramsey problems
Software by Pascal Schweitzer
Software by Aaron Robertson
Random subsets, sublists etc.
Specifying the AES random generator
Implementing the AES random generator
Filtering out
DONE (moved to ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Basics.mac) Move random_full_fcs
Implementation
Overview on theoretical possibilities
Connections
Create application test
Create unit tests
Enhance the table
Better error codes
Write wrapper script
Use Messages
Improved usage of Gmpfacilities
Better algorithms
Relations to other parts
Organisation
The notion of a base of a clauseset relative to some reduction
Considering special reductions
Application to the representation of boolean functions
Sampling of rbases
Computing minimum rbases
Preprocessing
Creating an htmlversion
Connections
rbased clausesets
Positive representations
Implement the reductions from the Kullmann/Luckhardtpreprints.
Implement bounded resolution.
All kinds of binaryclause reasoning are handled by module FailedLiteralReduction, or?
Write doxygendocumentation for Concepts::IncludeDirective.
Transfer the tests to the new test system.
The whole approach needs to be thought over.
Create milestones
ReingoldTilford algorithm at abstract level
The full ReingoldTilford algorithm
ReingoldTilford algorithm in Maxima.
Implement (similar to TestReflexivity) tests for:
Implement tests for
Implement the following induced relations (in module OrderRelations)
Improve the tests (so that they become more meaningful).
Developers
Release plan
ExternalSources repository
Special tag
Improved releases
Finding hard unsatisfiable hitting clausesets
Hardness
To be completed (see module SATCompetition, and there mainly SATCompetition/SingleResult.hpp).
Once subdirectories of modules are fully supported, these concepts should go to Concepts/CompetitionEvaluation.
Expand docus
Migrate the mupadcode.
Terminology (DONE Moved to ComputerAlgebra/Cryptology/docus/Rijndael.hpp)
Proper testing!
With C++09 stdint.h likely is to be replaced by cstdint.
Connections
Overview
First tests AES
Further tests
Problem specification
Naming
Basic data
Minimum representations using weighted MaxSAT : mincl_rinf <= 396
r_1bases : mincl_r1 <= 2712
Fix binary cardinality constraints lemmas
Add lemmas and definitions for *all* "nonclashing" matrices results
Tidy "nonclashing matrices" lemmas
Define target(s) for PhD
Update "Clauseset representations" section
Update "AES" section with latest definitions
Update "Representations of boolean functions" section with latest proofs.
Finish topological proof of vdW theorem section
Cardinality constraints
Consider preprocessing / recombination idea w.r.t. PHP
Clause set automorphisms vs Ramsey problem automorphisms
Literature research
Ten challenges
More precision
Add section on combinatorial enumeration
Writeup Ramsey's theorem and proofs
Update and extend generators for Ramsey problems
Evaluation of measures
Symmetries of Ramsey problems
Various Ramsey type problems to be investigated
Tuning and understanding of local search
Solvers and tools for solving Ramsey problems
Exploiting solution patterns
Make solutions from the literature available
Special methods
Processing of [Introduction to Boolean Algebras]
Update "Data matrices" section : DONE
Using homomorphisms in resolution proofs
Relating isomorphisms of clausesets with isomorphisms of graphs
Relations to graph theory
Bicliques
Biclique partitions
Write test cases according to my postings to the Boost mailing list (October 2005).
Another submodule needs to be created, which gives access to the platform specifics like __WORDSIZE.
Uniformly sampling biclique partitions
Random processes
Sampling maximal vertexbicliques
Sampling maximal edgebicliques
Parallel SAT solvers
SAT solvers
(P)Lingeling
Install Relsat
Improvements of CryptoMiniSat
Add todos for SATRace 2010 SAT solvers
Glucose outputs to STDERR not STDOUT (DONE solved with version 2.0)
Fuzzing
Write docus for March
Write docus for Satz
Write docus for Minisat
Update of GRASP
Installation in general
CryptoMiniSat : DONE
Documentation for CryptoMiniSat
Glucose
SAT4J
Jat
SMT (SAT modulo theories)
Minisat
Picosat
Precosat
March solvers
Experiment monitoring tools
Argo
Satz
MiniMaxSAT
EBDDRES
Walksat
BASolver
HeerHugo
SatMate
SIMO? SIM?
Kcnfs
Belief and Survey propagation
tts
2cl
Modoc
DONE (Hantao Zhang considers it as obsolete, and doesn't want it to be included) Sato
Boehm solver
CSat
Posit
Answer set programming
Symmetries
Maxsat
Counting
DONE (no need to do something here; the number of unitpropagations is not interesting, and the extraction tools shall just return 0 for numbers of conflicts etc.) Correct solvers with poor handling of trivial CNFs
Update and completion of plans regarding SAT 2011
Benchmarks for SAT 2012
Categories / "tracks" for SAT 2011
Variables
Value set
Total assignments
Domain association and allowed total assignments
The notion of "condition"
Constructing conditions
Functions for conditions
Backdoors
The simplest method is to compute the (exact) probability that a random assignment satisfies the instance (used in the old OKsolver).
Approximating the exact probability via inclusionexclusion
Experimentation
Counting falsifying assignment
Connections
Statistics on the performance of SAT solvers
Basic data
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 67)
1base : mincl_r1 <= 124
Move Sbox1specific investigations here
Basic data
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 67)
1base : mincl_r1 <= 129
Move Sbox1specific investigations here
Basic data
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 68)
1base : mincl_r1 <= 138
Move Sbox1specific investigations here
Basic data
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 69)
1base : mincl_r1 <= 128
Move Sbox1specific investigations here
Basic data
Overview
Combining Sbox with field addition
Generating all minimum representations via hypergraph transversals
Basic data
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 67)
1base : mincl_r1 <= 134
Move Sbox1specific investigations here
Basic data
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 66)
1base : mincl_r1 <= 136
Move Sbox1specific investigations here
Basic data
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 67)
1base : mincl_r1 <= 123
Move Sbox1specific investigations here
Basic data
Overview
Move individual investigations to submodules
Computing a minimum CNF represention : mincl_rinf <= 294
Using weighted MaxSAT to compute small CNFs
Minimum using exact espresso algorithms
Small CNFs with espresso
Using R QCA package
r_1bases : mincl_r1 <= 4398
Generate good CNF hitting clausesets
Analysing the AES prime implicates
Extracting prime implicate representations from the hittingclsrepresentations
Find the symmetries of the AES Sbox DNF
Basic data
Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 69)
1base : mincl_r1 <= 152
Move Sbox1specific investigations here
Connections
Add decomposed Sbox operations
Representations of the Sbox using additional variables
Other software systems offering Sbox translations
Rename to WSchur_BHR.cpp<p>Create complete specifications
Write modification to handle ordinary Schurproblems
Finding short treeresolution proofs
Regularresolution complexity
How to compute the minimal DPresolution complexity?
Resolution complexity
2CNF
Finding short resolution proofs via SAT
The role of maximal bicliques
Finding interesting biclique partitions
Searching pandiagonal latin squares
SAT translations
Further properties
deharmonise_eval_2
Transformations
New module ComputerAlgebra/Sets
Naming conventions
Unions and intersections
Computing all ordered tuples
Set creation
Function min_elements
Function max_elements
Minimal elements for convex setsystems
Connections
The general setting
Implementing the recursive algorithm according to [AB, Moller]
Connections
More information on the splittings
The order of the md5sumcomputation (SplittingViaOKsolver)
Script for applying partial assignments
Improving SplittingViaOKsolver
Good splitting
Computing a splitting tree
Distributing the tasks to machines
Are non1singular tuples totally singular?
Special properties of the greedoid of singular sets
Docus
Generating test vectors
DONE (Handled in "Notions and notations" in ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/plans/general.hpp) Datatypes and naming conventions
DONE Add decomposed Sbox boxes
Write application tests
Improving speed
Create milestones.
Links
Performance of Satz
Performance of OKsolver2002
Performance of march_pl
minisat2.2.0
glucose2.2
cryptominisat 296
precosat570
lingelingalab02aa1a121013
CubeandConquer (SplittingViaOKsolver)
Performance of OKsolver2002
Performance of march_pl
Performance of satz215
Performance of conflictdriven solvers
SplittingViaOKsolver
Move CLSAdaptorSortByClauseLength
Move AllEqual to OrderConstructions
Merge with SortByClauseLength.cpp
DONE Add application tests
Connections
Write tests
optimal_splitting_tree and optimal_r_splitting_tree
Processing splitting trees
optimal_r_splitting_tree
Direct encoding
Direct encoding and full symmetry breaking
Palindromic problem (direct encoding)
Palindromic problem with full symmetrybreaking (direct encoding)
Weak palindromic problem with full symmetrybreaking (direct encoding)
Comprehensive statistics
Further statistics
Naming
The only test available yet, Test_ContainerConcept, actually is a metatest (testing the concept), so this should go (with the new test system, and once arbitrary directorynesting is avaiable) to Concepts/tests/tests.
Write tests for Concepts::Container.
The notion of a "straightline program"
The notion of a "boolean circuit"
Other translations (than the Tseitin translation)
InjectivityConstraints:
Graph colouring conversion
Update namespace
Create milestones
General algorithm
Concepts
Organisation and connections
Algorithmic framework
Refinements
Connections
Iteration through lexicographical order
Improving colexicographical unranking
Enumerating all ksubsets in Graycode manner
The notion of a "literal substitution":
standardise_fcs
Move todos
Better algorithms
Improve code quality
Organisation
More unit tests
Test performance of Subsumption_Hypergraph generator
Offering live subsumption hypergraph generation
Relations to other modules
Implement the four mixed cases for the direct translation
Further improve implementation
Random Sudoku problems
Enumerating all solutions
Sampling of all solutions
Sampling of minimally uniquely satisfiable problems
Sudoku generator for the Minion constraint solver
Relations
Input file format:
Complete implementation of OKlib::LatinSquares::SudokuProblem
Complete implementation of OKlib::LatinSquares::Trivial_reduction_Sudoku
Test OKlib::LatinSquares::SudokuProblem<p>Test OKlib::LatinSquares::Trivial_reduction_Sudoku<p>Strong hypergraph colouring
Another representation of Sudoku uses one Latin square plus N*N bijectivity constraints (for the boxes).
As a prototype, implement Sudokusolvers.
Visualisation of the runs of solvers
Concepts:
Design and implement
Implementations
Acronyms
Computing powers, based on the cycle representation
Automorphisms
Full symmetrybreaking
Embedding coloursymmetrybreaking into the search
Enumerating all solutions without coloursymmetryrepetition
Relations between palindromic hypergraphs
Vertex degrees and their distributions
Handling symmetries using extended resolution
Performance of symmetry breaking by fixing monochromatic cliques
Using cardinality constraints
General look and feel
New target for main action
Target "all":
Target "check"
Target "prebuild"
Target "html"
Target "app_tests"
DONE (likely not needed, since at least for now we don't use cmake) Target "reset"
Target "newmodule"
Connections
Efficient computation of the taufunction:
Experimentation
Decision
Theory
Versions before version 2.0
Towards version 2.0
Version 2.0 and later
With tauprojection
Performance evaluation
Version 1.0
From version 1.0 to the version before the improved heuristics
Improving the heuristics (and the implementation)
With tauprojection
Performance evaluation
TestSystem::TestBase
Unknown exceptions
Encapsulation
Testing
Transition
TestSystem::messages::TestException : DONE
OKLIB_TEST_EQUAL : DONE Update the implementation according to TestSystem/TestExceptions.hpp.
TestSystem::messages::ErrorDescription (in TestSystem/messages/TestExceptions.hpp) : DONE
Offer a generic OKLIB_TEST_EQUAL_W* macro
More errorinformation
Test TestSystem::messages::ErrorDescription
OKLIB_TEST_RETHROW_NO_LOG
Transition
Overhaul of the testmacros (like OKLIB_TEST_EQUAL) seems to be needed
Update
New test system
Messages
Infos
ProgramOptions
Transition
General threshold functions
Cardinality constraints
The basic symmetric functions
Time and Date: Representations of time and date should move from General to Messages.
Improving Messages::Utilities::TimeDateStandardImplementation On the one hand it would be nice if we could specify different levels (say, the given implementation as "full", one implementation without timezone, seconds and day as "basic", and one implementation with full names for day and month (possibly also with daynumber and weeknumber) as "extensive"), but since this is not provided by the standard, we had to define it all ourselves (that is, the order of the components). So perhaps the given implementation is a reasonable compromise. (But the best thing would be if the format string could be determined, and then one would simply replace the abbreviated forms by their full forms, and potentially add something.)
Functions currentDateTime should go to module Messages.
Which components should be replaced by components from Boost ?!
Counting falsifying assignments found
Alternative sampling
Using the predictions
Software components
Improving CRunPdVdWk1k2
Script for searching for a vdWnumber
Version of RunVdW3k for palindromic problems
Submodules
Test all metafunctions.
Hypergraph transformations I
Hypergraph transformations Ib
Hypergraph transformations II
Parameters for encoding
Edgecentered SAT encoding
Vertexcentred SAT encoding
Transformations
Basic translation
Translation to SAT according to Liffiton and Sakallah
Simplify AES translation
Handling external data
Order of small scale matrix dimensions
Rewrite ncl_list_ss correctly
Remove AESspecific translation
Complete small scale helper functions
Standardise output files names
How to represent elements of arbitrary fields as boolean variables?
Provide additional translation into CSPsolver format
Write docus
Generate translation that allows multiple plaintext/ciphertext pairs
Translations reducing the lengths of clauses
Translations reducing the number of variableoccurrences
Standard "box" translations
The canonical box translation
The 1base box translation
The "minimum" box translation:
Standard "box" translations
The canonical box translation
The 1base box translation
The "minimum" box translation:
Treeresolution complexity
Treeresolution refutations found by simple algorithms
Developing a formula (now for the numbers of leaves)
Short proofs with the hitting proofsystem
Create milestones.
Investigate existing software
ReingoldTilford algorithm outline
Four aesthetic criterions for ReingoldTilford algorithm
Environment
Applications
Connections to other modules
Implementing the Tseitintransformation (with variations)
Horn specialities
Translations to CNF/DNF
Reorganisation
Optimisation
Renaming the file to "CanonicalTranslation.mac"
Add statistics
Translation of boolean circuits into boolean CNFclausesets
Understanding dualts_fcl
Strengthening dualts_fcl by adding some redundant clauses
Turing machines: general plans
Types of Turing machines
More readable large numbers
Better output
Update to version 1.2.0
Make clear the required package for dos2unix
Computing r_1bases for a set of prime implicates
Random r_1bases
Random shuffling
Random number generation
Shuffling and sorting
Improve efficiency of Bases/RUcpGen.cpp
Improve efficiency of Bases/RUcpBase.cpp
Further improve implementation of Bases/RUcpBase.cpp
Further improve implementation of Bases/RUcpGen.cpp
Create unittests for Bases/RUcpBase.cpp
Create unittests for Bases/RUcpGen.cpp
Shall uhit_def be redefined with every loading?
Problems with evaluation
Organisation
Connections to other modules
Tests
uhit_def
uhit_n : DONE
Evaluating the catalogue
New entries
ExternalSources for larger datasets
Reduction by 2subsumption resolution
Boolean functions representing unary addition
CNF and DNF representations of unary addition
Smallest prime CNFrepresentation
Smallest r_1based CNFrepresentation without new variables
Smallest r_2based CNFrepresentation without new variables
Better names
Improve efficiency of UnitClausePropagation(W).cpp
Connections
The most basic form of UCP
Translation via addition
Lookahead solvers with translation via addition
Conflictdriven solvers with translation via addition
Local search solvers with translation via addition
Using CSP solvers
General plans
Performance of Minisat
Performance of OKsolver2002
Relations to preprocessing
Considering diagonal (boolean) problems and full representations
Finding interesting inferences
Install version 3.6.0 : DONE
Update
Connections
Create tests
Checking certificates
Connections
Update
Speed of PdVanderWaerdenCNF.cpp
palindromise_vdw_ohg
DONE (now the implementation is nonrecursive, and in case more memory is needed, use default_memory_ecl()) Hypergraphs of arithmetic progressions
DONE Transfer Applications/RamseyTheory/plans/Van_der_Waerden_hypergraph.hpp to here
Generator
DONE Update namespace usage
New test system
Update
Literature overview
vanderwaerden_3(3,3,3) = 27
vanderwaerden_3(3,3,4) = 51
vanderwaerden_3(3,3,5) = 80
Overview
vanderwaerden_3(3,4,4) = 89
Known from the literature
vdw_3(4,4,4) > 150
Creating instances
vanderwaerden_3(3,3,3)
OKsolver_2002
march_pl
satz215
Minisat
The behaviour of m > vanderwaerdend(m,3)
Connections
Organisation : DONE
Standardisation
Statistics
Systematic output and outputfunctions
Palindromic versions with arithmetic progressions of length 3
Alternative handling of parametervalues 2
DONE More than two parts
Symmetry breaking for vdWproblems
Update namespaces.
For the future perhaps we should use a call traits instead of the fixed argument type const L& ?
Complete doxygendocumentation.
Transfer tests to the new test system.
Complete VariablesAsIndex_basic_test by applying tests:
It seems now artificial to me that variables are ordered by < : There is no default meaning  it could be the order as found in the input, or the order in the quantifier prefix, etc. So only refinements extend == to a linear order, using special predicate names, and there are refinements using <, which then is purely implementationdefined (for pointers for example, while for variables with index it's the index).
Variables can have *domains*, which are types (with values), for example bool or enumerations. Partial assignments restrict these domains further. Refinements allow only special domains, for example an enumeration with N values, or bool.
Categories
Active clausesets use "variable structures" to manage their variables, allowing for example to run through them, etc. These variable structures should have a type member showing which combination (OK: of what?) is possible (in principle).
Specify draw_lrt
Better organisation
Create milestones
DONE A basic example of visualising a tree using Gnuplot
DONE Full implementation of tree drawing using Gnuplot
Colouring schemes
draw_lrt_x