robbiemckinstry / acheron Goto Github PK

No need for anything to be behind an Arc pointer right now, since everything is expected to be single-threaded for the foreseeable future.

Blocked unitl I read more about CDCL and whether a priority heap is needed.

The dequeue in the solver should be replaced with a heap. In practice, we want to be able to order the operations to behave like a stack in some cases and a queue in others. We may also want to insert items into the middle of the queue, though I'm not sure we have a reason for that.

For DPLL, we may be able to get away with using push_front for unit propagation and pure literal elimination and push_back for splitting (to ensure we're moving through the search space in a depth-first manner, allowing reference-counted formulas to be freed. However, this approach feels fairly limiting w.r.t. parallelism, where we want multiple workers pulling from the queue at a time.

We should be running cargo make in CI to verify build correctness.

This "Diagnostics" subsystem should log operations as they are performed, and also generate Termination Trees using graphviz

Check the Handbook for definition of allowed statuses.

Clause keeps a "status" literal to cache whether its been satisfied or not. This makes the code harder to read, and it doesn't really provide any algorithmic benefits over using purely functional im::vectors. We should discard it as well as any related methods.

I believe the Resolution OpCode is misnamed. "Resolution" is specific to CDCL, and splitting is the term I'm looking for w.r.t. DPLL.

Not 100% sure about this. Confirm in the Handbook of Satisfiability first.

JobOutput, Job, and History store a copy of the Formula. We should decide on one location or the other for this.

Look through the Rustdocs to see if the API makes sense.

OpCode should be replaced with an AuditEntry which defines the list of operations applied. (I think CDCL uses something like this, so confirm whether the term is already well-defined before sticking with the name "AuditEntry").

We should also have an Operator trait, which modifies the formula and creates a new Frame. The Operator needs to be an object-safe trait since we may store it on the solver's DeQueue for operations like unit propagation and pure literal elimination.

Unify this vision with that of the Frame type.

Lint violations have crept in since I last worked on this project. This issue is to get linting clean.

These types should implement a custom(?) iterator that wraps a Vector's iterator.

The Core package has abysmal test coverage. We should cover a number of smoke tests, plus unit tests for Conditioning variables.

I'm aware of a few bugs in DIMACS parsing which result in empty clauses where none should be. This is probably caused by parsing empty lines, or lines with whitespace in them accidentally. I believe the DIMACS format does not allow empty clauses since that would not be valid CNF.

Clause::Display impl has a trailing comma at the end. This can be fixed with a test and using a "Join" function for strings.

There are a couple of places with "random" operations, which we should remove with a deterministic operation instead.