ctlab / fbsat Goto Github PK

Eliminate duplicated code with cardinality constraints. Possible solution is a Cardinality class, which stores a totalizer and manages the comparator updates.

Implement synthesis of modular automata with various models of connectivity:

• parallel
• sequential
• arbitrary

For now, we only focus on scenarios-only synthesis ("Basic" and "Extended" methods), leaving out the negative scenarios support ("Complete" method) for modular synthesis. But nothing stops us from supporting modular CEGIS in the future.

Add dockerfile to allow using fbSAT via Docker.

Implement a convenient data structure for SAT variables storage, similar to MultiArray (precisely, IntMultiArray), but specifically for boolean/integer variables, including automatic encoding of ExactlyOne constraints for "integer" variables.

We need to migrate from Travis, because it has changed its policy about OSS builds: https://blog.travis-ci.com/2020-11-02-travis-ci-new-billing. Github Actions seem to be a pretty decent replacement nowadays.

Currently, the code inside BinaryAlgorithm::toST(...) has a bug in it - when the algorithm is T->T, F->F (z := z), it is erroneously displayed as z := NOT z.

The correct behavior is to display such algorithms as z := z or, as we convert to ST, not to display them at all, as z := z is a no-op.