71 Commits

Author SHA1 Message Date
Laurent Perron
bd04f656b3 rename MODEL_SAT to FEASIBLE, MODEL_UNSAT to INFEASIBLE 2018-07-02 15:35:40 +02:00
Laurent Perron
c1ab121ff7 ITIVector -> gtl::ITIVector; experimental LNS code for SAT 2018-06-26 21:24:10 +02:00
Laurent Perron
70e73d8754 clang-format 2018-06-08 16:40:43 +02:00
Laurent Perron
df333efbcd rewrite drat checker for sat; make fz presolve deterministic; more optims on sat internals 2018-05-03 15:00:06 +02:00
Laurent Perron
ebee158577 small changes in SAT internals 2018-04-17 13:00:25 +02:00
Laurent Perron
8623fc3580 speed up sat cumulative; add namespaces to base library + fix code 2018-04-11 13:00:30 +02:00
Laurent Perron
9044de9355 new heuristics to minimize clauses in SAT; base library changes 2018-03-06 18:17:36 +01:00
Laurent Perron
b238ebbdda Some fixes in the pure-SAT part of the cp_model solver:
- Use the model time limit (to make ^C work)
- Take into account some part of the presolve in the deterministic time.
- Move the drat flag there.
2018-02-23 17:28:21 +01:00
Laurent Perron
6b8cd2cdc2 finish C$ Sat Integer API; Refactor Glop code; Add new option for Glop Scaling; speed improvements in the sat solver 2018-02-16 17:08:01 +01:00
Laurent Perron
05f03b33c1 improve sat/circuit; various reimplementations 2018-02-12 11:36:18 +01:00
Laurent Perron
604587eec7 minor changes; change the search parameters in the cp_model.proto 2018-01-15 10:41:09 +01:00
Laurent Perron
8d7320b962 deep sync with base library; prepare for abseil.io integration 2017-12-08 14:52:49 +01:00
Laurent Perron
e14ee86de3 move rcpsp parser to ortools/data; continue working on SAT 2017-11-07 15:45:52 +01:00
Laurent Perron
2c7a8bf8f6 change copyright date 2017-10-17 13:08:10 +02:00
Laurent Perron
394bbe232a move graph code around; improve internals of sat solver 2017-10-09 11:21:43 -07:00
Laurent Perron
086640da72 move graph code around; improve sat code 2017-09-29 15:08:48 +02:00
Laurent Perron
7155047b85 cleanup includes in sat 2017-07-27 11:28:55 -07:00
Laurent Perron
c6f128db17 simplify sat internals 2017-07-24 10:31:53 -07:00
Laurent Perron
0501a62221 add sat clause simplifications to cp_model solver 2017-07-20 11:30:17 -07:00
Laurent Perron
cbd8ba8641 introduce array slices and use them in sat 2017-06-01 16:28:29 +02:00
Laurent Perron
66b8d23079 move src to ortools; simplified python generation; remove some namespaces in the ortools/base helper files 2017-04-26 17:30:25 +02:00