1/*2Package solver gives access to a simple SAT and pseudo-boolean solver.3Its input can be either a DIMACS CNF file, a PBS file or a solver.Problem object,4containing the set of clauses to be solved. In the last case,5the problem can be either a set of propositional clauses,6or a set of pseudo-boolean constraints.78No matter the input format,9the solver.Solver will then solve the problem and indicate whether the problem is10satisfiable or not. In the former case, it will be able to provide a model, i.e a set of bindings11for all variables that makes the problem true.1213# Describing a problem1415A problem can be described in several ways:16171. parse a DIMACS stream (io.Reader). If the io.Reader produces the following content:1819 p cnf 6 720 1 2 3 021 4 5 6 022 -1 -4 023 -2 -5 024 -3 -6 025 -1 -3 026 -4 -6 02728the programmer can create the Problem by doing:2930 pb, err := solver.ParseCNF(f)31322. create the equivalent list of list of literals. The problem above can be created programatically this way:3334 clauses := [][]int{35 []int{1, 2, 3},36 []int{4, 5, 6},37 []int{-1, -4},38 []int{-2, -5},39 []int{-3, -6},40 []int{-1, -3},41 []int{-4, -6},42 }43 pb := solver.ParseSlice(clauses)44453. create a list of cardinality constraints (CardConstr), if the problem to be solved is better represented this way.46For instance, the problem stating that at least two literals must be true among the literals 1, 2, 3 and 4 could be described as a set of clauses:4748 clauses := [][]int{49 []int{1, 2, 3},50 []int{2, 3, 4},51 []int{1, 2, 4},52 []int{1, 3, 4},53 }54 pb := solver.ParseSlice(clauses)5556The number of clauses necessary to describe such a constrain can grow exponentially. Alternatively, it is possible to describe the same this way:5758 constrs := []CardConstr{59 {Lits: []int{1, 2, 3, 4}, AtLeast: 2},60 }61 pb := solver.ParseCardConstrs(clauses)6263Note that a propositional clause has an implicit cardinality constraint of 1, since at least one of its literals must be true.64654. parse a PBS stream (io.Reader). If the io.Reader contains the following problem:6667 2 ~x1 +1 x2 +1 x3 >= 3 ;6869the programmer can create the Problem by doing:7071 pb, err := solver.ParsePBS(f)72735. create a list of PBConstr. For instance, the following set of one PBConstrs will generate the same problem as above:7475 constrs := []PBConstr{GtEq([]int{1, 2, 3}, []int{2, 1, 1}, 3)}76 pb := solver.ParsePBConstrs(constrs)7778# Solving a problem7980To solve a problem, one simply creates a solver with said problem.81The solve() method then solves the problem and returns the corresponding status: Sat or Unsat.8283 s := solver.New(pb)84 status := s.Solve()8586If the status was Sat, the programmer can ask for a model, i.e an assignment that makes all the clauses of the problem true:8788 m := s.Model()8990For the above problem, the status will be Sat and the model can be {false, true, false, true, false, false}.9192Alternatively, one can display on stdout the result and model (if any):9394 s.OutputModel()9596For the above problem described in the DIMACS format, the output can be:9798 SATISFIABLE99 -1 2 -3 4 -5 -6100*/101package solver