Add basic python sat interface

[hbierlee]

Just getting started on this, making a draft pull request to get CI. No reviews required for the moment.

[codecov]

Codecov Report

Attention: Patch coverage is 0% with 13 lines in your changes missing coverage. Please review.

Project coverage is 71.95%. Comparing base (acd50ae) to head (28a1816).

Files with missing lines	Patch %	Lines
crates/pyndakaas/src/lib.rs	0.00%	13 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop      #86      +/-   ##
===========================================
- Coverage    72.07%   71.95%   -0.12%     
===========================================
  Files           20       20              
  Lines         7377     7389      +12     
  Branches      7377     7389      +12     
===========================================
  Hits          5317     5317              
- Misses        1933     1945      +12     
  Partials       127      127              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[hbierlee]

Summarizing the ideas and todos from today's meeting with Jip/Henk:

The encode functionality design

• Change special linear encoding function cnf.add_linear([a,b,c], coefficients=[2,3,5], comparator=pk.Comparator.LessEq, k=6, encoder=PbEnc.Pairwise()) to generic Constraint object encoder using cnf += Constraint(..)
  • Paves the way for overloaded Constraints: cnf += ((2a) + (3b) + (5*c) <= 6)
  • Also needed to epand to integer interface
• To support different encoders, use builder pattern e.g. cnf.with_encoder(Pairwise)
  • Expose our encoders + StaticEncoder (e.g. StaticEncoder(Pairwise, Adder, Adder) as default), return exception if unable to encode
    • Encoder type something like encode -> Result<(), Err<Unsat/Unsupported>
  • In the future, allow the user to create their own encoders for custom strategies

    class OurEncoder(Encoder):
        encode(con): # receives con post-aggregation
            if con == AMO:
                ...

Small formula changes

• abs -> var (of x.var()) (slight chance we do not need this at all since you're doing introspection which we would like to avoid)
• Ensure we allow Lit -> integer, but not integer -> Lit

Exposing "traits" using proc-macro'd abstract base class (ABC) implementations

• Trait exposure doesn't really work and there is no pyo3 ABC support. Instead, we'll have to support this ourselves using this structure:
  • Note: all subclasses of ClauseDatabase(ABC) (e.g. CNF) need to have python methods for the abstract functions; probably best to proc-macro those

  class ClauseDatabase(ABC):
      def add_clause(self, cls):
          raise Exception("I'm abstract")

        def new_var_range(self, cls, len):
            raise Exception("I'm abstract")

        ...

  class Solver(ClauseDatabase):
      def add_clause(self, cls):
          raise Exception("I'm abstract")

        def new_var_range(self, cls, len):
            raise Exception("I'm abstract")
           
  class Cnf(ClauseDatabase): # macro' pyo3 pythonmethod
      def new_var_range(self, clause):
        # rust: self.0.new_var_range ...


  class Cadical(Solver): # macro' pyo3 pythonmethod
      def new_var_range(self, clause):
        # rust: self.0.new_var_range ...

• Note we can handle the ClauseDatabaseTools extensions similarly:

# macro'd by ClauseDatabase
def add_var(self):
    self.0.add_var(..)

• with_conditions should use a context (somehow) (with cnf.with_conditions([p]) as ccnf: ...)

Solving and solve results

• Change current solver.solve() is True # Return True (SAT), False (UNSAT), None (UNKNOWN) to return an SolveResult
• Idea to let it implement __bool__
• Result.value(a) returns Unsatisfiable if it is
• Currently, we have the technical issuethat pyo3 cannot do lifetimes in classes; hopefully we can find a better solution than copying the full copy the solver ..?

Other TODOs not yet started / discussed:

• timeouts: solver.solve(time_limit=datetime.duration(10))
• all solutions iterator; for sol in solver.solutions(): (somehow as generator)
• pip install with optional features, e.g. pip install pindakaas[cadical,kissat]