OKlibrary  0.2.1.6
Todo List
File 06.hpp

Picosat913

OKsolver_2002

SplittingViaOKsolver

File 06.hpp

Basic statistics for n=1132

Local search solvers

Upper bounds

Determining the best ubcsat-algorithm for palindromic problems

vdw_2^pd(6,6) = (567,1132)

File 07.hpp

Best local search solver

vdw_2(5,7) >= 260

Using SplittingViaOKsolver

vdw_2^pd(5,7) = (227,236)

File 07.hpp

vanderwaerden_2(6,7) > 1155

Best local-search solver for palindromic problems

vdw_2^pd(6,7) >= (591,1156)

File 07.hpp

vanderwaerden_2(7,7) > 3703

Best local-search solver for palindromic problems

vdw_2^pd(7,7) >= (1544,1547)

File 08.hpp

OKsolver_2002

march_pl

Picosat913

SplittingViaOKsolver

Local search

File 08.hpp

Best local search solver

vdw_2(5,8) > 330

Best complete solver for palindromic problems

Best local-search solver for palindromic problems

vdw_2^pd(5,8) = (312,323)

File 08.hpp

Best local-search solver for palindromic problems

vdw_2^pd(6,8) >= (655,1168)

File 09.hpp

Best local-search solver for palindromic problems

vdw_2^pd(6,9) >= (943,1382)

File 09.hpp

Complete solvers

Parallelisation via SplittingViaOKsolver

Best ubcsat-solver

vanderwaerden_2(4,9) >= 309

vdw_2^pd(4,9) = (300,309)

File 09.hpp

vdw_2(5,9) > 472

Best complete solver for palindromic problems

Best local-search solver for palindromic problems

vdw_2^pd(5,9) >= (446,473)

File 0_23_13.hpp

Problem specification

Using the canonical box translation

Using the 1-base box translation

Using the "minimum" box translation

File 1.hpp

Overview

Using the canonical translation for the S-box (6-to-4)

Using the 1-base translation for the S-boxes (6-to-4)

Using the canonical+ translation for the S-boxes (6-to-4)

Using the canonical CNF translation for the S-boxes (6-to-4)

Using the "minimum" translation for the S-boxes (6-to-4)

File 10.hpp

vanderwaerden_2(4,10) > 328

vdw_2^pd(4,10) = (320,329)

File 10.hpp

vanderwaerden_2(5,10) > 668

Best complete solver for palindromic problems

Best local-search solver for palindromic problems

vdw_2^pd(5,10) >= (595,612)

File 10_13.hpp

Overview

Using the canonical translation

File 10_13.hpp

Problem specification

Using the canonical box translation

Using the "minimum" box translation

Using the 1-base box translation

File 10_13.hpp

Problem specification

Using the canonical box translation

Using the "minimum" box translation

File 11.hpp

Best ubcsat-solver

vanderwaerden_2(4,11) > 358

vdw_2^pd(4,11) = (343,348)

File 11.hpp

vanderwaerden_2(5,11) > 766

Best complete solver for palindromic problems

Best local-search solver for palindromic problems

vdw_2^pd(5,11) >= (748,767)

File 12.hpp

vanderwaerden_2(5,12) > 962

Best local-search solver for palindromic problems

vdw_2^pd(5,12) >= (950,963)

File 12.hpp

Best ubcsat-solver

vanderwaerden_2(4,12) > 401

vdw_2^pd(4,12) = (387,394)

File 13.hpp

vanderwaerden_2(4,13) > 569

vdw_2^pd(4,13) >= (519,538)

File 13.hpp

vanderwaerden_2(5,13) > 1204

Best local-search solver for palindromic problems

vdw_2^pd(5,13) >= (1176,1205)

File 14.hpp

OKsolver

satz215

SplittingViaOKsolver

Palindromic numbers

File 14.hpp

vanderwaerden_2(4,14) > 681

vdw_2^pd(4,14) >= (617,682)

File 14_13.hpp

Problem specification

Using the canonical box translation

Using the "minimum" box translation

File 15.hpp

OKsolver

satz215

Splitting via OKsolver

vdw_2^pd(3,15) = (200,205)

File 15.hpp

Best ubcsat-solver

vanderwaerden_2(4,15) > 747

vdw_2^pd(4,15) >= (724,727)

File 16.hpp

OKsolver

satz215

minisat2

Splitting via OKsolver

vdw_2^pd(3,16) = (232,237)

File 16.hpp

Best ubcsat-solver

vanderwaerden_2(4,16) > 871

vdw_2^pd(4,16) >= (824,839)

File 17.hpp

vanderwaerden_2(3,17) >= 279

Palindromic numbers

File 17.hpp

Best ubcsat-solver

vanderwaerden_2(4,17) > 1112

vdw_2^pd(4,17) >= (855,1076)

File 18.hpp

vanderwaerden_2(3,18) >= 312

Palindromic numbers

File 19.hpp

vanderwaerden_2(3,19) >= 349

Palindromic numbers

File 1_13.hpp

Overview

Using the canonical box translation

File 1_13.hpp

Problem specification

Using the canonical box translation

Using the "minimum" box translation

Using the 1-base box translation

File 1_13.hpp

Problem specification

Using the canonical box translation

File 1_13.hpp

Problem specification

Using the canonical box translation

File 1_13.hpp

Problem specification

Using the canonical box translation

File 1_13.hpp

Problem specification

Using the canonical box translation

Using the 1-base box translation

File 1_13.hpp

Problem specification

Using the canonical box translation

File 20.hpp

vanderwaerden_2(3,20) >= 389

Palindromic numbers

File 20_13.hpp

Overview

Comparison of box translations

Using the 1-base box translation

Using the minimum box translation

Using the canonical box translation

Using the canonical CNF box translation

File 20_13.hpp

Problem specification

Using the canonical box translation

File 20_13.hpp

Problem specification

Using the 1-base box translation

Using the minimum box translation

Using the canonical box translation

Using the canonical CNF box translation

File 20_13.hpp

Problem specification

Using the canonical core round box translation

Using the canonical box translation

File 21.hpp

vanderwaerden_2(3,21) >= 416

Palindromic numbers

File 22.hpp

vanderwaerden_2(3,22) >= 464

Palindromic numbers

File 23.hpp

vanderwaerden_2(3,23) >= 516

vdw_2^pd(3,23) = (506,507)

File 24.hpp

vanderwaerden_2(3,24) >= 593

vdw_2^pd(3,24) = (568,593)

File 25.hpp

vanderwaerden_2(3,25) > 655

vdw_2^pd(3,25) = (586,607)

File 26.hpp

vanderwaerden_2(3,26) >= 727

vdw_2^pd(3,26) = (634, 643)

File 27.hpp

vanderwaerden_2(3,27) >= 770

vdw_2^pd(3,27) = (664, 699)

File 28.hpp

vanderwaerden_2(3,28) >= 827

Palindromic numbers

File 29.hpp

vanderwaerden_2(3,29) >= 868

Palindromic numbers

File 2_13.hpp

Problem specification

Using the canonical box translation

Using the 1-base box translation

Using the "minimum" translation

Using the canonical CNF translation

File 2_13.hpp

Problem specification

Using the canonical box translation <u>l Translation of aes(2,4,2,4):

File 2_13.hpp

Problem specification

Using the canonical box translation <ul Translation of aes(2,1,16,8):

File 2CNF.hpp
Design for the algorithm "sb-2cnf" from [Nishimura, Ragde, Szeider; 2004, Detecting Backdoor Sets with Respect to Horn and Binary Clauses] (developers SS, MS, OK)
File 3.hpp

Overview

Using the Massacci DES translator

Using the canonical translation for the S-boxes (6-to-4)

Using the 1-base translation for the S-boxes (6-to-4)

Using the "minimum" translation for the S-boxes (6-to-4)

Using the canonical CNF translation for the S-boxes (6-to-4)

File 30.hpp

vanderwaerden_2(3,30) >= 903

vdw_2^pd(3,30) >= (844,855)

File 31.hpp

vanderwaerden_2(3,31) > 930

vdw_2^pd(3,31) >= (916,931)

File 32.hpp

vanderwaerden_2(3,32) > 1006

vdw_2^pd(3,32) >= (958,963)

File 33.hpp

vanderwaerden_2(3,33) > 1063

vdw_2^pd(3,33) >= (996,1005)

File 34.hpp

vanderwaerden_2(3,34) > 1143

vdw_2^pd(3,34) >= (1054,1081)

File 35.hpp

vanderwaerden_2(3,35) > 1204

vdw_2^pd(3,35) >= (1114,1155)

File 36.hpp

vanderwaerden_2(3,36) > 1257

vdw_2^pd(3,36) >= (1186,1213)

File 37.hpp

vanderwaerden_2(3,37) > 1338

vdw_2^pd(3,37) >= (1272,1295)

File 38.hpp

vanderwaerden_2(3,38) > 1378

vdw_2^pd(3,38) >= (1336,1369)

File 39.hpp

vanderwaerden_2(3,39) > 1418

vdw_2^pd(3,39) >= (1406,1411)

File 3_13.hpp

Problem specification

Using the canonical box translation

File 4.hpp

Overview

Using the Massacci DES translator

Using the canonical translation for the S-boxes (6-to-4)

Using the 1-base translations for the S-boxes (6-to-4)

Using the "minimum" translation for the S-boxes (6-to-4)

File 4_13.hpp

Problem specification

Using the canonical box translation

Using the 1-base box translation

File 4_13.hpp

Problem specification

Using the canonical box translation

File 5.hpp

Overview

Using the Massacci DES translator

Using the 1-base translation for the S-boxes (6-to-4)

Using the "minimum" translation for the S-boxes (6-to-4)

Using the canonical translation for the S-boxes (6-to-4)

Applying SplittingViaOKsolver

Systematic investigation of SplittingViaOKsolver for 1-base-instances

File 5_13.hpp

Problem specification

Using the canonical box translation

Using the 1-base box translation

File 5_13.hpp

Problem specification

Using the 1-base box translation

File 6.hpp

Overview

Using the 1-base translation for the S-boxes (6-to-4)

Using the "minimum" translation for the S-boxes (6-to-4)

Using the canonical translation for the S-boxes (6-to-4)

File ActiveClauses.hpp

Links

Partitioning into active clauses

Active clauses for field operations

File ActiveClauseSets.hpp

The following needs to be updated.

Dictionary: (The following is out-dated! "clause" -> "active clause" and "clause-set" -> "active clause-set")

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 clause-model ?!

For a "strong ACLS" all above operations are poly-time 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 clause-model? XXX This seems to be the point of speaking of "active clause-sets".

CNF versus DNF

File AdditiveNumberTheory.hpp

Connections

Some further considerations

Finding the first arithmetic progression

The conjecture from [Granville 2006]

The first arithmetic progression allowing a missing number

File AdvancedEncryptionStandard.hpp

Provide function for generating AES term

Standardise data types and documentation

Requirements

Add todos.

File AESKeyDiscovery.hpp
Breaking AES
File Aldor.hpp
Install Aldor
File Algebra_Applications_RSA.cpp

Use messages.

Complete input checking.

File Algebra_Models.hpp

These classes should go into a number theory module.

Using a static member for the modulus in Zmodn is very crude.

File Algorithms.hpp
What are the right places for the code to move? We have
File AlgorithmSelection.hpp

Connections

Selecting the best algorithm

File AlgorithmSelection.hpp

Finding best UBCSAT algorithm for Ramsey problems

Understanding local search algorithms

File AllDifferent.hpp

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 order-comparable?)

Test InjectivityConstraints::TrivialAllDifferent<p>Move the relevant parts from InjectivityConstraints/plans/general.hpp to here.

Old implementations: Perhaps the following tests can be reused?

File AMO.hpp

AMO(L) (V is a set of boolean literals) as a (strong) active clause-set 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 clause-sets:

Likely the ALO-constraint ("at least one") on boolean variables is not worth considering on its own?

File AnalyseTotalAssignment.hpp

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 source-files 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

File Annotations.hpp

Style-files

Partially moving repository Annotations:

Latex macros

Bibtex-database

File AppendDimacs.cpp
Move CLSAdaptorAppend
File Argo.hpp

Overview

minisat-2.2.0

File Arithmetic.hpp

Addition

Subtraction

Multiplication

Division

File AssociativeBlockDesigns.hpp

Organisation

Generators for unsatisfiable uniform and variable-regular hitting clause-sets

Searching for ABD(n,k) (via SAT)

Rules for ABD(n,k)

Properties of ABDs

File Asymptotics.hpp

Connections

Estimating the factors in the infinite Grosswald-Hagis-product

DONE (providing proven intervals containing the true value) Controlling the error of C_gh_hp(k,max_p,decimal_digits)

Improving the Grosswald-Hagis estimation

File AtomicConditions.hpp

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:

  • eval(x, y) : boost::tribool.

Write semantic tests.

File ATP.hpp

ACL2

Prover 9

Maude

First-order theory of the reals

Vampire

File AutarkyMonoid.hpp
The autarky monoid
File Auxiliary.hpp

Floors of logarithms

Positional (polyadic) representations of numbers

ext_integer_partitions

Unordered integer partitions

File Auxiliary.hpp
Establishing meaning
File Axiom.hpp

Install Axiom

Install OpenAxiom

FriCAS

File Axiom.hpp

Naming conventions

Aldor integration

Test system

Documenting the code

Input checking

File BacktrackingProbing.hpp

Literature review : NEEDS UPDATE

Write first outlines

File Basic.hpp

DONE Naming conventions

Graph concepts

Subgraph concepts

File BasicDataStructure.hpp
Classes like this should be simple models of the general concepts.
File BasicFunctions.hpp

Naming conventions

DONE (Moved to ComputerAlgebra/Satisfiability/Lisp/Generators/plans/RandomClauseSets.hpp) Random boolean function

File BasicNotions.hpp

Notions and abbreviations for ringframes

Notions and abbreviations for modules and generalisations

File BasicNotions.hpp

The notion of a "latin square"

Properties of latin squares

Enumeration and classification

Counting

File BasicNotions.hpp

Connections

The notion of a biclique partition

Combinatorial matrices

Directed graphs

Abbreviations

File BasicNotions.hpp

The notion of a "biclique"

Abbreviations

Maximal biclique

File BasicNotions.hpp

Notions and notations

Partial groupoids, and extensions

Different forms of tests

File Basics.cpp
To be completed
File Basics.hpp

Complete the tests

Organisation

Basic notions

Conversions

Symmetric matrices

Duality and polarity

File Basics.hpp

Lists instead of sets

Naming conventions

Polar hypergraphs

File Basics.hpp

Notions of "finite functions"

Representing boolean functions by their truth tables

Algebraic normal form

DONE (we just use full clause-sets) Boolean functions represented by sets of satisfied/falsified inputs

File Basics.hpp

resolvable versus resolvable_p

Renewal

DP

resolution_closure_cs

min_resolution_closure_cs : DONE

File Basics.hpp

rt2lrt_il

Generating all binary trees

Catalan numbers

Random binary trees

File Basics.hpp

Test the archetypes etc.

Write FullyConstructibleLt.

Write FullyConstructibleLo.

Use OKlib::Concepts::convertible_to_bool.

Write semantical tests.

File Basics_Tests.hpp
  • There must be (at least basic) tests for the tests itself.
  • Complete update!
  • Updating tests for FullyLessThanComparable (similar to tests for EqualityComparable).
  • Updating tests for LinearOrder (similar to tests for EqualityComparable).
  • Besides "axiomatix tests" we need "sporadic tests" (with given outcome). A range of (non-empy) ranges is the input here, where in case of ==-testing the elements in the single ranges are ==, and elements from different ranges are (not ==), while in case of < elements of the single ranges are equivalent (i.e., incomparable), and we have < for immediately succeeding ranges. The idea here is, that the minimal checks for these assertions are done here, and then a sequence of all the objects is fed into the systematic test from the previous points (altogether this must then guarantee that all asserted relations hold; for a LinearOrder for example we only need to compare within a single range neighbouring elements for ==, and the first elements of immediately successive ranges for <). Thus, for example for testing of a model of FullyConstructibleLinearOrder, the user only needs to provide such a set of sporadic test cases, and all possible checks are carried out.
File BasicSetOperations.hpp

Organisation

Class SetAlgorithms::Disjoint

File BDDs.hpp

Connections

Basic operations for boolean functions

OBDDs

Smurfs

File Benchmarks.hpp

Links

Prepare benchmarks for SAT 2011

File BinaryAddition.hpp

Boolean functions representing binary addition

CNF and DNF representations of binary addition

Smallest prime CNF-representation

Smallest r_1-based CNF representation

Smallest r_2-based CNF representation

File BipartiteGraphs.hpp

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 undo-operations.

Literal-clause graphs and vertex-hyperede 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 clause-sets, 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 Hypergraphs-concepts (see Hypergraphs/concepts/plans/general.hpp).

File Boolean.hpp

Class BPass0

Computing the clashing variables in PassClashes

Partial assignment output adaptor

Adaptor ApplyPassAdaptor

DONE Application ApplyPass

Write application tests for ApplyPass

File BooleanFunctions.hpp

Random boolean functions

Random boolean functions in 10 variables with 64 true points

Random boolean functions in 16 variables with 256 true points

File BooleanFunctions.hpp

BDD's

Aiger

ABC

Translations to SAT

Boolean functions

Logic synthesis

Improve documentation for Espresso

File Boost.hpp

Some errors when building 1_52_0

DONE (updated path to bjam-sources) Update to version 1_48_0

Update Boost installation

Documentation

distance versus size

File BoostPathCorrected.hpp

What kind of range exactly?

Notifying the boost e-mail list about the missing functionality.

Should go to module GeneralInputOutput.

File Branching.hpp

Purely local branches

Problems with branch rijndael:

Tutorial on branching : DONE (basic principle are understood; needs to be transferred to the documentation-document)

On branching (in our situation) DONE (fixed a reasonable procedure; needs to be transferred to the general documentation))

File BranchingPrograms.hpp

Connections

The notion of "branching program" (BP)

Translations into (boolean circuits):

File Call_Maxima.hpp

Improve locality

Setting userdir

File CardinalityConstraints.hpp

Connections

Representing "cardinality constraints"

Direct realisations

Simplifications

Application of partial assignments

At-most-one as a CNF

Implement sequential counter by [Sinz 2005]

Allow repeating literals for unary_bb_crd2fcl

Improved understanding/implementation of BB-method

Add statistics functions

Docus

Implement adder-circuit 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.

File CardinalityConstraints.hpp

Upper bounds

Lower bounds

File CardinalityConstraints.mac
DONE The text below regarding unary encoding needs a complete update.
File CarenPanofsky2005.hpp

Create milestones

Data

Perform analysis using additional variables

File Certificates.hpp

DONE The notion of a "certificate"

Implementation certificate_vdw_p(L,n,P)

Conversions

Analysing certificates

File Certificates.hpp

Verification of r-resolution refutations:

Stronger proof systems:

File CheckBuildSystem.hpp

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

File Chess.hpp

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 chess-programming?

Generalised chess

Completeness of generalised chess

File Clauses.hpp

Connections

Boolean clauses, and more general clauses

Signed clauses as conditions

Sets of conditions? (Clause-sets as special cases?) Big And resp. big Or ?!

File ClauseSetAdaptors.hpp
Write concept for CLSAdaptor:
File ClauseSetAdaptors.hpp

Is usage of boost::distance effective?

Need "ReverseDimacs" application and clause-set 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"

File ClauseSetAdaptors.hpp

Write generic tests for the concept (in module Concepts).

Write test for InputOutput::CLSAdaptorStatistics

Write test for InputOutput::RawDimacsCLSAdaptor

Write test for InputOutput::Statistics.

File ClauseSets.hpp
Improve flcls2fcls
File ClauseSets.hpp

Update with

Shouldn't we differentiate between

  • "ClauseSets"
  • "VirtualClauseSets"
  • "ActiveClauseSets"

Concepts for clause-sets as collections of clauses, which are collections of literals, holding a reference to a domain-assignment for the variables.

For an earlier attempt see OKsolver/Experimental/AllgKlassen200203/ClauseSets.hpp.

An important refinement is the concept of a "clause-set with history", which holds a reference to a structure consisting of a domain-assignment 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. Clause-sets with history support the reversal of the assignment process (controlled by the assignment structure).

Actually clause-sets with history are only special cases of *virtual clause-sets*, 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 clause-sets refine virtual clause-sets by returning a partial assignment themselves (the set of unit-clauses which the inference mechanism found; "strong active clause-sets" infer all clauses of length <= 1). More generally for k-active clause-sets sequences of derived clauses of length at most k are computed (so virtual clause-sets are 0-active clause-sets).

Clause-sets 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 resolution-subsumption 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 clause-literal graph likely should be accessed through the hypergraph-interface. The two refinements "clause-sets with history" and "clause-sets with bipartite structure" should be independent of each other, and there should be a common refinement.

Clause-literal graphs for clause-sets should contain all possible literals; however for P-clause-sets 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 P-clause-set is a partial assignment, such that for P-clauses which are not satisfied by the assignment no literal exists with a restricted set of satisfying values.

A virtual clause-set 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 P-clause-set 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 P-clause-set can (immediately) deliver, but might be (much) stronger).

An aliance of active clause-sets 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 clause-sets 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 clause-sets". And in SATAlgorithms/plans/GenericBacktracking.hpp the first prototype is being developed.

Sat status: For an active clause-set F,

File ClausesWithRemoval.hpp

Make the above concept definition more precise.

Write concept-check and concept-prototypes.

File Closures.hpp

Write tests

Closures extended

File ClsAdaptorUCP.hpp

Connections

Move todos from UnitClausePropagation/ClsAdaptorUCP.hpp here.

File CLSIsomorphisms.hpp

Relations to other modules

Reduction to graph isomorphisms

We also need the determination of the automorphism group of a clause-set, either explicitely listing all elements or giving a more compact representation (using some group theory software).

Applications

File Colouring.hpp

Connections to other modules

Greedy colouring

File Colouring.hpp

Relations to other modules

Organisation

Translations to SAT problems

Colouring by transversals

Generalised colouring problems

Greedy colouring

Positional games

Achievement and avoidance game

File Colouring.hpp
Write tests.
File Colouring.hpp

Improve design

Improve implementations

Generic translation

File Combinatorics.hpp
Should be overhauled and transferred to OKlib/Combinatorics.
Class Combinatorics::Binom_integer_over_integer< Int >
It seems that in the implementation some further special cases could be treated?!
Member Combinatorics::choose_possibilities

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 iterator-based.

The implementation is not very efficient; improve it.

The design should be perhaps be iterator-based.

File Combinatorics_Tests.hpp

When transferring to OKlib:

  • Use the new test system.
  • Complete the tests.

With C++09 stdint.h likely is to be replaced by cstdint.

File CommonPart.hpp
How can we combine the const- and the non-const variant (avoiding copy-and-paste) ?
File Commutativity.hpp
Complexity of finding centralising elements
File Comparisons.hpp

Testing CommonPart

Documenting CommonPart

File Comparisons.hpp
How to get a kind of version number like CVS's?
File Complexity.hpp

Complexity measurements

Complexity functions in dependency on n

File ComputeAnalysis.cpp

Usage of ProgramOptions.

Classes PrintStandard and PrintLatex should inherit from some common base class.

File ComputeLexicographicalEvaluation.cpp

The output should contain a legend, and the date and time of the evaluation (and also the version-information of this program).

The common output facilities for ComputeScores and ComputeLexicographicalEvaluation should go into a separate sub-module (and then used in these two programs).

Using the new module ProgramOptions (together with Messages).

File ComputerAlgebra.hpp

General systems

Computational commutative algebra

Vicinity of computational group theory

Polyeders, matroids etc. PORTA and SMAPO at http://www.iwr.uni-heidelberg.de/iwr/comopt/soft Code for [Bokowski, Computational Oriented Matroids] at http://juergen.bokowski.de, and other software.

File ComputeScores.cpp

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.

File ConceptsMetafunctions.hpp

The file-documentation should contain some general explanations about the roles of the supplied metafunctions.

Transfer the tests to the new test-system.

Perhaps a metafunction computing the concept-tag-class from a concept class would be useful?

Should tr1/type_traits completely replace boost/type_traits.hpp?

File Conditions.hpp

Connections

0,1 versus false,true

Notions, names and abbreviations

snbl2cdn

File Consensus.hpp

Notions and notations

The basic "consensus" operation

Maximisation functions

The consensus iteration

Handling general graphs

Improving the implementations

Compute all maximal bicliques

File ConstraintSatisfaction.hpp

constraint_backtracking

Heuristics

Further propagators

File ConstraintTemplateRewriteSystem.hpp

General idea

Data types and concepts

Naming conventions

Example

File ConstraintTemplateRewriteSystem.hpp
Notion of "constraint"
File ConstraintTemplateSmallScaleRewriteRules.hpp

Move AES box translations into separate file

Update specifications

Remove hard-coding of multiplication by 01 in small-scale MixColumn

Rearranging linear components of Sbox and MixColumns

File Constructions.hpp

Write tests

Products

DONE Complex composition

File Constructions.hpp
Rabung's method
File Constructions.hpp

Representations of the basic logical operations

Gluing operations

File Coq.hpp

Improve Coq installation

Improve ocaml installation

File Cores.hpp

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

File CountingProgressions.hpp

Connections

The distribution of arithmetic progressions amongst primes

The Grosswald-Hagis-formula

Computing the Grosswald-Hagis coefficients C_k

Using curve-fitting

k=3

k=4

k=5

k=6

k=7

k=8

File CryptographicProperties.hpp

Create sub-module

Cryptographic properties of AES

Keys for which AES encrypts P to P

File Cryptography.hpp

Connections

Terminology

New library (replacing Mhash)

Grain of salt

Create documentation

Argo DES instances

Kreuzer DES instances

DES generator

File CSP.hpp

Overview

Constraint modelling languages

Sugar

Gecode

Minion

Mistral

Choco

Mozart

Eclipse

N Queens

Sudoku (only "big Sudoku", of arbitrary dimensions)

TAILOR

Local search

File DataAnalysis_MGOK1.hpp

General content

Title

Journal

Structure

Create milestones

File DataCollection.hpp

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 new-ubcsat-okl as an option for run_ubcsat

Make run_ubcsat interruptible

Parallelisation

File Datak10.hpp

Elementary statistics

Only computing the transversal numbers

File Datak10.hpp
Elementary statistics for k=10
File Datak11.hpp
Elementary statistics for k=11
File Datak12.hpp

Elementary statistics for k=12

Only computing the transversal numbers

File Datak13.hpp

Elementary statistics for k=13

Only computing the transversal numbers

File Datak14.hpp

Elementary statistics for k=14

Only computing the transversal numbers

File Datak15.hpp

Elementary statistics for k=15

Only computing the transversal numbers

File Datak16.hpp

Elementary statistics for k=16

Only computing the transversal numbers

File Datak17.hpp

Elementary statistics for k=17

Only computing the transversal numbers

File Datak18.hpp

Elementary statistics for k=18

Only computing the transversal numbers

File Datak19.hpp

Elementary statistics for k=19

Only computing the transversal numbers

File Datak20.hpp

Elementary statistics for k=20

Only computing the transversal numbers

File Datak21.hpp

Elementary statistics for k=21

Only computing the transversal numbers

File Datak22.hpp

Elementary statistics for k=22

Only computing the transversal numbers

File Datak3.hpp

Elementary statistics

Only computing the transversal numbers

Local search

File Datak3.hpp
Elementary statistics
File Datak3.hpp

Elementary statistics

Only computing the transversal numbers

Predictions

Local search

Detailed investigations of Tr(ap(3,n_0)) for small n_0

File Datak4.hpp

Elementary statistics

Only computing the transversal numbers

File Datak4.hpp

Elementary statistics for k=4

Predictions

File Datak5.hpp

Elementary statistics

Only computing the transversal numbers

File Datak5.hpp

Elementary statistics for k=5

Predictions

File Datak6.hpp

Elementary statistics

Only computing the transversal numbers

File Datak6.hpp
Elementary statistics for k=6
File Datak7.hpp

Elementary statistics

Only computing the transversal numbers

File Datak7.hpp
Elementary statistics for k=7
File Datak8.hpp

Elementary statistics

Only computing the transversal numbers

File Datak8.hpp
Elementary statistics for k=8
File Datak9.hpp

Elementary statistics

Only computing the transversal numbers

File Datak9.hpp
Elementary statistics for k=9
File Deficiency2.hpp
All hitting clause-sets
File DeficiencyOne.hpp

Decision algorithms

Tree representations

Pebbling contradictions

Small variable-degrees 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

File Demangling.hpp

Testing

Usage of demangle.h

Linkage

File demo_Example_12_1.cpp

The output-file should go somewhere in system_directories, like a sub-directory "data"; build-system 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 functor-class.)

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 sub-directory demos. Or to a sub-directory "examples" ? (It is not a demo for our library, but for another library?!)

File demo_read_graph.cpp

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 doxygen-output of structure "process" is complete nonsense.

File Dimacs.hpp

Complete the doxygen-documentation.

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 Dimacs-parser for clause-sets with non-boolean variables

Write Dimacs-parser for weighted (partial) MaxSAT formats

Write higher level modules

File DirectTransversalEnumeration.hpp

Concepts

Implementation

Connections

File DistributedSolving.hpp
Connections
File DLL_solvers.hpp

Organisation

Heuristics, distances etc.

Concepts for heuristics

File Domains.hpp

Write tests

Concept of a "domain association"

File DopedMUOne.hpp

Hardness of prime-extremal satisfiable general Horn clause-sets

3 different representations of HIT(1)

File Doxygen.hpp
Install version 1.7.2
File DP-Reductions.hpp
Singular DP-reduction
File DPv.hpp
Improved implementations (as models of general concepts) in a new module DavisPutnamReduction.
File Ecl.hpp

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

File EliminationSequences.hpp

GraphDecomposition::Treewidth_by_enumerating_elimination_sequences

GraphDecomposition::Width_elimination_sequence

Greedy strategy

File EmptyPuzzle.hpp

Box-dimension p=3 with direct encoding and three standard translations

Box-dimension p=4 with direct encoding and three standard translations

Box-dimension p=5 with direct encoding and three standard translations

Box-dimension p=6 with direct encoding and three standard translations

Direct encoding, weak-pl translation

Direct encoding, weak-pb translation

Direct encoding, dual-weak-pl translation

Direct encoding, dual-weak-pb translation

Summary

File EncryptionDecryption.hpp

Overview

Encryption

Decryption

Update instructions

File Enumeration.hpp

Connections

Complete the implementation

All isomorphism types of small groupoids

File Enumeration.hpp

Enumeration and classification

Random generation of quasigroups and unital quasigroups

File Enumeration.hpp
Basic implementations
File Enumeration.hpp

Trivial SAT algorithm

Improving the trivial algorithm

Variations

File Enumeration.hpp
Enumerating biclique partitions
File EvaluatePartialAssignments.hpp

Measures

Design

File Evaluation.hpp
Evaluation tools for run_ubcsat
File EvolutionaryProgramming.hpp

Frameworks for genetic algorithms

Applications

File ExactTransversals.hpp

The basic algorithm

Exact transversal hypergraphs (that is, Tr(G) = ETr(G))

Generalisation to boolean CNF

Exact covers

File Examples.hpp
Pigeonhole formulas:
File Exceptions.hpp

Base class

Exceptions module

A general standard for the messages of the exceptions is needed

File ExperimentalThreads_Tests.hpp

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.

File Experimentation.hpp

Links

Investigating dimensions

Open problems

Update experiment script

Move experiment data to investigation-reports

Solvers to be used for experimentation

DONE (individual issues moved to separate todos) Prepare experiments for the SAT 2012 paper

Class Extend_include_directives_Two_directories
Update the explanation.
File ExtendedDimacsFullStatistics.cpp
Sharing with InputOutput/ExtendedDimacsStatistics.cpp
File ExtendedDimacsStatistics.hpp

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

File ExtendedResolution.hpp

Sat solvers on xxtended PHP clause-sets

Hardness

Analysis of blocking structure

File ExtendedToStrictDimacs.hpp

Parameter handling

Extended Dimacs format

Permutations

Complete doxygen-documentation

Write docus

Use Messages

Use ProgramOptions

Organisation

File ExtendingHittingClauseSets.hpp

Write the following algorithm which systematically searches for an extension of an input hitting clause-set 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 non-isomorphic ones (that is, where the extended clause-sets are non-isomorphic) are considered, and then recursively the algorithm tries to extend the clause-set 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 clause-sets with constant clause-length k and 2^k clauses, which have as many variables as possible. Interesting also the structure of the extremal clause-sets (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 clause-sets 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 1-regular hitting clause-sets --- here not just satisfying assignments are sought, but "exactly satisfying assignments". See HypergraphTransversals/plans/ExactTransversals.hpp.

File ExternalSources.hpp

Links

Boost-documentation

GCC-documentation

Further documentation

File Factorisation.hpp

Literature review

Interesting good constraint representations

File FailedLiteralReduction.hpp
Connections
File FaronsPuzzle.hpp
See script for CS_342, week 05.
File FaronsPuzzle.hpp

Comments in output

Create doxygen-documentation.

Use an CLSAdaptor for output

Write docus

Test.cpp

Tools

Symmetries

Alternative translations

Generalisations

File FieldOperationsAnalysis.hpp

Add XOR translations for field multiplications

Move experimental todos to investigations

Generate good CNF hitting clause-sets for the AES Field Operations

Prime implicate representations from hitting-cls-representations

Find the symmetries of the AES Field Operations

Determine *all* prime implicates (for the purpose of analysis)

File FileIdentification.hpp

Test class FileIdentification.

Provide other languages with FileIdentification.

File FilterDimacs.cpp

Add application tests

Weak implementation

Move CLSAdaptorFilter

File FiniteFields.hpp

Move to Ringframes/Fields.

Write tests for all functions provided

Complete docus

Demos

Maxima bugs

Missing functionality

File Formulas.hpp

Replacement of "makelist" by "create_list"

Basic concepts

Using Maxima expressions

File Foundations.hpp
Improve the general design discussions : DONE
File FreeWillConfiguration.hpp

Detailed examination of Peres33PointConfiguration.cnf

Testing realisability

Minimal configuration

File FundamentalADTs.hpp

Collaborating modules

Variables

Literals

Clauses

File Games.hpp
Parity games
File GAP.hpp
Improve installation
File Gasarch.hpp
Completition
File Gcc.hpp

Problems building 4.6.4

Incorrect .texi-files

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

Loop-optimisation

DONE (gcc-building 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

File general.hpp

Connections

Update namespaces.

Update milestones.

Update todos.

Whatever remains of module DPv shall move here

The basic problems

Write docus

A Resolvent-class

File general.hpp

Relations to other modules

A general framework

Examing search landscapes

Theoretical random walk algorithms

File general.hpp

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.

File general.hpp
Systematising output functionality
File general.hpp

Connections

The notion of a "linear constraint"

File general.hpp

Connections

Create milestones

Generalising positional games to SAT

File general.hpp

Create milestones

Connections to other modules

General plans

Quadratic functions

Horn functions

Finite functions with full application of partial assignments

And-inverter graphs (AIGs)

File formats

File general.hpp

Relations to other modules

Update plans:

Redesign

MaxSAT, weighted MaxSAT, and partial MaxSAT

Clause-lists instead of clause-sets

Better general naming conventions

Develop combinations of look-ahead with conflict-driven solvers

Proof systems

Finding out "all properties" of an instance

Survey and belief propagation

Converting CNFs to DNFs

File general.hpp

Organisation

Notions

Connections / Relations

Create milestones.

Extract the methods related to splitting trees

Shortest dual representations

Computations of all prime clauses for full clause-sets

File general.hpp

The notion of a "pseudo-boolean constraint"

Application of partial assignments

Pseudo-boolean constraints as active clauses

Add milestones

File general.hpp

Create milestones

Create tests

Connections to other modules

Overview on generators for MUSAT

File general.hpp

Create milestones.

Simplifications

File general.hpp

Create milestones

Connections to other modules

Basic concepts

Basic backtracking algorithms

Representing solutions by finite functions

Generators

Perhaps only considering the simplest case

File general.hpp

Write tests

Write docus

Bounded resolution

Create milestones : DONE

File general.hpp

Create milestones

Organisation

Relations to other modules

Notions for symmetries

Brute-force algorithms

Reduction to graph isomorphisms

is_isomorphic_btr_cs

Exploring symmetries

Homomorphisms

File general.hpp
Create a development plan
File general.hpp

How to calibrate floating-point efficiency

Create milestones.

DONE Improving assert

Outline of the test system

Testing the demos

Improving the test system

Handling floating and bigfloating numbers

File general.hpp

Create milestones

Write tests

Write docus

Relations to other modules

SAT translations

File general.hpp

Create milestones.

Reorganisation

Concepts and abbreviations

Tree drawing (output as Latex code)

Graph drawing (output as Latex code)

File general.hpp

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:

  • atomic conditions
  • literals
  • partial assignments
  • active clause-sets
  • clauses and clause-sets.

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:

File general.hpp

Update namespaces

Update namespace-usage

General update

New test system

File general.hpp

Update namespaces.

Concept design "Rooted trees with ordered children"

In a module GraphTrees rooted trees as Boost-graphs with one distinguished vertex establishing, while Parent-graph-trees additionally are equipped for every vertex with a property yielding the parent vertex (which in case of the root is the root itself).

File general.hpp
AES Challenge
File general.hpp

Connections

Functions should not cache return values

Generating defaults constant for small scale

Generating polynomial representations of field operations

S-box and multiplication boolean 6xm functions

Translating the constraint-system into SAT, CSP, ...

Evaluating AES "constraints"

Rewrite translation functions using ss_field_op_fulldnf_gen_fcl etc

File general.hpp

Update namespaces

Update

Concepts

SET ("SAT Evaluation Toolkit")

New tests Transfer to the new test system

Messages Use Messages.

File general.hpp

Iteration

Connections

Basic overview

File general.hpp

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).

MO-FAP: (G, D, c, T, K)

  • for vertex v in V(G) with requested number c(v) of frequencies and set D(v) <= NN_0 of possible frequencies we have variables v_1, ..., v_{c(v)}, each with domain D(v), and the constraint INJ({v_1, ..., v_{c(v)}}) (see module InjectivityConstraints);
  • for every edge {u,v} in E(G) we have an active constraint forbidding the differences in T({u,v}) (it seems questionable to me whether the compression enabled by T is worth to pursue, or whether we better consider the more general constraint, which allows to forbid specific pairs of frequencies (then perhaps we should gather all these constraints in a ("real") clause-set); if T just demands, that the distance is at least a certain threshold t, then T might be worth its own active clause-set (and other systematic situations are conceivable), if T however is just "random", then perhaps it's not worth a special active clause-set);
  • for all variables together (gathered in set VA) we have the upper bound constraint UPPER_V(VA, K) (see module LinearInequalities).

MS-FAP: We MO-FAP, but the third condition (the constraint on K) is replaced by:

  • maximal value for v in VA - minimal value for v in VA <= K.

Are there competitions on the subject? (We look only at the decision side; likely most activities in this field concentrate on optimisation?!)

File general.hpp
Overview
File general.hpp

General databases

Documentation

make

Other files

File general.hpp
Meta heuristics
File general.hpp

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 experiment-system

Launching and monitoring

Tests

File general.hpp

Handling changing solver output

Testing solver extraction scripts

Running experiments

Better summary statistics

Extraction tools

Add monitoring for all other solvers

File general.hpp

Connections

Minimum CNF/DNF representations

File general.hpp

Connections

Hardness of boolean function representations

Propagation hardness of 2-CNF

Hardness of canonical translation of positive DNF

Hardness of Sudoku problems

File general.hpp

Update namespace

Write milestones

Travelling salesman problem

File general.hpp

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

File general.hpp

Links

Satisfiability of products

File general.hpp

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

File general.hpp

Update namespaces

DES

RSA

MD4, MD5

File general.hpp

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 key-schedule and block-cipher

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"

File general.hpp

Connections

Graph colouring benchmarks

Searching for small hard planar graphs

File general.hpp

Update namespace.

Create milestones.

Literature review

Organisation

Different perspectives:

Different formulations

Active clause-sets for the moves-condition

The challenge of counting

File general.hpp

Problem specification

Overview

Remove linear diffusion from translation

Translations

Minisat-2.2.0

precosat236

precosat-570.1

OKsolver_2002

march_pl

satz

File general.hpp

Problem specification

Overview

Translations

Minisat-2.2.0

precosat236

OKsolver_2002

march_pl

satz

File general.hpp

Update namespace.

Create milestones.

Empirical study

Alternative formulations

Special algorithms

Generalisation for arbitrary graphs

File general.hpp

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 clause-sets:

  • injectivity (bijectivity) for v_1, ..., v_n
  • v_i, v_{i+1} must get adjacent vertices in G (if considering Hamiltonian cycles, then this wraps around); call this active clause-set the adjacency constraint.

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 clause-sets 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 clause-sets 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 non-Hamiltonian 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

File general.hpp

Problem specification

Translations

Minisat-2.2.0

File general.hpp

Overview

Problem specification

Translations

Minisat-2.2.0

The 1-base box translation

The "minimum" box translation

File general.hpp

Problem specification

Instance characteristics

Translations

Analysing the data

Comparison of run-times for the three translations

Minisat-2.2.0

File general.hpp

Problem specification

Overview

Translations

Minisat-2.2.0

File general.hpp

Update namespaces.

Create milestones.

Update namespace usage.

File general.hpp

Connections

Update namespaces.

Create milestones.

What other games are interesting?

"Problem solver"

Tools for translations

File general.hpp

Problem specification

Overview

Translations

Minisat-2.2.0

File general.hpp

Overview

Problem specification

The canonical box translation (bidirectional MixColumns)

The canonical box translation (forward MixColumns)

The 1-base box translation (bi-directional Mixcolumns)

The 1-base box translation (forward Mixcolumns)

The "minimum" box translation (bidirectional MixColumns)

The "minimum" box translation (forward MixColumns)

File general.hpp

Problem specification

Translations

Minisat-2.2.0

Glucose-2.0

File general.hpp

Problem specification

Overview

Translations

Minisat-2.2.0

File general.hpp

Update namespaces.

Update milestones.

Update the following todos.

Review: Software and literature review.

Connections to other modules

Basic direct algorithms

Active clause-sets

Completing partial latin squares

Strong hypergraph colouring

MOLS

Sizes

N(n)

Experiments

Pairs of orthogonal latin squares

The upper bounds for N(k)

File general.hpp

Problem specification

Translations

Minisat-2.2.0

File general.hpp
Problem specification
File general.hpp

Introduce namespace-alias.

First the distinction between this part and part Satisfiability has to be cleared:

Create milestones

File general.hpp
Problem specification
File general.hpp
Problem specification
File general.hpp
Problem specification
File general.hpp
Problem specification
File general.hpp

Update namespaces and their usage

Connections

File general.hpp

Transformations

The natural operation of N

Semilattices

File general.hpp
Problem specification
File general.hpp
Quantum simulation
File general.hpp

Show and explain sizes of minimum-translations

Patterns

Explanations

Naming of translations

Links

Boundaries

Fast generation of AES translations

File general.hpp

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

File general.hpp

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

k-based representations

The square of the Sbox

Understanding prime implicates after any partial assignment

File general.hpp

Understanding DES

Generating satisfying DES assignments

DES benchmarks

Basic translation

Encryption and decryption

r_2-bases of a round

Understanding the Massacci-Marraro translation

More advanced treatments

File general.hpp

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

File general.hpp

Overview

Number of solutions for DES key discovery

Experiment scripts

Add information on specific S-box translations to experiment instances

DONE Move into separate sub-module

File general.hpp

Links

Analysing the S-boxes

Analysing the 6-to-1 bit Sbox functions

File general.hpp

Overview

Analysing the KeeLoq round function

File general.hpp

Comparing translations and solvers

Translating stream ciphers using our translations

Create milestones.

File general.hpp

Complete documentation

Patches

Enable local/global installation for all packages

Organisation of links

Installation of C/C++ tools

Supporting Java

Combinatorics

SAT-applications in evolutionary biology

Matrix libraries

Logic programming

Other sources:

Suspending running processes

File general.hpp

Counting groupoids

Classifying groupoids

Counting semigroups

Classifying semigroups

Counting quasigroups and latin squares

Classifying quasigroups and latin squares

File general.hpp

Strictly pandiagonal latin squares

Counting the number of n-jective relations

Isomorphismen

File general.hpp

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

File general.hpp

Further links on the Internet-page

Domain name

File general.hpp

Connections

Translations to boolean CNFs based on the direct encoding

Finding hard instances for box-dimension 3

Finding hard instances for box-dimension >3

Tools for investigations with concrete Sudoku instances

File general.hpp

Create milestones.

Computing the probability of a "contradictory input matrix"

File general.hpp

Checking all links

Doxygen problems regarding stability of links

Better general documentation

File general.hpp

Connections

Hitting proof systems

Understanding the recursion for non-Mersenne numbers

Understanding S_2(k)

Maximal number of MUS's of a clause-set

File general.hpp

Prime implicates

Applying partial assignments

MU structure

File general.hpp

Update of pulling and pushing facilities

Markers instead of links

Improved makefiles

Further enhancements

Add file template generation option

File general.hpp

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.

File general.hpp

Structure

Rerun time-sensitive experiments WHAT IS THE STATUS OF THIS?

Experiment scripts

Sat-probability-approximations

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 clause-sets

Order principles

File general.hpp
Connections
File general.hpp

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

File general.hpp

Prepare benchmarks for SAT 2011

Standardisation on notation : DONE

Trivial Green-Tao 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

File general.hpp

No "useful" programs!

Using the right tools (nearly) from the beginning!

Anticipated parts

File general.hpp

Update namespace.

Create milestones.

File general.hpp
Create milestones : DONE
File general.hpp

Basic considerations

Investigating greentao_2(2,k)

File general.hpp

Connections

Generation

Only products

The case k=1

hindman_2(2) = 39

hindman_3(2) > 80000

hindmani_2(2) = 252

File general.hpp

Create milestones.

Connections

Hales-Jewett problems

File general.hpp

Connections

Density versions

File general.hpp

Link checking

General rules for html-pages

Install configuration system

Search engines

Handling of paths

Creating styles

File general.hpp

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

File general.hpp

Connections to other parts

Simple Unix/Linux tools

Investigating existing tools for parsing and refactoring code

Update namespaces.

Update namespace-usage.

Update the doxygen-documentation, and create further plans(-files).

Move Concepts/RefactoringIncludeHandling.hpp here.

Transfer the tests to the new test system.

File general.hpp

Connections

Organisation of the module

Literature exploration

Duality

Compare with the SAT-generalisation

File general.hpp

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

Self-dual solutions

"Visualising" solutions

Statistics functions are needed to analyse counter examples

Better SAT solvers

File general.hpp

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)

File general.hpp

Overview

What is known

Main research questions

Enumerating all solutions

Palindromic problems

Modular form of Schur numbers

File general.hpp

Overview

Estimation of run times for direct encoding

OKsolver_2002 for direct encoding

pdschur(5)

Forbidden elements for palindromic problems

pdwschur(5)

wmschur(5)

File general.hpp

Overview

Statistics

Certificates

File general.hpp

Create milestones

Write tests

Write docus

"Theoretical algorithms"

File general.hpp

Evaluation mode for oklib

Making make-variables compatible with shell-variables:

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

File general.hpp

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

File general.hpp
Local search
File general.hpp

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 git-repositories by users) Plans-structure review: The plans-structure in Buildsystem/ReleaseProcess/plans/ needs review.

"Prerequisites" for further development

File general.hpp

Connections

Predictions of vdw_2(3,k)

Analysing certificates

SAT 2011 competition

Local search for the satisfiable instances

Predictions of pdvdw_2(3,k)

File general.hpp

Literature overview

Why so hard?

Performance of OKsolver-2002

Performance of satz215

Performance of march_pl

Performance of minisat

Performance of picosat

Precosat

Glucose

CryptoMiniSat, Grasp

Palindromic numbers for k <= 8

File general.hpp

Literature overview

Best complete solver for vdw_2(5,k)

Best complete solver for palindromic problems

Best local-search solver for palindromic problems

File general.hpp

Update namespaces

Update namespace-usage

Transfer the todos

Update the doxygen-documentation.

Switch to the new test system

Move the iterated-related concepts from module Concepts here.

File general.hpp

Literature overview

Best complete solver for palindromic problems

Best local-search solver for palindromic problems

File general.hpp

Update namespaces.

Create a development plan and milestones.

See module ComputerAlgebra/Enumeration.

File general.hpp

Literature overview

Best complete solver for palindromic problems

Best local-search solver for palindromic problems

File general.hpp

Update namespaces.

Relations:

File general.hpp

Connections

Prepare benchmarks for SAT 2011

Create milestones

DONE (as stated) Organisation

Boolean van der Waerden numbers

Translations for non-boolean problems

Palindromic diagonal problems

Symmetry breaking for van der Waerden numbers

Palindromic versions

Overview on performance of SAT solvers

Lower bounds

File general.hpp

Best practices

Clean-up 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) Notification-e-mails

Remote access

Tagging

More advanced usage:

Combining different repositories

Change dates and revision numbers

Exploring usage patterns

Space usage:

File general.hpp

Concepts

Investigate whether there is something usable in the following old files:

Collect

Input/Output

Update namespaces.

File general.hpp

Connections

Plingeling

Cryptominisat

Parallelisation via OKsolver-2002

Parallel Satz

Using Open MPI

Update Data

Verify vdw_2(4,9) = 309 (conjectured)

Verify vdw_2(5,7) = 260 (conjectured)

File general.hpp

Naming the transversal hypergraph of arithprog_hg(k,n)

Relations to vanderwaerden_m(k_1, ..., k_m)

Studying the transversal hypergraph

Exploiting "self-similarity"

File general.hpp
Reduction to the hypergraph transversal problem
File general.hpp

Connections

Experimentation tools

Saturated Horn clause-sets

Saturated minimally unsatisfiable clause-sets of deficiency 2

Further test-cases

File general.hpp
Connections
File general.hpp

Update namespaces.

Relations

File general.hpp
Create links to whatever related already exists in the library.
File general.hpp

Connections

Overview

File general.hpp

Connections

Exact transversals of hypergraphs of partitions

File general.hpp
Create milestones.
File general.hpp

Scope of the catalogue

Connections

Integer sequences of interest

Deficiency = 3, n = 5

Primes

File general.hpp
Splitting trees.
File general.hpp

Update namespace-usage.

Module structure

Translations

Other implementations

Active clause-sets

Investigate the problem of determining the chromatic number:

Property B

Square hypergraphs

File general.hpp

Update namespaces.

Discussion

File general.hpp

Update namespaces.

Relations

File general.hpp

Update namespaces.

The general framework

General plans on evaluating solvers, algorithms, heuristics

File general.hpp

Update namespaces.

Create milestones.

Graphs/Isomorphisms/SimpleBacktracking.cpp

File general.hpp

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 cvs-logs 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).

File general.hpp

Update namespaces.

Basic revision

Improvements

Other tools

File general.hpp

Update namespaces.

Create milestones.

First we need some system installed under ExternalSources.

Relations

File general.hpp

Update namespaces.

Relations

File general.hpp

Create milestones.

Using Prover9

Notations

Proving distributivity of union and intersection

Updating and extending axioms.bel

File general.hpp

Create milestones.

Plans

File general.hpp

Update namespaces.

Scope discussion

File general.hpp

Update namespaces.

Module Computability

NP-completeness

NP-completeness 2

File general.hpp

Update the namespaces : DONE

All sub-modules have milestones.

Clarify the relations

Update namespace usage.

Graph generators

Graph operations

Organisation

File general.hpp

Update namespaces.

Create milestones.

Circuits

What else?

File general.hpp

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.

File general.hpp

Update namespaces.

Relations: We need to establish links to other modules.

File general.hpp
Overview on fundamental tasks
File general.hpp

Connections

Create milestones

File general.hpp

Update namespaces.

Relations:

Which systems?

Usage discussion

File general.hpp
Submodule "Experimental 200203"
File general.hpp

Update namespaces.

Create milestones.

Generic algorithm

File general.hpp

Special actions July/August 2011 (MG, OK)

"OKlib" instead of "Transitional" : DONE

Super-modules:

Handling of version-numbers : DONE

Research sub-modules : DONE

Organisation of plans-directories

Access to version numbers

Demos

Backups and archives

Upgrade the C++ code to gcc-4.5.3

Promoting the OKlibrary

File general.hpp

Ranking

Estimated time needed

File general.hpp

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

File general.hpp

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 ("value-based"): For every (new) message a class has to be written in an appropriate file in a meesage-subdirectory.

File general.hpp

Compiler options for Programming/InputOutput/PathDifference.cpp

Update namespaces

Update namespace-usage

Complete doxygen-documentation

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

File general.hpp

Update namespaces.

Create milestones.

Relations

File general.hpp

Update namespaces. DONE

Input and output

File general.hpp

Update namespaces

Update namespace-usage

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

File general.hpp

Update namespace

Update namespace usage.

Identification services: We need further classes (and macros) for identification purposes:

Warning and error messages

Error handling

Testing

Umlaute

File general.hpp

Update namespaces

Update namespace usage

Update the doxygen documentation

Update plans

Transfer tests to the new test system

File general.hpp

Update namespace-usage.

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.

File general.hpp

Update namespaces

Update namespace-usage

Update the doxygen-documentation 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?)

File general.hpp
Create a milestones file (once there is enough substance).
File general.hpp

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 generalised-SAT algorithms

Overview on more sophisticated algorithms

File general.hpp

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

File general.hpp

Update namespaces.

Relations

File general.hpp

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?

File general.hpp

Update namespace.

Update milestones.

Write docus.

File general.hpp
Combinatorial matrices
File general.hpp

Create milestones

Iterators and ranges

File general.hpp

Connections

Notions and notations

Homomorphisms

File general.hpp

Cleaning up

Future plans

Update namespaces

Update namespace-usage

Create milestones.

File general.hpp

Update namespaces : DONE

Update namespace usage

Write doxygen documentation

Write docus

Write demos.

Write tests (in the new system).

String comparison

File general.hpp

Orbits and stabilisers

Centralisers

File general.hpp

Update namespace : DONE

Write milestones

File general.hpp

Update namespaces.

Write milestones.

First prototype

File general.hpp

Create milestones

Connections to other modules

Overview on implementations

The lexicographical canonical numbering

File general.hpp

Connections to other modules

Conversions

Associativity resp. group test

File general.hpp

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?

File general.hpp

Connections to other modules

Algorithms for the matching lean kernel

Finding matching autarkies

Implementation

Applications

Incremental

File general.hpp

Connections to other modules

Lean kernel

File general.hpp

Update namespace usage.

Link to ComputerAlgebra/Satisfiability/Lisp/Autarkies/plans/general.hpp

File general.hpp

Write tests

Naming conventions

Forms of "constructive" groupoids

Straight-line programs

Congruence relations

File general.hpp

Update namespaces.

Connections to other modules

File general.hpp

Update namespace usage.

Concepts

New milestones

Move the content of OKlib/SATAlgorithms here : DONE

Update namespaces : DONE

File general.hpp

Connections

Notions and notations

File general.hpp

Update namespaces.

Create milestones

Considering the following graphs for clause-set F with clauses as vertices, where clauses C, D in F, C != F, are joined iff

  • var(C) intersection var(D) not empty (the common-variable graph cvg(F))
  • C and D clash in at least one literal (the conflict-graph cg(F))
  • C and D are resolvable (the resolution graph rg(F))
  • C and D are resolvable and the resolvent is not subsumed in F (the resolution-subsumption graph rsg(F)).

Considering the following graphs for clause-set F with variables as vertices, where variables v, w in var(F), v != w, are joined iff

  • there is C in F with v, w in var(C) (the variable-interaction graph vig(F)).

Given a clause-set with bipartite structure, "construct" the above graphs as "virtual graphs" in the Boost-sense. Algorithms needed for graphs:

  • Determination of the connected components (available with Boost::graph)
  • Computation of all articulation vertices (available with Boost::graph (see biconnected components))
  • Computation and Approximations of the treewidth (see module TreeDecomposition).

Statistics for benchmark formulas :

  • for each connected component : + n, c, for each clause-length k the number c_k + number of accumulation vertices + treewidth (approximations).
  • Perhaps monitoring, how especially successful algorithms behave regarding decomposition (perhaps they split "intuitively" the graphs ?!).
  • Perhaps exploring whether by branching a decomposition can be reached.

Possible heuristics exploiting decompositions:

  • Opportunistic heuristics: Together with any "standard" heuristics, just exploiting a decomposing graph (or when articulation points exist).
  • Replacing the "standard" heuristic by minimisation of some treewidth-approximation (which is used as complexity measure).

Classical tree decomposition algorithms and improvements

File general.hpp

Develop the ideas

Framework

Semantical trees

A very attractive form of learning is "r_k-compressed learning"

Afterburner

Re-working 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

File general.hpp

Two general forms of preprocessing

Preprocessing by reduction

Preprocessing by local compilation

Preprocess a clause-set by local dualisation

Finding and exploiting functional dependencies

File general.hpp

Abstract representation of structures

Modules

DONE (see above) Semirings, rings, fields

DONE Module UniversalAlgebra

DONE Modular arithmetic

DONE Actions and operations

File general.hpp

Relations to other modules

Create further milestones (for 0.0.7)

Framework for the analysis of search space structures

File general.hpp

Using Ubcsat as a library

Installation of UBCSAT completed

Contact the developers of Ubcsat

File general.hpp

Update namespaces

Connections

Different levels of generalisation:

Concepts

File general.hpp
The basic concept of a "total assignment"
File general.hpp

Organisation

Write tests

Homomorphisms

Module "Operations"

File general.hpp

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 clause-sets

Relation to the notion of clauses

File general.hpp

Update namespace usage.

Old implementations

Evaluation

Design study for evaluation

File general.hpp
Naming
File general.hpp

Clause-based approach

Connections

First-order theory of the reals

File general.hpp
Create milestones
File general.hpp

Links to other modules

Planning

CLS(n)

CLS(n, c)

CLS(n, c, k)

File general.hpp

Rename applications

Links and plans

Prime implicants and implicates

Minimisation

BDDs

File general.hpp

Connections

Basic notions

Abbreviations

Concrete categories

Functors

Natural transformations

File general.hpp

Connections to other modules

Other tools

Basic notions

Basic examples

File general.hpp

Create further milestones

Using different algorithms for different parameter values

File general.hpp
Incorporate the theory from OK's SAT-Handbook-article: planning
File general.hpp

Relations to other modules

Organisation

File general.hpp

Update the module according to OK's SAT-Handbook article

What are the relations to module "Projections"

Update namespaces : DONE

Move OKlib/Statistics/plans/TimeSeriesAnalysis.hpp to here : DONE

File general.hpp

Create milestones

Connections

Adding distribution power to SplittingViaOKsolver

Organising distributed solving

Sampling tool

Distribution via splitting trees

File general.hpp
Create milestones
File general.hpp

Tests for error cases in scripts

Update output for application tests

Strange tool statistics_add_missing_clause_lengths.awk

Comprehensive statistics

Elementary file-surgery

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

File general.hpp
Ladder logic
File general.hpp

Convenience functions

Variable ordering and standardisation

S-box boolean 6xm functions

Add variants with reduced number of rounds

Improve tests

Create constraint evaluation system

Triple-DES

Links

Translating the constraint-system into SAT, CSP, ...

DONE (see des_sbox_bit_fulldnf_cl) Add 6-to-1 bit Sbox functions

File general.hpp

Update namespaces.

Improve minimisation scripts

Computing all minimum transversals one by one

Create module MinOnes (or "WeightedSAT" ?)

Create module MinSAT.

Create module MaxSat.

File general.hpp

New supermodule on autarkies

New supermodule on CSP

File general.hpp
General idea
File general.hpp

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 complexity-measure for an injectivity constraint is the sum of the logarithms of the domain sizes of the variables involved. Also the measures for the simulating clause-sets (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 CNF-representation.

Extraction: We should also investigate how to extract injectivity constraints (from ordinary clause-sets for example, and in general from active clause-sets).

For variables v, v' not only " v <> v' " is needed, but more general " f(v) <> f(v') " for some function f.

File general.hpp
General structure
File general.hpp

Update namespaces. DONE

Create milestones.

File general.hpp

Update namespaces.

Given a boolean clause-set, 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^{k-1}, 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^{k-1}. Stronger approaches find also "hidden equivalences".

Then we need an active clause-set 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 clause-sets? It seems most natural not to do anything special here, but just let the active clause-set 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 clause-sets their complexity measurements.

How to generalise the concept of equivalences to non-boolean variables? Systems of equations over ZZ_m ? More general handling of system of equations of fields ? Rings ??!

File general.hpp

Connections

Implement WP (warning propagation)

Implement BP (belief propagation)

Implement SP (survey propgation)

File general.hpp

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.

File general.hpp

Update namespaces.

Create milestones.

First the scope (the (informal) concept) has to be established, and the relation to module LinearInequalities.

File general.hpp

Update

Standardising variable names

Sudoku

Biclique-transformations

MUSAT

Matching formulas

Generators for finding incidence structures and designs

Extended resolution

From non-boolean clause-sets

Pebbling formulas

Implement the general construction of Soeren Riis (especially interesting when we know that the formulas have short refutations).

File general.hpp

Other SAT-related attacks

Decryption using iterative block ciphers

Other cryptosystems

File general.hpp

Update namespaces: DONE

Create milestones

Connections

Organisation

Updates

Head-tail clauses

File general.hpp

Connections

General ideas

DONE (we have now Clauses::RClausesAsVectors and Clauses::RClausesAsSets) Clauses for unit-clause propagation

Partial assignments

File general.hpp

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.

File general.hpp

Move concepts from OKlib/Concepts here.

Update code w.r.t. new namespaces.

Further trivial atomic conditions

First prototype of general atomic condition

File general.hpp

Improve key schedule tests

Specification

Add variants with reduced number of rounds

Find more test vectors

Notion of DES round

Links

Triple-DES

File general.hpp

Tidy todos and update milestones

Improving tests

natl vs nat_l

Notions and notations

Modularising the Rijndael-implementation

Docus and Demos

Coding Standards

File general.hpp

Design conditions more general than "atomic conditions"

Integration with computer algebra

File general.hpp

Move the related concepts and plans from OKlib/Concepts here.

Boolean literals

File general.hpp

Good definition

Add todos

Create milestones

File general.hpp

Update namespace-usage

Prototypes

Write tests

File general.hpp

Update namespaces. DONE

Create milestones. DONE

All existing components related to problem instances are moved here. DONE (handled already by another todo)

All sub-modules have milestones.

Create a docus page with an overview on the concepts and ideas.

Integration with computer algebra.

File general.hpp

Move the related concepts and plans from OKlib/Concepts here.

Update namespace-usage.

Prototypes

Update

Old implementations

New test system

File general.hpp
Further development
File general.hpp

Conversion functions

New structure DONE

Create milestones. DONE

File general.hpp

DONE Update namespaces.

Create further milestones

Stronger propositional proof systems than resolution

Systems related to extended resolution

File general.hpp

Restructuring

See Applications/Cryptanalysis/plans/general.hpp

Write a general docus-file

File general.hpp

Create milestones

DONE Move the helper-functions from Cryptology here.

File general.hpp

Create milestones.

Main challenge are the concepts.

What are the input formats?

Applications

Basic autarkies

Bounded maximal deficiency

File general.hpp

Add application tests for RandomUcpBases

Connections

The notion of r-bases

r_0-base

Docus for RUcpGen

File general.hpp

Basic notions

More general notions

File general.hpp

First simple implementation

Transferring the implementation used in OKsolver_2002

Timestamp

Avoiding repetition

Local learning

Interface

Graph representation

Responsibility

2-clauses

There is the recurrent theme of "local vs. global"

Double look-ahead

File general.hpp

DONE Update namespaces.

Connections

Create milestones.

File general.hpp

DONE Update namespaces.

Preprocessing wrappers

File general.hpp

DONE Update namespaces.

Update namespace usage

Connections

Update the plans.

Create milestones.

Implement trivial unit-propagation (quadratic time)

Implement generic standard linear-time algorithm for boolean clause-sets

Implement initial UCP based on head-tail clauses

Implementing the standard linear-time UCP-algorithm (based on the bipartite structure) for Power-clause-sets.

Investigate how to specialise the general UCP-algorithm for clause-sets and boolean clause-sets.

The basic algorithm should assume an "active clause-set" and an "active partial assignment"

A clause-set F can be constructed with a binding to a partial assignment F.phi().

Regarding unit-clause-propagation for an alliance of active clause-sets

UCP for clause-sets 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)

File general.hpp

Connections

Document options

Control verbosity of output

Output of learned clauses

Output all information when aborted by SIGINT

Correcting include-directives

Usage as library

File general.hpp

Update namespaces.

Create milestones.

Trivial DLL-solver "DLL-Implementations"

File general.hpp

Directed graphs

Maximum bicliques

File general.hpp
Update todos
File general.hpp
Use the local Gmp : DONE
File general.hpp

Translations to clause-sets

The conjecture of [Galesi, Kullmann]

NP-completeness of determining bcp

File general.hpp

Create milestones

Newer versions

Links

Output learned clauses

DONE Improve patches

File general.hpp

Update namespaces.

How to refer to the different versions of OKsolver ?

Combination of OKsolver with Minisat

File general.hpp

Concepts

Exactly one common neighbour

File general.hpp

More information on the current path

Splitting-output in iCNF format

Differences

Improve the Dimacs-output

Introduce error-codes

Output to files

OUTPUTTREEDATAXML

Documentation problems

Language standards

Buildsystem (replacing Buildtools/UebersetzungOKs.plx)

Complete the help facilities of the OKsolver

Write docus-pages

Add doxygen-documentation

Eliminate old history in code.

Create systematic application tests

Add asserts throughout

Investigate unit-testing

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 const-qualification

Use restrict-qualification

Elimination of compile-time options

Output of clause-sets

Inefficiency on 64-bit platforms

Extend statistics

Output intermediate results

More influence on heuristics

Improving the implementation

Start planning on evaluating and optimising heuristics

Apply time-measurements

Optimising the code

Why so slow on easy instances?

Extension by cardinality constraints

Improved Delta(n)-distance

Enable finding all solutions

File general.hpp

External solvers

Special solvers

DONE Update namespaces.

File general.hpp

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

File general.hpp

Improve file output

Correct memory handling

Use signals as with OKsolver_2002

Provide application tests

Update to C99

Add Doxygen documentation

File general.hpp

Create milestones

Provide information

Timing

Using the tau-function

Handle signals : DONE

Provide Doxygen documentation

Introduce macros : DONE

DONE Check number of variables and clauses

Version information : DONE

Improving the clause-bitsets

Optimising weights

File general.hpp

Concepts

Isomorphism testing

Spanning trees

File general.hpp

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 clause-set.

Likely, in this module also multi-hitting clause-sets should be considered (with non-boolean variables).

File general.hpp

Update namespaces.

Create milestones.

Generator-plans mentioned elsewhere and relevant here should move to here.

SNS-matrices, Pfaffian graphs etc. (possibly this should go to its own module on combinatorial autarkies?)

File general.hpp

Connections

Organisation

Statistics

Sudoku

File general.hpp
Update namespaces.
File general.hpp

Direct translations

Overview

Preprocessing

Good representations

File general.hpp

Literature overview on boolean translations

Ladder logic standard

Input format

Output format

Iteration

Properties

File general.hpp

Connections

Transfer

Testing

transversal_hg

File general.hpp

Update namespaces : DONE

Create milestones : DONE

Update namespace-usage.

Travelling salesman

File general.hpp

Connections

Organisation

The triangle of the three possibilities

ind_hg(G)

File general.hpp

Overview on SMT

Overview on main types of constraints

How to translate these problems into our domain

Create new milestones

File general.hpp

Update namespaces.

Create module on NaeSat.

Create module on XSat.

Module on counting

File general.hpp
Update namespaces.
File general.hpp

Concept for aes-usage

Crypto++

OKgenerator

File general.hpp

Update namespaces.

Create milestones

Update namespace-usage.

Tests

File general.hpp

Create milestones

Write tests

Write docus

Indices

Algorithms for the hermitian rank

File general.hpp

Boost:

The basic concept for big integers should (just) include:

  • fully constructible
  • constructor from integral types
  • the assignment operations +=, *=, -=, /=, %=
  • the basic operation +, *, -, /, %
  • linear order
  • swap
  • absolute value
  • div and mod combined
  • partial specialisation of boost::numerical_cast
  • partial specialisation of boost::lexical_cast (from and to strings)
  • input and output streaming.

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 number-theoretical.)

File general.hpp

Update the namespace.

Boost

See the concepts in Concepts/plans/BigIntegers.hpp. DONE

File general.hpp

Basic notions

The main parameters

Polar and bipolar incidence structures

File general.hpp

Create namespace

Create milestones

File general.hpp

Update namespaces.

Organisation

File general.hpp

Matrices

Representing partial boolean functions

Analysing the extension-landscape

Generalisations

File general.hpp

Create a milestones file.

First Maxima implementation:

Axiom-atisation

File general.hpp
Create a milestones file.
File general.hpp

Compute propagation-hardness

DONE (function hardness_wpi_cs has been provided) Computing the hardness of a clause-set representation

Create milestones

Write docus

File general.hpp

Update namespace

Update namespace-usage

Update doxygen-documentation

Update plans, transfer todos

Reorganisation

New test system

Write docus.

Write demos.

Introduce subsumption hypergraph generator

File general.hpp

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

File general.hpp
Write CyclicGroups.mac<p>Write DiederGroups.mac
File general.hpp

Update namespace

Update the documentation

Documentation

Build system

Compiler warnings

File general.hpp

Update namespaces.

Graphics library

Graph visualisation library

External libraries / programs:

Concepts

Applications

Conversions

File general.hpp
Fundamental notions
File general.hpp
Create milestones
File general.hpp

Fundamental notions

Examples

Greedy algorithm

File general.hpp
External sources
File general.hpp

Rewrite hypergraph transversal functions in Maxima

Rewriting: All modules are to be redesigned and reimplemented in Maxima

File general.hpp

Function "min_scanning" (ComputerAlgebra/Numerical/Lisp/Minimisation.mac)

Implement the "downhill simplex method in multidimensions" (according to Nelder and Mead).

File general.hpp

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

File general.hpp

Connections

Translations to SAT

Using ILP

Exploiting known bounds

File general.hpp
Relations to other modules
File general.hpp
Create milestones.
File general.hpp

Architectures of the systems for showing/computing Ramsey-type numbers

Handling bounds

How to annotate numbers with justifications?

File general.hpp
Systematic notations for the numbers in Ramsey theory : DONE
File general.hpp

Develop plans

Create milestones.

File general.hpp

Blind search for backdoors of size k

2-CNF backdoors

Horn backdoors

Backdoors w.r.t. clause-sets of bounded deficiency

File General.hpp
Move all components in this module to appropriate new places.
File general.hpp

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

File general.hpp

Fundamental notions

Branching greedoids

File general.hpp

Relations to other modules

Automorphisms of Ramsey hypergraphs

Automorphisms of Ramsey clause-sets

Representing counter-examples

File general.hpp

Relations to other modules

Fundamental notions

Categories of boolean functions

File general.hpp

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

File general.hpp

Update output_pa

Create milestones

Write tests

Write docus

Notions for clauses, clause-sets etc.

Organisation

Input and output

File general.hpp

Create milestones

Write tests

Write docus

Conflict graph

Hermitian rank

Relations to other modules

mcind_cs, cind_cs:

File general.hpp

Relations to other modules

Handling of duplicate entries for vdW-numbers

Lower bounds

Considering finite commutative groups G

Automorphisms of van-der-Waerden hypergraphs

Automorphisms of van-der-Waerden clause-sets

File general.hpp

Create milestones.

Write the direct algorithm (running through all total assignments)

Write a scheme which uses r_k-splitting trees

okltest_satprob

satprob_mcind

satprob_incexl_hitting

Connect to the counting-module in part Satisfiability.

Sum-product (belief propagation) and beyond

Sampling falsifying assignments

File general.hpp

Add tests for parity generators

Update milestones

Accompanying statistics

Write basic docus

Variables

Flood-it

SMUSAT(1) and tree hitting clause-sets

Hard clause-sets (for resolution and refinements)

Operations (new clause-sets from old ones)

Hiding small unsatisfiable clause-sets

DONE Split Generators/Generators.mac

File GeneralisedUCP.hpp
First implementation, based on watched literals
File GeneralisedUCP.hpp

Connections

Update names

More efficient implementations

Strengthen the tests

Use oracles

File Generators.hpp

Generalisations of the Kneser graphs

Parameters of the Kneser graphs

Forms of complete graphs

File Generators.hpp

Counting, enumeration and sampling

Evaluating the Maxima function random_tree

Evaluating uniform_randomtree_og

File Generators.hpp

Write tests

Concept of a "propagator"

"n Queens"

Hitting clause-sets

File GenericBacktracking.hpp

Class OKlib::SATAlgorithms::Backtracking

Intelligent backtracking and learning

Integration

Goal

Test OKlib::SATAlgorithms::Backtracking<p>More flexible splitting

File Git.hpp

Prerequisites

Asciidoc

Info- and man-pages

Git book

Installation process

File Github.hpp

General usage strategy : DONE (we only use Github, no own server)

Github terminology and features

Collaborative work on github

SourceForge

File Glucose.hpp
Extracted data attribute names
File Gmp.hpp

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

File GMPWrapper.hpp

Design the concept of a wrapper for a big-int-class

Write tests for the concepts

Implementation of the basic wrappers: I guess, best based on the C-interface.

File GraphIsomorphisms.hpp

Vertex invariants

Alliances

What about the graph embedding problem ? This should likely go to another module.

File Graphs.hpp

General C++ graph libraries

Graph isomorphism

Graph drawing

Treewidth

Travelling salesman

Graph colouring

Cliques

Hamiltonian cycles and paths

File GraphTraversal.hpp

Implement the generic graph_traversal algorithm from the CS-232 script (generic enough, and with enough event-points, so that protocolling and visualisation are possible).

Implement the main applications or graph_traversal from the CS-232 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.

File GrayCodes.hpp

Basic concepts

Algorithms

Efficiency

File GreedyColouring.cpp
Specify the lexicographical order
File GreedyColouring.hpp
Complete doxygen documentation.
File GreedyColouring.hpp

Relations to other modules

Outsourcing

Class Greedy_colouring

GreedyColouring.cpp

Literature

How do these algorithms translate into SAT algorithms?

Local search for a good vertex ordering

Generalisation to hypergraphs

File GreenTao.cpp

Use InputOutput::CLSAdaptorDIMACSOutput

Use Messages

File GreenTao.hpp

Connections

Generator

File GreenTao.hpp

Connections

Further information on arithmetic progressions in prime numbers

File GreenTao.hpp

Connections and scope

The basic generators

Improving SAT translations

Improving GTTransversals

Improving GTTransversalsInc

File GreenTao_2-3-6.hpp

Finding the best algorithm from ubcsat

greentao_2(3,6) >= 2072

OKsolver_2002

Minisat2

march_pl

File GreenTao_2-3-7.hpp

Finding the best algorithm from ubcsat

Survey propagation

greentao_2(3,7) > 13800

File GreenTao_2-3-k.hpp

Investigate greentao_2(3,k)

SAT 2011 competition

greentao_2(3,4) = 79

Predicting greentao_2(3,k)

File GreenTao_2-4-4.hpp
greentao_2(4) = 512
File GreenTao_2-4-5.hpp

Finding the best local search solver

greentao_2(4,5) > 4231

Survey propagation

File GreenTao_2-5-5.hpp

greentao_2(5) > 33500

Survey propagation: greentao_2(5) > 34308

Conjecture: greentao_2(5) = 34309

File GreenTao_2-5-5_OKsolver.hpp
greentao_2(5) : threshold behaviour of OKsolver-2002
File GreenTao_3-3-3-k.hpp

greentao_3(3,3,4) >= 434

greentao_3(3,3,5) > 1989

Upper bounds

File GreenTao_3-3-4-k.hpp

greentao_3(3,4,4) > 1662

greentao_3(3,4,5) > 8300

File GreenTao_3-3.hpp

DONE (available now) Symmetry breaking:

adaptnovelty+

OKsolver_2002

march_pl

satz215

minisat2

picosat913

precosat236

Why is minisat2 so much faster than OKsolver_2002 ?

File GreenTao_3-4-4-k.hpp
greentao_3(4) > 5500
File GreenTao_4-3-3-3-4.hpp

Best local search algorithm

Lower bounds: greentao_4(3,3,3,4) > 1052

File GreenTao_4-3-3-4-4.hpp

Best local search algorithm

greentao_4(3,3,4,4) > 2750

File GreenTao_4-3.hpp

Best local search algorithm

Lower bounds: greentao_4(3) > 384

Upper bounds

Minisat2 for n=377

Picosat913 for n=377

OKsolver for n=377

File GreenTao_te_m-3-3-3.hpp

greentao_4(2,3,3,3) = 151

greentao_5(2,2,3,3,3) >= 154

File GreenTao_te_m-3-3-4.hpp

greentao_4(2,3,3,4) >= 453

greentao_5(2,2,3,3,4) >= 472

File GreenTao_te_m-3-3.hpp

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

File GreenTao_te_m-3-4.hpp

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

File GreenTao_te_m-3-5.hpp

greentao_3(2,3,5) = 581

greentao_4(2,2,3,5) >= 582

greentao_5(2,2,2,3,5) >= 610

File GreenTao_te_m-4-4.hpp
greentao_3(2,4,4) >= 553
File GreenTaoGCNF.cpp

Improve implementation

Compare with specification

Provide other translations

File GreenTaoProblems.hpp

Connections

Generator for Green-Tao problems

Statistics on the number of arithmetic progressions

Computing minimum transversals

File GreenTaoProblems.hpp

Connections

Standardisation

Statistics

Statistics output for Green-Tao problems in the Dimacs-file

Symmetry breaking for GT-problems

Arithmetic progressions for prime numbers

File GrosswaldHagisFormula.hpp

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 k-values : DONE

DONE (when using time, then the output needs to be copied to a file) Potential bug

File Groupoids.hpp

Encodings

Quasigroups

Literature surview

Discrete groupoids

File Guidelines.hpp
Calling sub-tests
File Hardness.hpp
Influence of totally blocked clauses
File HashMaps.hpp

Introduce memoise function wrapper

Using the Maxima "associative arrays"

New naming conventions

Concept of a set-theoretical map

Improving the hash-maps

Improving the okl-arrays

File Hindman.hpp
Class Generators::Hindman_k2
File Hindman.hpp
How to get a kind of version number like CVS's?
File Hindman.hpp

Implement iterator-forms

Implement general functionality (arbitrary k)

Implement "all products"

File Hindman.hpp

Connections

Write simple generator for boolean problems (r=2)

File HindmanProblems.hpp

Improve generator names

The notion of a "Hindman parameter tuple"

Write tests

File History.hpp
Package history : DONE
File HittingClauseSets.hpp

Organisation

Connections

Allowed parameter values

Constructions

max_var_hitting_def

Representations

Decomposing clause-sets into hitting clause-sets

Generators for unsatisfiable hitting clause-sets

Generators for satisfiable hitting clause-sets

derived_hitting_cs_pred_isoelim

Non-singular unsatisfiable hitting clause-sets of given deficiency

all_cld_uhit_minvd

File HomePage.hpp

Complete local home page

Improved logo

Meta tags : DONE

File Homomorphisms.hpp

Organisation

Naming conventions

Isomorphisms

Transport via homotopies

Homotopisms

Induced congruence relation

File Homomorphisms.hpp

Organisation

Brute-force automorphism enumeration

Handling of automorphism groups

Visualising automorphisms

Deciding whether for given H there is a graph morphism G -> H

File Horn.hpp

Relate to ComputerAlgebra/Satisfiability/Lisp/Backdoors/plans/general.hpp.

Design for the algorithm "sb-horn" from [Nishimura, Ragde, Szeider; 2003, Detecting Backdoor Sets with Respect to Horn and Binary Clauses] (developers SS, MS, OK)

File HypergraphColouring.hpp

Relations to other modules

First prototypes

File Hypergraphs.hpp

Organisation

Lazy combinatorial matrices

Implication graphs

File ImplicitConversionsBoost.hpp

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 run-time and run-space efficiency (with compiler optimisation turned on they should not).

File IncludeHandling.hpp
More flexible tools are needed for
File IncludeHandling_Tests.hpp
More thorough testing: For example if we want to test container class X, and we initialise a data member, then we should check that member.
File Input_output.hpp
The new implementations (see below) could be the starting point for a generic Dimacs input library (belongs to the module InputOutput)
File InputOutput.hpp

Documentation

Dot-format

Reading graphs in dot-format

Maxima graphs-package

Other graph-formats

File InputOutput.hpp

Transfer the tests to the new test system.

Write concept InputStreamable (and related constructs).

File Inv_8.hpp

Basic data

r_1-bases : mincl_r1 <= 4200

Using weighted MaxSAT to compute small CNFs

Find the symmetries of the AES inversion DNF

File InverseSingularDP.hpp

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

File Isomorphisms.hpp

Isomorphism testing by backtracking

Connections to other modules

Invariants for matrix isomorphism

Invariants for square matrix isomorphism

Self-duality

Valued matrices and their homo- and isomorphisms

File IsomorphismTypes.hpp

The notion of isomorphism

Enumerating isomorphism types

Considering special boolean functions

File IteratedConditionSystems.hpp

Basic notions

Finding literature

The trivial algorithm

AES as an ics

Applications from railway safety

File IteratorHandling_Tests.hpp
Testing of the iterator adaptors for sequences.
File Iterators.hpp

First the Boost-iterator-concepts 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

File KnownKeyBits.hpp

Translations

Overview

Transferring the Argosat-desgen example

Canonical+ translation for the S-box (6-to-4)

Canonical translation for the S-box (6-to-4)

Applying SplittingViaOKsolver

DONE Add todos

DONE Summarise results

File LanguageNames.hpp

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 string-matching algorithm (for realising the map in Messages::LanguageName).

File Languages.hpp

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:

  • "Austria" in French?
  • "Untranslated" in French?

Doxygen documentation Doxygen documents the macros OKLIB_QUOTE and OKLIB_QUOTED_SEQUENCE, although they are undefined --- how to correct this?

File LatinSquares.hpp

Relations to other modules

Organisation

Different encodings

Further conditions

Update

Systematisation

Extensions

Generators for latin square completion problems

File LBounds.hpp
Mathematical precise proofs
File LeanKernel.hpp

Lean kernel via variable-elimination

Lean kernel via oracle for leanness-decision

File Learning.hpp

Connections

basic_learning

Intelligent conflict-analysis

File Levels.hpp

Write tests (in the new test system).

Doxygen documentation The explicit instantiation of Messages::S<Basic> is not listed --- how to correct this?

File LexicographicalEvaluation_Tests.hpp
Distinguishinging between basic and enhanced tests is needed; running through these big files is "enhanced testing".
File LexicographicalEvaluationPolicies.hpp

Write a concept.

Write accompanying Test and Testobjects files.

Class LexicographicalSeriesPolicy
Write a concept.
File LibraryBasics.hpp
Update the above description (several macros below are not captured yet).
File LibraryBasics.hpp

Should the helper-classes for archetype-definitions (like Concepts::convertible_to_bool) go into their own file?

Should boost/type_traits.hpp be replaced by the tr1-components?

Perhaps the macros need some clean-up.

Transfer the tests to the new test system.

File Licence.hpp
Licence maintenance
File Linear.hpp

Connections

Affine bijections over ZZ_2

The complement of the diagonal matrix

Random sampling

Mathematical investigations

File LinearAutarkies.hpp
Finding linear autarkies
File LinearEquations.hpp

Connections

gen_2xor_fcl

Translating two xor-clauses

File LinearMap_8.hpp

Basic data

Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 48

File LinearProgramming.hpp
Handling of variables
File LineHandling.hpp
Extend doxygen-documentation for Messages::MessagesPrePost<p>Write demo-programs for Messages::MessagesLines and Messages::MessagesPrePost<p>Generic testing of MessagePrePost-classes:
File LinInequal.hpp

Update function names

Complete LinInequal.cpp

Also handle ">=" and "=" (besides "<=")

Create Doxygen documentation

Restore old "assignment-application"

Improve VdWTransversals and VdWTransversalsInc

Write docus

File Lisp.hpp

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 64-bit Xeon machine

DONE (no longer in active development, and thus not considered anymore) Installing and using GCL

Installing other Lisp's

File Lists.hpp

Generating list of elements 1 to n

Apply-functionality

Correct implementation of some_s and every_s

In-place modification

Improving sort_length

Improve partition_list_eq

Correct split_list and split_list_epo

File Literals.hpp
Boolean literals, and more general literals
File Literals.hpp

Arity

Generalised literals:

Requirements literals

File Logical.hpp
Likely the macros are superfluous, and should be removed.
File Logical_Testobjects.hpp
Likely the special namespace Metafunction_tests should be eliminated.
File Logics.hpp

Hets

Proof assistants

Modal logic

Support for bounded arithmetic

File MachineLearning.hpp

Weka

Repositories

Book [Machine Learning, Tom Mitchell]

File MailingLists.hpp

DONE Mailing lists

Instructions

User mailing list

File Makefile.hpp

Documentation

Future of this makefile:

File MakeSystem.hpp

Makepp

DONE (we don't use CMake ourselves, and let the Linux distribution provide it) CMake

Competition extraction tools

File ManipParam.cpp
Better parameter-handling
File Marginalisation.hpp
Implementation
File Marx2008.hpp

Create milestones

Data

Functional analysis

Relational analysis

File MatchFiles.cpp

Replace use of boost-regex by the facility from the standard library.

Use module ProgramOption (once available).

File MatchingAutarkies.hpp

Connections to other modules

Matching satisfiability

Deciding matching leanness

Finding matching autarkies

Computing the matching-lean kernel

Computing a quasi-maximal matching autarky

Surplus

File Maxima.hpp

Why is Maxima file output so slow?

DONE (this was fixed in Maxima, after communication on the mailing-list) Stable sorting

DONE (transferred to docus) Restricted recursion for memoised functions

Memoised functions

Argument-length restriction

How to use function-parameters reliably??

Problems with errcatch

What is "equalp" ?

Maxima/CLisp bug for larger data-sets

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

File Maxima.hpp

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

System-wide installation

Handling of redefined load-function

File Maxima_Init.hpp

DONE (now Ecl-memory-management only loaded for Ecl) Using CLisp

What memory-bounds?

File MaximiseMinVarDegrees.hpp

Minimally unsatisfiable clause-sets

Unsatisfiable non-singular hitting clause-sets

File MaxVarDegrees.hpp

Minimal variable-degree of uniform minimally unsatisfiable clause-sets

Pumping up binary clauses

Implementing [Hoory, Szeider, SIAM Discrete Mathematics, 2006]

File Measures.hpp

Basic statistics

Conflict-independence number

Conflict-partition_number

Hermitian rank

Characteristic polynomial

File MemoryManagement.hpp
Improve default_memory_ecl
File Messages_Testapplication.cpp
Transfer to the (new) test system.
File MessagesBase.hpp

Write tests (in the new test system).

Create a Messsages-concept.

File MessagesMain.hpp
Write tests (in the new test system; at least consistency checks for the macros).
File Methods.hpp

Overview

Connections

Tidy hitting-clause-set todos and move method here

Add instructions for using Pseudo-boolean 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.

File MGDissertation.hpp

Complete "From groupoids to groups" (MG)

Section "Actions and operations"

Create more todos.

Explain macros (MG) DONE

File MGPhDThesis.hpp

Overview

Differences between MG_PhDThesis.tex and 2011_SAT_MGOK.tex

File MGThesis.hpp

Chapter 2 - Boolean functions and Satisfiability

Throughout

Introduction

LaTeX corrections/improvements

File MGWorkflow.hpp
Day to day topic themes
File Mhash.hpp
Complete MHash documentation
File MHash.hpp

Continuing with MHash ?

Computing the md5sum-value of a directory

File milestones.hpp
Refine milestones.
File milestones.hpp
Update the following milestones.
File milestones.hpp
Update the following milestones.
File milestones.hpp
Create new milestones.
File MinimalAssignments.hpp

Brute-force 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.

File MinimalSatisfyingAssignments.hpp
Implement the trivial algorithm
File MinimiseMaxVarDegrees.hpp

Low variable-degrees and high clause-lengths

Unsatisfiable non-singular hitting clause-sets

File MinimumTransversalsMongen.cpp
Making the types available
File Minisat2.hpp
Move read_minisat2_output functionality to wrapper script
File MinOnes2PseudoBoolean.cpp

Improve specification

Move to correct place

File MinOnes2WeightedMaxSAT.cpp

Improve specification

Move to correct place

File MinVarDegrees.hpp
Organisation
File MixColumns.hpp

Sizes (and structure)

Direct linear representation

Computation of r_k-bases

16-bit MixColumn operation (2x2 matrix)

File MLDissertation.hpp

Improving notations

Improving usage of Latex

Section "Category of literal structures"

Correction of errors

Transfer to part "Dissertation"

File ModelChecking.hpp

Model checking and variations

BAT

File Mul_11_8.hpp

Basic data

r_1-bases : mincl_r1 <= 1376

Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 66

File Mul_13_8.hpp

Basic data

r_1-bases : mincl_r1 <= 1040

Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 60

File Mul_14_8.hpp

Basic data

r_1-bases : mincl_r1 <= 1052

Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 56

File Mul_2_8.hpp

Basic data

Minimising using hypergraph transversal tools : mincl_rinf = 20, num_mincl_rinf=102

r_1-bases : mincl_r1 <= 22

File Mul_3_8.hpp

Basic data

Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 36

r_1-bases : mincl_r1 <= 80

File Mul_9_8.hpp

Basic data

r_1-bases : mincl_r1 <= 272

Using weighted MaxSAT to compute small CNFs : mincl_rinf <= 42

File Mul_e_4.hpp

Basic data

Generating all minimum representations via hypergraph transversals

File Mul_e_8.hpp

Links

Basic data

File MultipleParameters.hpp

Linear combination

Experimentation:

File Multiplexer.hpp
Complete the documentation.
File MultivaluedPartialAssignments.hpp

Implementation OKlib::PartialAssignments::MultiPASS

Test OKlib::PartialAssignments::MultiPASS

File Musatd2.cpp
Write application tests
File NestedTranslation.hpp

Strong form

The order of Horn clauses

The reduced forms

File NonBoolean.hpp
Notions for generalised literals
File NonBooleanTranslations.hpp

Connections to other modules

Add standardised translations

Generalised canonical translation

DONE Translating non-boolean clause-sets into boolean clause-sets

DONE Add translations for non-boolean clause-lists with uniform domain

File Numbers.hpp

Connections to other modules

Update the number-system

Computation of initial sequences of transversal GT-numbers

File Numbers.hpp

Weak specifications

Write docus

Add known Ramsey bounds

Proofs of numbers

Ramsey numbers

File Numbers.hpp

Connections to other modules

General organisation

Improving exactf_tau_arithprog

Improving initial_sequence_vdWt

The LRC-formula

Transversal and independence numbers

File Numerical.hpp

Write Factorial.

What about the generalisations discussed for Power?

Class Numerics_Tests::test_round< Round >

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):

File OK_RamseyTheory_2vdWshort.hpp

Numbers to be included

Improving SplittingViaOKsolver

Other SAT solvers

Target-journal JSAT

File OK_XSZ_min_degree.hpp

General plans

DONE (now left/right-overarrows are used, which look somewhat nicer) Is there a better symbol for the min-var-degree?

First article

DONE (everything has been transferred resp. generalised) Transfer XSZ's original preprint

Transfer OK's notes

Incorporate XSZ new report (from SAT2009)

Class OKlib::Combinatorics::Hypergraphs::Generators::Accumulate_l< V, Num >

Create application tests.

Create unit tests.

Move to stratification submodule.

Class OKlib::Combinatorics::Hypergraphs::Generators::Arithmetic_progression< Integer >

Add the concept tag (a special case of a "const collection with begin, end and size; not default-constructible, but copyable, assignable, equality comparable").

See class IteratorHandling::Arithmetical_progression in General/IteratorHandling.hpp

Class OKlib::Combinatorics::Hypergraphs::Generators::Arithmetical_progressions< Int >
Integration
Class OKlib::Combinatorics::Hypergraphs::Generators::Arithmetical_progressions_colex< Int >
Integration
Class OKlib::Combinatorics::Hypergraphs::Generators::First_prime_numbers< UInt >
Move to module Structures/NumberTheory
Class OKlib::Combinatorics::Hypergraphs::Generators::GreenTao< UInt >

Complete implementation

To be tested

Class OKlib::Combinatorics::Hypergraphs::Generators::Hindman_k2< UInt >

To be implemented

To be tested

Design of the concept

Class OKlib::Combinatorics::Hypergraphs::Generators::Iterator_arithmetic_progression< Integer >
Make a const random iterator out of it.
Class OKlib::Combinatorics::Hypergraphs::Generators::Pd_arithmetical_progressions< Int >
Integration
Class OKlib::Combinatorics::Hypergraphs::Generators::Pd_arithprog_ohg< Int >

Update concepts

Write tests

Improve implementation

Class OKlib::Combinatorics::Hypergraphs::Generators::Sizes_strata_indmon< Vertices, Hyperedges >

Create application tests.

Create unit tests.

Move to stratification submodule.

Class OKlib::Combinatorics::Hypergraphs::Transversals::Bounded::DirectStratification< SetSystem, UInt >

Move to stratification module.

Handling of order

Write tests

Class OKlib::Concepts::Assignable< T >
Shouldn't there be a concept "CopyAssignable", which also requires that copying and assigning have the same effect?
Class OKlib::Concepts::Container< C >

What is the meaning of type-members "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 container-concepts 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.).

Class OKlib::Concepts::EqualityComparable< T >
LessThanComparable_Archetype should use the provided type convertible_to_bool.
Class OKlib::Concepts::EqualityComparable_Axiom_reflexivity< T >
Should be an instance of a general reflexivity-test.
Class OKlib::Concepts::EqualityComparable_Axiom_symmetry< T >
Should be an instance of a general symmetry-test.
Class OKlib::Concepts::EqualityComparable_Axiom_transitivity< T >

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 transitivity-test.

Class OKlib::Concepts::EqualityComparable_basic_test_one_object< T >
Shouldn't be syntax-checking included here?!
Class OKlib::Concepts::InputIterator< Iterator >

"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.

Class OKlib::Concepts::LessThanComparable< T >
LessThanComparable_Archetype should use the provided type convertible_to_bool.
Class OKlib::Concepts::LessThanComparable_Axiom_asymmetry< T >
Should be an instance of a general asymmetry-test.
Class OKlib::Concepts::LessThanComparable_Axiom_equivalence_transitivity< T >

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).

Class OKlib::Concepts::LessThanComparable_Axiom_irreflexivity< T >
Should be an instance of a general irreflexivity-test.
Class OKlib::Concepts::LessThanComparable_Axiom_transitivity< T >

To conform with the other tests here, it should be applicable under all circumstances?!?

Should be an instance of a general transitivity-test (see already above).

Class OKlib::Concepts::LessThanComparable_basic_test_one_object< T >
Shouldn't here also syntax-checking be involved?
Class OKlib::Concepts::LessThanComparable_basic_test_three_objects< T >
For the transitivity check, currently a < b and b < c is assumed. Likely this should be generalised.
Class OKlib::Concepts::ResultElementWithName_basic_test< Res >
To be completed, by creating suitable names and result elements from those names, and calling the above sub-tests; furthermore the available general tests on linear orders shall be employed.
Class OKlib::Concepts::tests::AtomicCondition_basic< AC >
Create basic semantic tests.
Class OKlib::Concepts::tests::Literals_basic< Lit >
Create basic semantic tests.
Class OKlib::Concepts::Variables< Var >
Archetype
Class OKlib::Concepts::VariablesLiterals_tag< Var_tag, Lit_tag >
It seems besides providing such a combined tag, we need also to provide "projections", which enable us to extract from such a combined tag the Var-tag and the Lit-tag? Or perhaps not, since all what is needed from the combined tag are the base classes (for tagging-polymorphism)?
Class OKlib::Concepts::VariablesWithIndex_Axiom_index_identity< Var >
This axiom actually should go into a refinement (variables with equal indices could be different, for example when used in different contexts) ?!?
Class OKlib::GeneralInputOutput::DirectoryIterator

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 past-the-end iterator. The concept InputIterator should refine InputIteratorDefault and MultiPassInputIterator (???).

Member OKlib::GeneralInputOutput::NullStream
How can we define a global constant like std::cerr and std::cout?
Class OKlib::GeneralInputOutput::Test_DirectoryIterator< DirectoryIterator >

Using path-equality or path-equivalence ?

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 non-trivial cases.

Class OKlib::GeneralInputOutput::Test_OStreamMultiplexer< OStreamMultiplexer >
Use test for OStreamDescriptor as subtest.
Class OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >

For the output-jobs message-classes should be employed.

Handling of extended Dimacs-format (with real variable-names) is needed:

Class OKlib::InputOutput::CLSAdaptorPreciseStatistics< Int, String >

Correction : DONE

Extensions : DONE

Class OKlib::InputOutput::CLSAdaptorStatistics< Int, String >
CLSAdaptorPreciseStatistics
Class OKlib::InputOutput::Statistics< Int >

For the output better a message-class is provided.

Create a concept

Class OKlib::InputOutput::Test_StandardDIMACSInput< StandardDIMACSInput >

Extending the tests (not just checking whether the statistics are right).

Test with the archetype of a CLSAdaptor.

For the negative tests:

  • catch all exceptions thrown
  • test the specific exceptions thrown.

For the positive tests:

  • catch all exceptions thrown.

Test for errors where the numbers read-in are too large to be represented.

Class OKlib::Iterators::counting_iterator< Incrementable, CategoryOrTraversal, Difference >
Example where this extension is really useful?
Class OKlib::Iterators::Test_counting_iterator< counting_iterator >
Yet the tests are very sporadic:
  • Use the generic test facilities to check whether counting_iterator is actually a forward iterator etc.
  • Test whether all specific functionality of boost::counting_iterator has been transferred.
Class OKlib::LatinSquares::SudokuProblem< Box_size, BijectivityConstraint >

Once we have fixed the concepts (a bit more), likely we should rename the parameter BijectivityConstraint.

More doxygen-documentation is needed.

Class OKlib::LatinSquares::Trivial_reduction_Sudoku< SudokuP >
This should be the responsibility of the alliance, or? (Like "generalised UCP" ?!)
Class OKlib::Matrices::Is_equal< Matrix >

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.

Class OKlib::Matrices::Is_self_dual< Matrix, PermutationsGenerator >

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 Gray-codes, then an improved implementation should be able to exploit this.

Enquiry to the boost e-mail list, whether somehow uBLAS can handle row and column permutations?

Class OKlib::Matrices::Is_self_polar< Matrix, PermutationsGenerator >

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.

Class OKlib::Matrices::Is_symmetric< Matrix >

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 e-mail list why is_symmetric is not provided (see above).

Class OKlib::MetaProgramming::Power< b, e >

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, e-1>::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:

Class OKlib::Parallelism::CounterWithMutex< N >

Document the class (what's the point of the strange design?).

Can assertions be made about member mutex?

Class OKlib::Parser::Test_ParsingString< Parser >
What is the future of this class?!
Class OKlib::Programming::Sequences::tests::CommonPart< CP, ImpPol >
Yet only the non-const version is handled.
Class OKlib::Programming::Utilities::OrderRelations::Colexicographical_comparison< Container >

Generalise to Ranges

Write tests

Class OKlib::Programming::Utilities::OrderRelations::SizeLessThan< LessThanRelation >
Write tests
Class OKlib::Refactoring::BaseTestData
Eliminate this class, making the type members template parameters of the other (yet derived) classes.
Class OKlib::Refactoring::ExtendIncludeDirectives< APC, UniquenessPolicy >

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. !!

Class OKlib::Refactoring::ExtendIncludeDirectivesTwoRanges< ReferenceRange, WorkingRange, UniquenessPolicy, HandleProgramRepresentation >

Write two models for the strategy.

Write a convenience function for the type deduction.

Class OKlib::Refactoring::IncludeDirective< String >

A concept is needed.

Test inequality operator.

Class OKlib::Refactoring::IncludeParsingGrammar

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 parse-function which then instantiates the IncludeParsingGrammar and ProgramRepresentationIncludes accordingly to the character type actually used.

A concept is needed.

Class OKlib::Refactoring::PrefixTestData
Urgently add some more test cases.
Class OKlib::Refactoring::StreamExtractor_by_copy
Extended explanation as above.
Class OKlib::Refactoring::StreamExtractor_by_istream_iterator

Extended explanation should mention the other implementation.

Management of stream-formatflags-resources should be handled by (RAII) object.

Write a test for it.

Create a concept.

Class OKlib::Refactoring::Test_ExtendIncludeDirectives< ExtendIncludeDirectives >

Wrong template arguments.

Testing of all functionality (including exceptions thrown).

Class OKlib::Refactoring::Test_IncludeDirective< Include_Directive >

Add an extended description.

Testing of equality and inequality operators.

Class OKlib::Refactoring::Test_IncludeParsingGrammar< Include_Parsing_Grammar >

Reinstate testing of program strings which are not matched by the grammar.

Add an extended description.

Class OKlib::Refactoring::Test_Parsing< Program_Representation_Includes, StreamExtractor >

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?

Class OKlib::Refactoring::Test_ProgramRepresentationIncludes< Program_Representation_Includes >

Add an extended description.

Testing of equality and inequality operators.

Class OKlib::Refactoring::TestData

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.

Class OKlib::SATAlgorithms::Backtracking< ExtProblem, Red, Heur, Vis >
Update
Class OKlib::SATCompetition::ElementaryAnalysis< Database >

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 ?

Class OKlib::SATCompetition::LexicographicalEvaluation< IndexedDatabase, SeriesPolicy, NumberType >

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 pair-type here, since for pair-types 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).

Class OKlib::SATCompetition::PurseScoring< IndexedDatabase, SeriesPursePolicy, NumberType >

Concepts for IndexedDatabase and SeriesPursePolicy are needed.

Make the implementation more efficient by storing intermediate results.

Class OKlib::SATCompetition::ResultDatabase< ResultIterator >
Create a concept for ResultDatabase:
  • ResultIterator is an input iterator, ResultIterator::value_type is Result or ResultRandomSat (yet). It is assumed that the lifetime of these results is as long as the lifetime of the ResultDatabase object.
Class OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >

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.

Class OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::scoring
Not only the number of instances solved, but also the number of sat and unsat instances solved.
Class OKlib::SATCompetition::Test_LexicographicalEvaluation< LexicographicalEvaluation >
Checking the average running times.
Class OKlib::SATCompetition::Test_LexicographicalEvaluationRandom< LexicographicalEvaluationRandom >

Completing like Test_LexicographicalEvaluation.

Checking the average running times.

Checking the order details of the variations on lexicographical ordering.

Class OKlib::SATCompetition::Test_RepresentationSolverSeries< LexicographicalEvaluation >
Complete the tests as outlined below (using the extended test machinery).
Class OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithQueue< Lit >

Provide specification

Write unit-tests

Improve implementation

Class OKlib::Satisfiability::Assignments::TotalAssignments::BAssignmentWithRQueue< Lit >
Complete.
Class OKlib::Satisfiability::Interfaces::InputOutput::GeneralisedHypergraphColouring< SetSystem, Int >

Write tests.

Would the use of smart pointers be appropriate?

Class OKlib::Satisfiability::Interfaces::InputOutput::HypergraphTwoColouring< SetSystem, CLSAdaptor, Int >

Handle the range-requirements correctly.

Provide the mapping-information in the comments.

Class OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsSets< Lit >
Write unit-tests.
Class OKlib::Satisfiability::ProblemInstances::Clauses::RClausesAsVectors< Lit >
Write unit-tests.
Class OKlib::Satisfiability::ProblemInstances::Clauses::WatchedLiterals_mono< Lit >

Complete the concept

Provide unit-tests

Complete sequence-member-functions

Improve implementation

Class OKlib::Satisfiability::Reductions::KLevelForcedAssignments::CLSAdaptorKUcp< WatchedClauses, Assignment >

Complete implementation

Write unit-tests

Class OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcp< Lit, Clauses >

Complete container-functionality

Write unit-tests.

Improve implementation

Use messages.

Separate the transfer from the unit-clause propagation

Harmonise with KLevelForcedAssignments::CLSAdaptorKUcp

Class OKlib::Satisfiability::Reductions::UnitClausePropagation::CLSAdaptorUcpW< WatchedClauses, Assignment >

Complete specification

Complete implementation

Write unit-tests

Harmonise with UnitClausePropagation::CLSAdaptorUcp

Class OKlib::SearchDataStructures::AssociativePrefixContainer< Range >

In a new module Iterators a metafunktion InverseRange<Range> should be implemented (in sub-module 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).

Class OKlib::SearchDataStructures::BaseTestData

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.

Class OKlib::SearchDataStructures::ExtensionTestData
Again the problem with the static data members!
Class OKlib::SearchDataStructures::PrefixTestData

What is the meaning of the *two* vectors?

Static data member should need no constructor!!

Class OKlib::SearchDataStructures::Test_AssociativePrefixContainer< PrefixContainer >

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.

Class OKlib::SetAlgorithms::Erase< Container >
Organisation
Class OKlib::SetAlgorithms::MapValue< Map >

There should also exist another version which returns the function value as a copy.

Via an error-policy there should be the possibility to throw an exception in case of an argument not in the domain.

Class OKlib::SetAlgorithms::Subsumption_elimination< ContainerSets, UniquenessTag, OrderTag, SizeTag >

Improve implementation

Create the concept

Class OKlib::SetAlgorithms::Test_Subsumption_elimination< Subsumption_elimination >

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.

Class OKlib::TestExecutionTools::Test_Empty< Empty >

Test also the concept.

Error reporting: Indices.

Class OKlib::TestExecutionTools::Test_Id< Id >

Test also the concept.

Error reporting: Indices.

Class OKlib::TestExecutionTools::Test_Total< Total >

Test also the concept.

Error reporting: Indices.

Class OKlib::TestExecutionTools::TestAntisymmetry< Range, BinaryPredicate >
Error reporting: report the indices.
Class OKlib::TestExecutionTools::TestAsymmetry< Range, BinaryPredicate >
Error reporting: report the indices.
Class OKlib::TestExecutionTools::TestEquivalence< Range, BinaryPredicate >
Error reporting: report the indices.
Class OKlib::TestExecutionTools::TestIrreflexivity< Range, BinaryPredicate >
Error reporting: report the index.
Class OKlib::TestExecutionTools::TestQuasiorder< Range, BinaryPredicate >
Error reporting: report the indices.
Class OKlib::TestExecutionTools::TestReflexivity< Range, BinaryPredicate >
Error reporting: report the index.
Class OKlib::TestExecutionTools::TestSymmetry< Range, BinaryPredicate >
Error reporting: report the indices.
Class OKlib::TestExecutionTools::TestTotality< Range, BinaryPredicate >
Error reporting: report the indices.
Class OKlib::TestExecutionTools::TestTransitivity< Range, BinaryPredicate >
Error reporting: report the indices.
Class OKlib::TestExecutionTools::TestTrichotomy< Range, BinaryPredicate >
Error reporting: report the indices.
Class OKlib::TestSystem::messages::BasicTestDescription
While we use capitalised "Test function" etc., the test-level comes out as "test level" etc..
Class OKlib::TestSystem::messages::ErrorDescription
Provide different output-languages.
Class OKlib::TestSystem::messages::LogDescription
Once the message-construction is more powerful, generalised the handling of the different levels and languages accordingly:
Class OKlib::TestSystem::messages::NotEqual< T1, T2 >
Provide different output-languages.
Class OKlib::TestSystem::messages::TestException
Provide different output-languages.
Class OKlib::TestSystem::messages::TestLevelDescriptions
How to handle that sometimes we may want to start with "Test level" instead of "test level" ?
Class OKlib::TestSystem::OutputWrapper2< T >
Should this class go to a general output facilities module?
Class OKlib::TestSystem::OutputWrapper3< T >
Should this class go to a general output facilities module?
Class OKlib::TestSystem::OutputWrapper< T >

Should this class go to a general output facilities module?

Should this class go to a general output facilities module?

Class OKlib::TestSystem::TestBase
Use Messages.
Class OKlib::TestSystem::tests::TestSystem

Complete it.

Doxygen documentation.

Improve the output (a more systematical approach for better structuring; and replacing the use of trivial messages).

Member OKLIB_TEST_EQUAL_RANGES (c1, c2)
Upgrade to OKLIB_THROW_M.
Member OKLIB_TEST_EQUAL_W (v1, v2)
Likely the same treatment as for OKLIB_TEST_EQUAL is needed (to avoid double evaluation).
Member OKLIB_TESTDESCRIPTION
Explain its usage.
File OKsolver.hpp

DONE (outputting "NA" in case field does not exist) Handling splitting output

Write extraction tool

R-problem with read_oksolver_mon

Object-oriented syntax

Function plot_oksolver_mon_nodes

Function summary_oksolver

Function hist_oksolver_mon_nodes

File OKsolver2002.hpp

Differences to the original OKsolver2002

Annotated tree output

Improving the implementation

Tree pruning ("intelligent backtracking")

Local learning

Adding look-ahead autarky clauses

Counting satisfying assignments

File OKsolver_1_0.hpp

Once we are ready to start, a new sub-module is needed

Update namespaces

First in computer-algebra

Create first milestones.

Create detailed milestones until completion

File OKsolver_2_0.hpp

New planning

Once we are ready to start, a new sub-module 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 clause-sets with (at least) three members :

DONE (not done, since there are no active clause-sets) Further sub-division of the instance

After-burner 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 clause-sets 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 activity-based ideas could be considered for OKsolver version 3) Heuristics

Local search

DONE (the open questions now are about self-abortion and full restart, and that's a question of the time-prediction) 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) Time-prediction

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

File OKsolver_3_0.hpp

Once we are ready to start, a new sub-module 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.

File Optimisation.hpp

COIN-OR

Linear and integer programming

Local search

File OrthogonalSquares.hpp
Experiments with the example from [Knuth, Vol. 4, Fascicle 0]
File OrthogonalTriples.hpp

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

  • vector_product (not in Boost::Ublas ?)
  • orthogonal (checking needs to be improved) to appropriate modules, and test them.

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 33-point 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.

File PackageBuilding.hpp

DONE Package directory structure

Providing update mechanisms for the package-clone

CreatePackage extensions

File ParameterTuning.hpp
Selecting the best parameters
File PartialAssignments.hpp

Connections

Boolean partial assignments

File PartialAssignments.hpp

Exceptions

Improvements of InputOutput::ReadPass

Write unit-tests

File PathDifference.cpp

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.

File PdNumbers.hpp
Palindromic numbers
File PdVanderWaerden.cpp

Use InputOutput::CLSAdaptorDIMACSOutput

Use Messages

File Permutations.hpp

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 "non-intrusive" generator, while a more efficient generator would be "intrusive".

Implement lexicographic enumeration

Implement enumeration with only one neighbour-swap to get to the next permutation. This is the equivalent to Gray-codes (see GrayCodes.hpp), and similar considerations apply).

File Persons.hpp
Developers information : DONE
File Picosat.hpp
Move read_picosat_output functionality to wrapper script
File Pigeonhole.hpp

Standard variable ordering for extended-pigeon-hole formulas

Update the php-functions

Extended Resolution clauses for the Pigeon Hole Principle

DONE Add tests for weak_php_ext_fcs

File PlantedSolutions.hpp
Uniquely satisfiable problems
File PointOfUnsatisfiability.hpp

Connections

Finding the n where a problem series changes from SAT to UNSAT

Simpler strategies

File Poker.hpp

Links

Scope

Definitions and probability calculations

Poker assistant

File PostgreSQL.hpp

Missing pgsql/libpq-fe.h

Improvements

File PreprocessSplitting.cpp

Better error messages

Write application tests

File PrimeImplicatesImplicants.hpp

Tests

Organisation

Best method for prime_clauses_cs

Improving min_extdp_cs

min_2resolution_closure_cs

Dualisation

Connections

Hitting clause-sets

contained_prime_implicate

File PrimeNumbers.hpp

Connections

Enumerating prime numbers

count_primes

product_primes

File ProbabilityOfSuperiority.hpp

The wider framework

Specifications for ProbabilityOfSuperiority.R

Write docus

File ProcessSplitViaOKsolver.hpp

Better stopping

More powerful processing options

DONE (available now with ProcessiCNF) Option for using only decision variables with ProcessSplitViaOKsolver

Class ProgramRepresentationIncludes< String >

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.)

File ProjectivePlanes.hpp
Projective planes with polarity
File Prolog.hpp

Swi Prolog

Gnu Prolog

File Proofs.hpp

php_ext_resl

Resolution trees

Resolution proofs

Read-once resolution proofs

File PseudoBoolean.hpp

Install pseudo-boolean solvers

Tools for PB -> SAT translation

minisat+ input format

borg-pb

clasp:

SAT4J:

BoolVar/PB

File QBF.hpp

Finding sources

Duaffle

MiniQbf

File Quadratics.hpp
count_quadintsol
File QuineMcCluskey.hpp

Connections

Specify the order of the output-clauses

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 compile-time

Improvements of the implementation

Parallelisation

Precise definitions, and basic types

File QuineMcCluskey.hpp
Computing all prime clauses for a full clause-set
File QuineMcCluskeySubsumptionHypergraph.hpp

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

File R.hpp

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 docus-page

Building dvi,pdf,info-documentation

File Rado.hpp

Connections

Basic functionality

Checking regularity

Known Rado numbers

File Ramsey.hpp

Ramsey hypergraphs

Generalised Ramsey hypergraphs

File Ramsey.hpp

Strengthen connection to Maxima/Lisp level

Move todos to this file

Write unit tests

Add generator to generate general Ramsey problems

Class Ramsey::Enumerate_hyperedges< Int >

See ComputerAlgebra/Hypergraphs/Lisp/Generators/plans/Ramsey.hpp

Update the underlying notion of "hypergraph"

Class Ramsey::Ramsey_TwoColours_1< Int >
Use components from module InputOutput.
File Ramsey_2_3_10.hpp

General information

Using DPLL and Conflict driven solvers

File Ramsey_2_4_4.hpp

General information

Using DPLL and conflict-driven solvers

File Ramsey_2_4_6.hpp

General information

Using DPLL and Conflict driven solvers

File Ramsey_2_5_5.hpp

General information

Using DPLL and Conflict driven solvers

Using UBCSAT

File RamseyProblems.hpp

MG must completely update this file!

Create a systematic naming scheme

Implement the general (i.e., non-diagonal) 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 Ramsey-symmetries of the clause-set

Symmetry breaking by recursive application of pigeonhole principle

Considering only labellings with bounded number of particular colours

Reimplement "Symmetry breaking by using %Ramsey-symmetries of the clause-set"

Generators for all standard Ramsey problems

File RamseyTheory.hpp

Software by Pascal Schweitzer

Software by Aaron Robertson

File RandomClauseSets.hpp

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

File RandomGraphs.hpp

Implementation

Overview on theoretical possibilities

File RandomShuffleDimacs.cpp
Move CLSAdaptorRandomShuffle
File range_type.hpp
Where is this needed??
File RankPrimes.hpp

Connections

Create application test

Create unit tests

Enhance the table

Better error codes

Write wrapper script

Use Messages

Improved usage of Gmp-facilities

Better algorithms

File RBases.hpp

Relations to other parts

Organisation

The notion of a base of a clause-set relative to some reduction

Considering special reductions

Application to the representation of boolean functions

Sampling of r-bases

Computing minimum r-bases

File README.hpp

Preprocessing

Creating an html-version

File RecogniseRandomFormulas.hpp
First tool
File RecursiveDirectoryIteration_Tests.hpp
There is now a recursive directory-iterator in boost!
File ReductionBasedRepresentations.hpp

Connections

r-based clause-sets

Positive representations

File Reductions.hpp

Implement the reductions from the Kullmann/Luckhardt-preprints.

Implement bounded resolution.

All kinds of binary-clause reasoning are handled by module FailedLiteralReduction, or?

Member Reduktion1 (void)
It should be unsigned char.
Member Reduktion2 (void)
It should be unsigned char.
File RefactoringIncludeHandling.hpp

Write doxygen-documentation for Concepts::IncludeDirective.

Transfer the tests to the new test system.

The whole approach needs to be thought over.

File ReingoldTilford.hpp

Create milestones

Reingold-Tilford algorithm at abstract level

The full Reingold-Tilford algorithm

Reingold-Tilford algorithm in Maxima.

File RelationTests.hpp

Implement (similar to TestReflexivity) tests for:

  • partial order (quasi-order, antisymmetric)
  • linear order (partial order, total)
  • strict order (irreflexiv, transitiv)
  • strict total order (strict order, trichotomy)
  • strict total order with equivalence ("strict weak ordering" in the language of the C++ standard) (strict total order, the induced similarity relation x ~ y <=> not (x < y) and not (y < x) is an equivalence relation).

Implement tests for

  • R' is the complement of R
  • R' is the inverse of R
  • R = R'.

Implement the following induced relations (in module OrderRelations)

  • given a quasi-order R, the canonical equivalence E is x E y <=> x R y and y R x
  • given a strict order R, the associated partial order P is x P y <=> x R y or x == y
  • given a strict order R, the induced similarity relation S is x S y <=> not (x < y) and not (y < x)
  • given a strict order R, the associated total quasi-order Q is x Q y <=> x R y or x S y.

Improve the tests (so that they become more meaningful).

File RelationTests_Tests.hpp
TestQuasiorder should use Test_TestEquivalence which in turn uses Test_TestReflexivity !
File Release.hpp

Developers

Release plan

ExternalSources repository

Special tag

Improved releases

File Renaming.hpp
ReplaceStrings
File Representations.hpp
tree2pruefercode_og
File ResolutionClosure.hpp
Primimplicates via resolution
File ResolutionComplexity.hpp

Finding hard unsatisfiable hitting clause-sets

Hardness

File ResultElements.hpp

To be completed (see module SATCompetition, and there mainly SATCompetition/SingleResult.hpp).

Once sub-directories of modules are fully supported, these concepts should go to Concepts/CompetitionEvaluation.

File ResultElements_Tests.hpp
Once the concepts in Concepts/ResultElements.hpp have been extended, they need to be tested.
File ResultProcessing.hpp
Yet the types ResultNode etc. are hard-coded --- they should become parameters.
File Rijndael.hpp

Expand docus

Migrate the mupad-code.

Terminology (DONE Moved to ComputerAlgebra/Cryptology/docus/Rijndael.hpp)

File rijndael.hpp

Proper testing!

With C++09 stdint.h likely is to be replaced by cstdint.

File Rijndael.hpp
Axiom: design and implementation
File Rijndael.hpp

Connections

Overview

First tests AES

Further tests

File RoundColumn_2_4.hpp

Problem specification

Naming

Basic data

Minimum representations using weighted MaxSAT : mincl_rinf <= 396

r_1-bases : mincl_r1 <= 2712

File RProcessSplitViaOKsolver.hpp
Basic prototype
File RUcpGen.cpp
Update application tests
File RunningReportMG.hpp

Fix binary cardinality constraints lemmas

Add lemmas and definitions for *all* "non-clashing" matrices results

Tidy "non-clashing matrices" lemmas

Define target(s) for PhD

Update "Clause-set 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

Write-up 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

File RunningReportML.hpp

Using homomorphisms in resolution proofs

Relating isomorphisms of clause-sets with isomorphisms of graphs

Relations to graph theory

Bicliques

Biclique partitions

File RunTest.hpp
Transition
File RunTest_Declarations.hpp
Create a concept for TestSystem::RunTest.
File SafeReading.hpp

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.

File Sage.hpp
DONE (now using 4.7.1) Update to newer Sage
File Sampling.hpp

Uniformly sampling biclique partitions

Random processes

File Sampling.hpp

Sampling maximal vertex-bicliques

Sampling maximal edge-bicliques

File SAT.hpp

Parallel SAT solvers

SAT solvers

(P)Lingeling

Install Relsat

Improvements of CryptoMiniSat

Add todos for SAT-Race 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

C-Sat

Posit

Answer set programming

Generators

Symmetries

Maxsat

Counting

DONE (no need to do something here; the number of unit-propagations is not interesting, and the extraction tools shall just return 0 for numbers of conflicts etc.) Correct solvers with poor handling of trivial CNFs

File SATCompetition.hpp

Update and completion of plans regarding SAT 2011

Benchmarks for SAT 2012

Categories / "tracks" for SAT 2011

File SatisfactionProblems.hpp

Variables

Value set

Total assignments

Domain association and allowed total assignments

The notion of "condition"

Constructing conditions

Functions for conditions

Backdoors

File SatisfiabilityPrediction.hpp

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 inclusion-exclusion

Experimentation

Counting falsifying assignment

File SATSolving.hpp

Connections

Statistics on the performance of SAT solvers

File Sbox_1.hpp

Basic data

Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 67)

1-base : mincl_r1 <= 124

Move Sbox-1-specific investigations here

File Sbox_2.hpp

Basic data

Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 67)

1-base : mincl_r1 <= 129

Move Sbox-1-specific investigations here

File Sbox_3.hpp

Basic data

Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 68)

1-base : mincl_r1 <= 138

Move Sbox-1-specific investigations here

File Sbox_4.hpp

Basic data

Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 69)

1-base : mincl_r1 <= 128

Move Sbox-1-specific investigations here

File Sbox_4.hpp

Basic data

Overview

Combining Sbox with field addition

Generating all minimum representations via hypergraph transversals

File Sbox_5.hpp

Basic data

Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 67)

1-base : mincl_r1 <= 134

Move Sbox-1-specific investigations here

File Sbox_6.hpp

Basic data

Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 66)

1-base : mincl_r1 <= 136

Move Sbox-1-specific investigations here

File Sbox_7.hpp

Basic data

Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 67)

1-base : mincl_r1 <= 123

Move Sbox-1-specific investigations here

File Sbox_8.hpp

Basic data

Overview

Move individual investigations to sub-modules

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_1-bases : mincl_r1 <= 4398

Generate good CNF hitting clause-sets

Analysing the AES prime implicates

Extracting prime implicate representations from the hitting-cls-representations

Find the symmetries of the AES Sbox DNF

File Sbox_8.hpp

Basic data

Using weighted MaxSAT to compute small CNFs (mincl_rinf <= 69)

1-base : mincl_r1 <= 152

Move Sbox-1-specific investigations here

File SboxAnalysis.hpp

Connections

Add decomposed Sbox operations

Representations of the Sbox using additional variables

Other software systems offering Sbox translations

File Schur_BHR.cpp

Rename to WSchur_BHR.cpp<p>Create complete specifications

Write modification to handle ordinary Schur-problems

File Scoring_Tests.hpp
Write basic tests.
File Search.hpp

Finding short tree-resolution proofs

Regular-resolution complexity

How to compute the minimal DP-resolution complexity?

Resolution complexity

2-CNF

Finding short resolution proofs via SAT

File Search.hpp
Connections
File Search.hpp

The role of maximal bicliques

Finding interesting biclique partitions

File SecondOrderTestTools.hpp
With C++09 stdint.h likely is to be replaced by cstdint.
File SelfDuality.hpp
Smallest self-dual but not self-polar matrix
File SelfOrthogonal.hpp

Searching pandiagonal latin squares

SAT translations

Further properties

File SequenceOperations.hpp
Moving Sum_sizes fully to the range concept (accepting only ranges as input)
File SequenceOperations_Tests.hpp
Completing Test_Sum_sizes:
  • using boost::assign (and a general loop)
  • more test cases.
File Sequences.hpp

deharmonise_eval_2

Transformations

File SetSystems.hpp

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 set-systems

File SetUp.hpp
Further actions by the setup-process:
File SimpleGraphGames.hpp

Connections

The general setting

Implementing the recursive algorithm according to [AB, Moller]

File SimpleParallelisation.hpp

Connections

More information on the splittings

The order of the md5sum-computation (SplittingViaOKsolver)

Script for applying partial assignments

Improving SplittingViaOKsolver

Good splitting

Computing a splitting tree

Distributing the tasks to machines

File SingleResult.hpp
Writing doxygen comments for all classes in here.
File SingularDP.hpp

Are non-1-singular tuples totally singular?

Special properties of the greedoid of singular sets

File SmallScaleAdvancedEncryptionStandard.hpp

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

File Smusat_Horn.cpp

Write application tests

Improving speed

File SnowCress2000Analysis.hpp

Create milestones.

Links

File SolversPdVdw.hpp

Performance of Satz

Performance of OKsolver-2002

Performance of march_pl

minisat-2.2.0

glucose-2.2

cryptominisat 296

precosat-570

lingelingala-b02aa1a-121013

Cube-and-Conquer (SplittingViaOKsolver)

File SolversVdw.hpp

Performance of OKsolver-2002

Performance of march_pl

Performance of satz215

Performance of conflict-driven solvers

SplittingViaOKsolver

File SortByClauseLength.cpp

Move CLSAdaptorSortByClauseLength

Move AllEqual to OrderConstructions

File SortByClauseLengthDescending.cpp

Merge with SortByClauseLength.cpp

DONE Add application tests

File SplittingTrees.hpp

Connections

Write tests

optimal_splitting_tree and optimal_r_splitting_tree

Processing splitting trees

optimal_r_splitting_tree

File SplittingViaOKsolver.hpp

Direct encoding

Direct encoding and full symmetry breaking

Palindromic problem (direct encoding)

Palindromic problem with full symmetry-breaking (direct encoding)

Weak palindromic problem with full symmetry-breaking (direct encoding)

File Statistics.hpp

Comprehensive statistics

Further statistics

Naming

File Statistics.hpp
These things (and more) should be part of the general hypergraph library (which must be directly applicable to clause-sets).
File Statistics.hpp
Vertex degrees
File std_Basics.hpp
Complete doxygen-documentation.
File std_Basics_Tests.hpp
Complete the implementations.
File std_Container.hpp
Write the other concepts from the standard.
File std_Container_Tests.hpp

The only test available yet, Test_ContainerConcept, actually is a meta-test (testing the concept), so this should go (with the new test system, and once arbitrary directory-nesting is avaiable) to Concepts/tests/tests.

Write tests for Concepts::Container.

File std_Iterators.hpp
Write concepts for
  • OutputIterator
  • BidirectionalIterator
  • RandomAccessIterator.
File std_Iterators_Tests.hpp
Write the test functions:
  • InputIterator has only one exploitable (additional) semantical property (besides the properties of ConstructibleCAEq), namely that if i == j for iterators i,j and (i,j) is in the domain of == (which can be empty), where i, j are dereferencable, that then i and *j are substitution-equivalent. (Note that a model of InputIterator in general is not a model of EqualitySubstitutable.) If value_type is a model is EqualityComparable, then we have (i == j, (i,j) in the domain of == and i, j dereferencable => *i == *j), and this should be put into an axiom. Note: It seems to be possible, that although == is syntactically allowed, application always leads to undefined behaviour.
  • For MultiPassInputIterator we have EqualitySubstitutable and thus i == j and i, j dereferencable implies ++i == ++j.
  • ForwardIterator has default constructors, and i == j iff either i, j are not dereferencable or both are dereferencable and *i is the same object as *j (this is stronger than *i == *j). The domain of == is total (note, that there is no such thing as a "valid iterator": If ++ or is applied on non-dereferencable iterators, then the result is undefined in general, and thus the whole program is broken).
  • BidirectionalIterator: additionally --++i == i and ++--i == i (the latter not in the standard?)
  • RandomAccessIterator: "i+n" has the same meaning as operation ++ applied n-times to i (and so on). Furthermore we have LinearOrder.
File StraightLinePrograms.hpp

The notion of a "straight-line program"

The notion of a "boolean circuit"

Other translations (than the Tseitin translation)

File StringHandling.hpp
How much should be replaced by Boost components?!
File StrongColouring.hpp

InjectivityConstraints:

Graph colouring conversion

File SubClauseSets.hpp

Update namespace

Create milestones

General algorithm

File Subsets.hpp

Concepts

Organisation and connections

Algorithmic framework

Refinements

File Subsets.hpp

Connections

Iteration through lexicographical order

Improving colexicographical unranking

Enumerating all k-subsets in Gray-code manner

File Substitutions.hpp

The notion of a "literal substitution":

standardise_fcs

File Subsumption.hpp

Move todos

Better algorithms

File SubsumptionHypergraph.hpp

Improve code quality

Organisation

More unit tests

File SubsumptionHypergraph.hpp

Test performance of Subsumption_Hypergraph generator

Offering live subsumption hypergraph generation

File Sudoku.hpp

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

File Sudoku.hpp

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 Sudoku-solvers.

Visualisation of the runs of solvers

File SupportTotalAssignments.hpp

Concepts:

Design and implement

File SymmetricGroups.hpp

Implementations

Acronyms

Computing powers, based on the cycle representation

File Symmetry.hpp

Automorphisms

Full symmetry-breaking

Embedding colour-symmetry-breaking into the search

Enumerating all solutions without colour-symmetry-repetition

Relations between palindromic hypergraphs

Vertex degrees and their distributions

File SymmetryBreaking.hpp

Handling symmetries using extended resolution

Performance of symmetry breaking by fixing monochromatic cliques

Using cardinality constraints

File TableauAlgorithm.hpp
find_aut_tableau_cl
File TargetSpecifications.hpp

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 "new-module"

File TauMethod.hpp

Connections

Efficient computation of the tau-function:

Experimentation

Decision

Theory

File TawSolverPdVdw.hpp

Versions before version 2.0

Towards version 2.0

Version 2.0 and later

With tau-projection

Performance evaluation

File TawSolverVdw.hpp

Version 1.0

From version 1.0 to the version before the improved heuristics

Improving the heuristics (and the implementation)

With tau-projection

Performance evaluation

File TenChallenges.hpp
Baltimore conference
File TestBaseClass.hpp
Improve the include list: Make clear what are library files, and what is to be tested.
File TestBaseClass.hpp

TestSystem::TestBase

Unknown exceptions

Encapsulation

Testing

Transition

File TestExceptions.hpp

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 error-information

Test TestSystem::messages::ErrorDescription

OKLIB_TEST_RETHROW_NO_LOG

Transition

Overhaul of the test-macros (like OKLIB_TEST_EQUAL) seems to be needed

File TestExecutionTools.hpp

Update

  • doxygen documentation
  • new plans files, transferring todos

New test system

File TestFondement.hpp
Once the old test system has been removed, check whether all links in the doxygen documentation are correct.
File TestProgram.hpp

Messages

Infos

ProgramOptions

Transition

File TestSATCompetition.cpp
Tests reading files belong to the enhanced tests.
File Thresholds.hpp

General threshold functions

Cardinality constraints

The basic symmetric functions

File TimeAndDate.hpp

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 day-number and week-number) 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.)

File TimeHandling.hpp

Functions currentDateTime should go to module Messages.

Which components should be replaced by components from Boost ?!

Class TimeHandling::SystemTime
It is actually not clear whether boost::timer is specified to be the *system* time?! Send an e-mail to the Boost mailing list.
File TimeSeriesAnalysis.hpp

Counting falsifying assignments found

Alternative sampling

Using the predictions

Software components

File Tools.hpp

Improving CRunPdVdWk1k2

Script for searching for a vdW-number

Version of RunVdW3k for palindromic problems

File traits.hpp

Submodules

Test all metafunctions.

File traits.hpp
For this kind of files we should also have some test process.
File Transformations.hpp

Hypergraph transformations I

Hypergraph transformations Ib

Hypergraph transformations II

File Transformations.hpp

Parameters for encoding

Edge-centered SAT encoding

Vertex-centred SAT encoding

Transformations

File Transformations.hpp
Translations to MUSAT
File Translations.hpp

Basic translation

Translation to SAT according to Liffiton and Sakallah

File Translations.hpp

Simplify AES translation

Handling external data

Order of small scale matrix dimensions

Rewrite ncl_list_ss correctly

Remove AES-specific translation

Complete small scale helper functions

Standardise output files names

How to represent elements of arbitrary fields as boolean variables?

Provide additional translation into CSP-solver format

Write docus

Generate translation that allows multiple plaintext/ciphertext pairs

File Translations.hpp

Translations reducing the lengths of clauses

Translations reducing the number of variable-occurrences

File Translations.hpp
General idea
File Translations.hpp

Standard "box" translations

The canonical box translation

The 1-base box translation

The "minimum" box translation:

File Translations.hpp

Standard "box" translations

The canonical box translation

The 1-base box translation

The "minimum" box translation:

File TreeResolution.hpp

Tree-resolution complexity

Tree-resolution refutations found by simple algorithms

Developing a formula (now for the numbers of leaves)

Short proofs with the hitting proof-system

File Trees.hpp

Create milestones.

Investigate existing software

Reingold-Tilford algorithm outline

Four aesthetic criterions for Reingold-Tilford algorithm

Environment

Applications

File TrivialAtomicConditions.hpp
Test AC_bool semantically.
File TrivialLiterals.hpp
Update namespaces.
File TseitinTransformation.hpp
Connections
File TseitinTranslation.hpp

Connections to other modules

Implementing the Tseitin-transformation (with variations)

Horn specialities

Translations to CNF/DNF

Reorganisation

Optimisation

File TseitinTranslation.hpp

Renaming the file to "CanonicalTranslation.mac"

Add statistics

Translation of boolean circuits into boolean CNF-clause-sets

Understanding dualts_fcl

Strengthening dualts_fcl by adding some redundant clauses

File TuringMachines.hpp

Turing machines: general plans

Types of Turing machines

File TypeTraits.hpp
It seems we should guarantee that this file includes <boost/type_traits.hpp> ?!
File TypeTraits_Tests.hpp
Tests for metafunction is_std_container and has_size_function.
File Ubcsat-okl.hpp

More readable large numbers

Better output

File Ubcsat.hpp

Update to version 1.2.0

Make clear the required package for dos2unix

File UcpBase.hpp

Computing r_1-bases for a set of prime implicates

Random r_1-bases

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 unit-tests for Bases/RUcpBase.cpp

Create unit-tests for Bases/RUcpGen.cpp

File uhit_def.hpp

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 data-sets

Reduction by 2-subsumption resolution

File UnaryAddition.hpp

Boolean functions representing unary addition

CNF and DNF representations of unary addition

Smallest prime CNF-representation

Smallest r_1-based CNF-representation without new variables

Smallest r_2-based CNF-representation without new variables

File UnitClausePropagation.hpp

Better names

Improve efficiency of UnitClausePropagation(W).cpp

File UnitClausePropagation.hpp

Connections

The most basic form of UCP

File UnitClausePropagationW.cpp
Write application tests : DONE
File UnitPropagation.hpp
Update namespaces
Member UnitPropagation::unit_propagation_improved (const Cls &F, typename Cls::Pass &phi)
Make the underlying concepts explicit
Member UnitPropagation::unit_propagation_simple (Cls &F)
Make the concept for Cls explicit
File UpperBounds.hpp
Partitionings of processes
File UsingPB.hpp
Using minisat+
File UsingSAT.hpp

Translation via addition

Look-ahead solvers with translation via addition

Conflict-driven solvers with translation via addition

Local search solvers with translation via addition

Using CSP solvers

File UsingSAT.hpp

General plans

Performance of Minisat

Performance of OKsolver-2002

File UsingSubProblems.hpp

Relations to preprocessing

Considering diagonal (boolean) problems and full representations

Finding interesting inferences

File Valgrind.hpp

Install version 3.6.0 : DONE

Update

File VanderWaerden.hpp

Connections

Create tests

Checking certificates

File VanderWaerden.hpp

Connections

Update

Speed of PdVanderWaerdenCNF.cpp

File VanderWaerden.hpp

palindromise_vdw_ohg

DONE (now the implementation is non-recursive, and in case more memory is needed, use default_memory_ecl()) Hypergraphs of arithmetic progressions

File VanderWaerden.hpp

DONE Transfer Applications/RamseyTheory/plans/Van_der_Waerden_hypergraph.hpp to here

Generator

DONE Update namespace usage

New test system

Update

File VanderWaerden_3-3-3-k.hpp

Literature overview

vanderwaerden_3(3,3,3) = 27

vanderwaerden_3(3,3,4) = 51

vanderwaerden_3(3,3,5) = 80

File VanderWaerden_3-3-4-k.hpp

Overview

vanderwaerden_3(3,4,4) = 89

File VanderWaerden_3-4-4-4.hpp

Known from the literature

vdw_3(4,4,4) > 150

File VanderWaerden_4-3-3-3-3.hpp

Creating instances

vanderwaerden_3(3,3,3)

OKsolver_2002

march_pl

satz215

Minisat

The behaviour of m -> vanderwaerdend(m,3)

File VanderWaerdenCNF.cpp
Update needed
File VanderWaerdenCNF.hpp
Use InputOutput::CLSAdaptorDIMACSOutput
File VanderWaerdenProblems.hpp

Connections

Organisation : DONE

Standardisation

Statistics

Systematic output and output-functions

Palindromic versions with arithmetic progressions of length 3

Alternative handling of parameter-values 2

DONE More than two parts

Symmetry breaking for vdW-problems

File var.hpp

Update namespaces.

For the future perhaps we should use a call traits instead of the fixed argument type const L& ?

File Variables.hpp

Complete doxygen-documentation.

Transfer tests to the new test system.

Complete VariablesAsIndex_basic_test by applying tests:

  • Concepts::VariablesWithIndex_Axiom_index_nonnegative
  • Concepts::VariablesWithIndex_Axiom_index_zero_negative
  • Concepts::VariablesWithIndex_Axiom_index_identity<p>Is a generalisation of the Variables-concept useful, where there is no default constructor, and no handling of singular values? (Perhaps with the name "GeneralIndex" ?)

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 implementation-defined (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 clause-sets 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).

File Variables_Tests.hpp
Perhaps within namespace Concepts::tests we have namespace Variables? And further differentiations are conceivable, corresponding to the refinements?
File Visualisation.hpp

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

File WatchedLiterals.hpp
Basic concepts
File XMLHandling.hpp
What to do with this?