1package solver23// A Result is a status, either Sat, Unsat or Indet.4// If the status is Sat, the Result also associates a ModelMap with an integer value.5// This value is typically used in optimization processes.6// If the weight is 0, that means all constraints could be solved.7// By definition, in decision problems, the cost will always be 0.8type Result struct {9 Status Status10 Model []bool11 Weight int12}1314// Interface is any type implementing a solver.15// The basic Solver defined in this package implements it.16// Any solver that uses the basic solver to solve more complex problems17// (MAXSAT, MUS extraction, etc.) can implement it, too.18type Interface interface {19 // Optimal solves or optimizes the problem and returns the best result.20 // If the results chan is non nil, it will write the associated model each time one is found.21 // It will stop as soon as a model of cost 0 is found, or the problem is not satisfiable anymore.22 // The last satisfying model, if any, will be returned with the Sat status.23 // If no model at all could be found, the Unsat status will be returned.24 // If the solver prematurely stopped, the Indet status will be returned.25 // If data is sent to stop, the method may stop prematurely.26 // In any case, results will be closed before the function returns.27 // NOTE: data sent on stop may be ignored by an implementation.28 Optimal(results chan Result, stop chan struct{}) Result29 // Enumerate returns the number of models for the problem.30 // If the models chan is non nil, it will write the associated model each time one is found.31 // If data is sent to stop, the method may stop prematurely.32 // In any case, models will be closed before the function returns.33 // NOTE: data sent on stop may be ignored by an implementation.34 Enumerate(models chan []bool, stop chan struct{}) int35}