1package solver23import (4 "bufio"5 "fmt"6 "io"7 "strconv"8 "strings"9)1011// ParseCardConstrs parses the given cardinality constraints.12// Will panic if a zero value appears in the literals.13func ParseCardConstrs(constrs []CardConstr) *Problem {14 var pb Problem15 for _, constr := range constrs {16 card := constr.AtLeast17 if card <= 0 { // Clause is trivially SAT, ignore18 continue19 }20 if len(constr.Lits) < card { // Clause cannot be satsfied21 pb.Status = Unsat22 return &pb23 }24 if len(constr.Lits) == card { // All lits must be true25 for i := range constr.Lits {26 if constr.Lits[i] == 0 {27 panic("literal 0 found in clause")28 }29 lit := IntToLit(int32(constr.Lits[i]))30 v := lit.Var()31 if int(v) >= pb.NbVars {32 pb.NbVars = int(v) + 133 }34 pb.Units = append(pb.Units, lit)35 }36 } else {37 lits := make([]Lit, len(constr.Lits))38 for j, val := range constr.Lits {39 if val == 0 {40 panic("literal 0 found in clause")41 }42 lits[j] = IntToLit(int32(val))43 if v := int(lits[j].Var()); v >= pb.NbVars {44 pb.NbVars = v + 145 }46 }47 pb.Clauses = append(pb.Clauses, NewCardClause(lits, card))48 }49 }50 pb.Model = make([]decLevel, pb.NbVars)51 for _, unit := range pb.Units {52 v := unit.Var()53 if pb.Model[v] == 0 {54 if unit.IsPositive() {55 pb.Model[v] = 156 } else {57 pb.Model[v] = -158 }59 } else if pb.Model[v] > 0 != unit.IsPositive() {60 pb.Status = Unsat61 return &pb62 }63 }64 pb.simplifyCard()65 return &pb66}6768func (pb *Problem) appendClause(constr PBConstr) {69 lits := make([]Lit, len(constr.Lits))70 for j, val := range constr.Lits {71 lits[j] = IntToLit(int32(val))72 }73 pb.Clauses = append(pb.Clauses, NewPBClause(lits, constr.Weights, constr.AtLeast))74}7576// ParsePBConstrs parses and returns a PB problem from PBConstr values.77func ParsePBConstrs(constrs []PBConstr) *Problem {78 var pb Problem79 for _, constr := range constrs {80 for i := range constr.Lits {81 lit := IntToLit(int32(constr.Lits[i]))82 v := lit.Var()83 if int(v) >= pb.NbVars {84 pb.NbVars = int(v) + 185 }86 }87 card := constr.AtLeast88 if card <= 0 { // Clause is trivially SAT, ignore89 continue90 }91 sumW := constr.WeightSum()92 if sumW < card { // Clause cannot be satsfied93 pb.Status = Unsat94 return &pb95 }96 if sumW == card { // All lits must be true97 for i := range constr.Lits {98 lit := IntToLit(int32(constr.Lits[i]))99 found := false100 for _, u := range pb.Units {101 if u == lit {102 found = true103 break104 }105 }106 if !found {107 pb.Units = append(pb.Units, lit)108 }109 }110 } else {111 pb.appendClause(constr)112 }113 }114 pb.Model = make([]decLevel, pb.NbVars)115 for _, unit := range pb.Units {116 v := unit.Var()117 if pb.Model[v] == 0 {118 if unit.IsPositive() {119 pb.Model[v] = 1120 } else {121 pb.Model[v] = -1122 }123 } else if pb.Model[v] > 0 != unit.IsPositive() {124 pb.Status = Unsat125 return &pb126 }127 }128 pb.simplifyPB()129 return &pb130}131132// parsePBOptim parses the "min:" instruction.133func (pb *Problem) parsePBOptim(fields []string, line string) error {134 weights, lits, err := pb.parseTerms(fields[1:], line)135 if err != nil {136 return err137 }138 pb.minLits = make([]Lit, len(lits))139 for i, lit := range lits {140 pb.minLits[i] = IntToLit(int32(lit))141 }142 pb.minWeights = weights143 return nil144}145146func (pb *Problem) parsePBLine(line string) error {147 if line[len(line)-1] != ';' {148 return fmt.Errorf("line %q does not end with semicolon", line)149 }150 fields := strings.Fields(line[:len(line)-1])151 if len(fields) == 0 {152 return fmt.Errorf("empty line in file")153 }154 if fields[0] == "min:" { // Optimization constraint155 return pb.parsePBOptim(fields, line)156 }157 return pb.parsePBConstrLine(fields, line)158}159160func (pb *Problem) parsePBConstrLine(fields []string, line string) error {161 if len(fields) < 3 {162 return fmt.Errorf("invalid syntax %q", line)163 }164 operator := fields[len(fields)-2]165 if operator != ">=" && operator != "=" {166 return fmt.Errorf("invalid operator %q in %q: expected \">=\" or \"=\"", operator, line)167 }168 rhs, err := strconv.Atoi(fields[len(fields)-1])169 if err != nil {170 return fmt.Errorf("invalid value %q in %q: %v", fields[len(fields)-1], line, err)171 }172 weights, lits, err := pb.parseTerms(fields[:len(fields)-2], line)173 if err != nil {174 return err175 }176 var constrs []PBConstr177 if operator == ">=" {178 constrs = []PBConstr{GtEq(lits, weights, rhs)}179 } else {180 constrs = Eq(lits, weights, rhs)181 }182 for _, constr := range constrs {183 card := constr.AtLeast184 sumW := constr.WeightSum()185 if sumW < card { // Clause cannot be satsfied186 pb.Status = Unsat187 return nil188 }189 if sumW == card { // All lits must be true190 for i := range constr.Lits {191 lit := IntToLit(int32(constr.Lits[i]))192 pb.Units = append(pb.Units, lit)193 }194 } else {195 lits := make([]Lit, len(constr.Lits))196 for j, val := range constr.Lits {197 lits[j] = IntToLit(int32(val))198 }199 pb.Clauses = append(pb.Clauses, NewPBClause(lits, constr.Weights, card))200 }201 }202 return nil203}204205func (pb *Problem) parseTerms(terms []string, line string) (weights []int, lits []int, err error) {206 weights = make([]int, 0, len(terms)/2)207 lits = make([]int, 0, len(terms)/2)208 i := 0209 for i < len(terms) {210 var l string211 w, err := strconv.Atoi(terms[i])212 if err != nil {213 l = terms[i]214 if !strings.HasPrefix(l, "x") && !strings.HasPrefix(l, "~x") {215 return nil, nil, fmt.Errorf("invalid weight %q in %q: %v", terms[i*2], line, err)216 }217 // This is a weightless lit, i.e a lit with weight 1.218 weights = append(weights, 1)219 } else {220 weights = append(weights, w)221 i++222 l = terms[i]223 if !strings.HasPrefix(l, "x") && !strings.HasPrefix(l, "~x") || len(l) < 2 {224 return nil, nil, fmt.Errorf("invalid variable name %q in %q", l, line)225 }226 }227 var lit int228 if l[0] == '~' {229 lit, err = strconv.Atoi(l[2:])230 lits = append(lits, -lit)231 } else {232 lit, err = strconv.Atoi(l[1:])233 lits = append(lits, lit)234 }235 if err != nil {236 return nil, nil, fmt.Errorf("invalid variable %q in %q: %v", l, line, err)237 }238 if lit > pb.NbVars {239 pb.NbVars = lit240 }241 i++242 }243 return weights, lits, nil244}245246// ParseOPB parses a file corresponding to the OPB syntax.247// See http://www.cril.univ-artois.fr/PB16/format.pdf for more details.248func ParseOPB(f io.Reader) (*Problem, error) {249 scanner := bufio.NewScanner(f)250 var pb Problem251 for scanner.Scan() {252 line := scanner.Text()253 if line == "" || line[0] == '*' {254 continue255 }256 if err := pb.parsePBLine(line); err != nil {257 return nil, err258 }259 }260 if err := scanner.Err(); err != nil {261 return nil, fmt.Errorf("could not parse OPB: %v", err)262 }263 pb.Model = make([]decLevel, pb.NbVars)264 pb.simplifyPB()265 return &pb, nil266}