MAX-SAT with sum constraint

[Aleksei Safronov]

Hello,

Sorry for such a lame question, checked almost all "minimize/maximize" examples and can't find answer anywhere. Seems like I missed something.

I have some 3-CNF formula (in generic N-CNF) and I want to maximize number of "true" clauses with constraint of how many "true" variables I can take.

Something like this:

 

model = cp_model.CpModel()
variables = []
for i in range(N):
  variables.append(model.NewBoolVar("variable_n%d" % i))
conditions = []
for clause in clauses:
  assert len(clause) <= 3
  conditions.append(model.AddBoolOr([variables[i] for i in clause]))
model.Maximize(sum(conditions))
model.Add(sum(variables) <= M)

But obviously I can't maximize conditions count. 

Formally, I have some disjunction clauses, in each clause I have at most 3 variables and I want to maximize count of "true" disjunctions.

But at most I can make M "true" variables.

Right now I have some randomized C++ solution trying to flip each variable.

[Xiang Chen]

Somthing like this?

conditions = []
for clause in clauses:
  assert len(clause) <= 3

  tmp = model.NewBoolVar("")

  model.AddBoolOr([variables[i] for i in clause]).OnlyEnforceIf(tmp)

  model.AddBoolAnd([variables[i].Not() for i in clause]).OnlyEnforceIf(tmp.Not())  
  conditions.append(tmp)

--
You received this message because you are subscribed to the Google Groups "or-tools-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/4455ba6d-5310-480d-a147-ceef1eb4e701%40googlegroups.com.

[Aleksei Safronov]

Xiang,

Thanks a lot.

Is CP-CAT solver optimal choice for such type of problems?

Because my hand-made C++ simple solver (random flipping each variable if value of target functions is not decreased) works way more faster.

I have ~30000 variables and ~80000 of clauses.

It's very strange that each step for CP-CAT solver takes several minutes comparing to several milliseconds for hand-made one.

How I run solver:

solver = cp_model.CpSolver()
solver.parameters.log_search_progress = True
solver.parameters.num_search_workers = 4
status = solver.Solve(model)

Output:

Parameters: log_search_progress: true num_search_workers: 4
Optimization model '':
#Variables: 108600 (78600 in objective)
 - 108600 in [0,1]
#kBoolAnd: 78600 (#enforced: 78600) (#literals: 220800)
#kBoolOr: 78600 (#enforced: 78600) (#literals: 220800)
#kLinearN: 1
*** starting model presolve at 0.03s
- 0 affine relations were detected.
- 0 variable equivalence relations were detected.
- rule 'bool_or: removed enforcement literal' was applied 78600 times.
- rule 'linear: simplified rhs' was applied 1 time.
- rule 'presolve: iteration' was applied 1 time.
Optimization model '':
#Variables: 108600 (78600 in objective)
 - 108600 in [0,1]
#kBoolAnd: 78600 (#enforced: 78600) (#literals: 220800)
#kBoolOr: 78600 (#literals: 299400)
#kLinearN: 1
*** starting Search at 3.35s with 4 workers and strategies: [ auto, lp_br, pseudo_cost, no_lp, helper, rnd_lns_auto, var_lns_auto, cst_lns_auto, rins/rens_lns_auto ]
#Bound   3.98s best:-inf  next:[-0,78600] no_lp
#1       4.20s best:74038 next:[74039,78600] no_lp num_bool:108600
#2       4.25s best:74039 next:[74040,78600] no_lp num_bool:108600
#3       7.04s best:74040 next:[74041,78600] no_lp num_bool:108600
#4      17.48s best:74041 next:[74042,78600] pseudo_cost num_bool:108600
#5     609.68s best:74042 next:[74043,78600] no_lp num_bool:108600
#6     609.79s best:74043 next:[74044,78600] no_lp num_bool:108600
#7     1022.74s best:74044 next:[74045,78600] no_lp num_bool:108600
#8     1023.00s best:74045 next:[74046,78600] no_lp num_bool:108600
#9     1024.32s best:74046 next:[74047,78600] no_lp num_bool:108600
#10    1122.25s best:74048 next:[74049,78600] no_lp num_bool:108600
#11    1124.18s best:74049 next:[74050,78600] no_lp num_bool:108600
#12    1497.10s best:74050 next:[74051,78600] no_lp num_bool:108600
#13    2156.26s best:74051 next:[74052,78600] no_lp num_bool:108600 

понедельник, 24 февраля 2020 г., 0:10:17 UTC+3 пользователь Xiang Chen написал:

To unsubscribe from this group and stop receiving emails from it, send an email to or-tools...@googlegroups.com.

[Frederic Didier]

Can you send us the model in proto format? So we can see if something weird happens, thanks.

Note that it might not be surprising if your problem is generated in a "random" way, then heuristic/local search solver can work better. 

CP-SAT algorithms are more adapted for applications where usually the problems are a lot more structured.

To unsubscribe from this group and stop receiving emails from it, send an email to or-tools-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/a9953a72-001c-4ac6-b135-8919fb0baf4a%40googlegroups.com.

[Laurent Perron]

You can also try to remove all the implication constraints (AddBoolAnd) as these do not change the optimal value.

To view this discussion on the web visit https://groups.google.com/d/msgid/or-tools-discuss/CABqCn%3DdmWzAceUgjHu-K0kqqq16KPpqry7EiVueb9GfjX5-1Eg%40mail.gmail.com.

--

--Laurent