always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix sat presolve with complex encoding interactions; speed-up scheduling code

Browse Source
This commit is contained in:
Laurent Perron
2020-02-24 17:10:20 +01:00
parent b7e5373dbf
commit e1c1828b62
26 changed files with 471 additions and 380 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
ortools/bop/bop_base.cc
View File

@@ -79,7 +79,7 @@ ProblemState::ProblemState(const LinearBooleanProblem& problem)
lower_bound_ = 0;
for (int i = 0; i < objective.coefficients_size(); ++i) {
// Fix template version for or-tools.
lower_bound_ += std::min<int64>(0LL, objective.coefficients(i));
lower_bound_ += std::min<int64>(int64{0}, objective.coefficients(i));
}
upper_bound_ = solution_.IsFeasible() ? solution_.GetCost() : kint64max;
}

162
ortools/flatzinc/parser.tab.cc
View File

@@ -11,7 +11,7 @@
// See the License for the specific language governing permissions and
// limitations under the License.
/* A Bison parser, made by GNU Bison 3.4.1. */
/* A Bison parser, made by GNU Bison 3.4.2. */
/* Bison implementation for Yacc-like parsers in C
@@ -61,7 +61,7 @@
#define YYBISON 1
/* Bison version. */
#define YYBISON_VERSION "3.4.1"
#define YYBISON_VERSION "3.4.2"
/* Skeleton name. */
#define YYSKELETON_NAME "yacc.c"
@@ -761,7 +761,9 @@ static void yy_symbol_value_print(
#ifdef YYPRINT
if (yytype < YYNTOKENS) YYPRINT(yyo, yytoknum[yytype], *yyvaluep);
#endif
YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
YYUSE(yytype);
YY_IGNORE_MAYBE_UNINITIALIZED_END
}
/*---------------------------.
@@ -1310,7 +1312,7 @@ yyreduce:
{
yyerrok;
}
#line 1439 "./ortools/flatzinc/parser.tab.cc"
#line 1441 "./ortools/flatzinc/parser.tab.cc"
break;
case 19:
@@ -1333,7 +1335,7 @@ yyreduce:
}
delete annotations;
}
#line 1463 "./ortools/flatzinc/parser.tab.cc"
#line 1465 "./ortools/flatzinc/parser.tab.cc"
break;
case 20:
@@ -1353,7 +1355,7 @@ yyreduce:
delete assignments;
delete annotations;
}
#line 1482 "./ortools/flatzinc/parser.tab.cc"
#line 1484 "./ortools/flatzinc/parser.tab.cc"
break;
case 21:
@@ -1369,7 +1371,7 @@ yyreduce:
context->integer_array_map[identifier] = std::vector<int64>();
delete annotations;
}
#line 1497 "./ortools/flatzinc/parser.tab.cc"
#line 1499 "./ortools/flatzinc/parser.tab.cc"
break;
case 22:
@@ -1389,7 +1391,7 @@ yyreduce:
delete assignments;
delete annotations;
}
#line 1516 "./ortools/flatzinc/parser.tab.cc"
#line 1518 "./ortools/flatzinc/parser.tab.cc"
break;
case 23:
@@ -1405,7 +1407,7 @@ yyreduce:
context->float_array_map[identifier] = std::vector<double>();
delete annotations;
}
#line 1531 "./ortools/flatzinc/parser.tab.cc"
#line 1533 "./ortools/flatzinc/parser.tab.cc"
break;
case 24:
@@ -1437,7 +1439,7 @@ yyreduce:
delete assignments;
delete annotations;
}
#line 1561 "./ortools/flatzinc/parser.tab.cc"
#line 1563 "./ortools/flatzinc/parser.tab.cc"
break;
case 25:
@@ -1474,7 +1476,7 @@ yyreduce:
}
delete annotations;
}
#line 1599 "./ortools/flatzinc/parser.tab.cc"
#line 1601 "./ortools/flatzinc/parser.tab.cc"
break;
case 26:
@@ -1548,7 +1550,7 @@ yyreduce:
delete annotations;
}
}
#line 1671 "./ortools/flatzinc/parser.tab.cc"
#line 1673 "./ortools/flatzinc/parser.tab.cc"
break;
case 27:
@@ -1556,7 +1558,7 @@ yyreduce:
{
(yyval.var_or_value) = (yyvsp[0].var_or_value);
}
#line 1677 "./ortools/flatzinc/parser.tab.cc"
#line 1679 "./ortools/flatzinc/parser.tab.cc"
break;
case 28:
@@ -1564,7 +1566,7 @@ yyreduce:
{
(yyval.var_or_value) = VariableRefOrValue::Undefined();
}
#line 1683 "./ortools/flatzinc/parser.tab.cc"
#line 1685 "./ortools/flatzinc/parser.tab.cc"
break;
case 29:
@@ -1572,7 +1574,7 @@ yyreduce:
{
(yyval.var_or_value_array) = (yyvsp[-1].var_or_value_array);
}
#line 1689 "./ortools/flatzinc/parser.tab.cc"
#line 1691 "./ortools/flatzinc/parser.tab.cc"
break;
case 30:
@@ -1580,7 +1582,7 @@ yyreduce:
{
(yyval.var_or_value_array) = nullptr;
}
#line 1695 "./ortools/flatzinc/parser.tab.cc"
#line 1697 "./ortools/flatzinc/parser.tab.cc"
break;
case 31:
@@ -1588,7 +1590,7 @@ yyreduce:
{
(yyval.var_or_value_array) = nullptr;
}
#line 1701 "./ortools/flatzinc/parser.tab.cc"
#line 1703 "./ortools/flatzinc/parser.tab.cc"
break;
case 32:
@@ -1597,7 +1599,7 @@ yyreduce:
(yyval.var_or_value_array) = (yyvsp[-2].var_or_value_array);
(yyval.var_or_value_array)->PushBack((yyvsp[0].var_or_value));
}
#line 1710 "./ortools/flatzinc/parser.tab.cc"
#line 1712 "./ortools/flatzinc/parser.tab.cc"
break;
case 33:
@@ -1606,7 +1608,7 @@ yyreduce:
(yyval.var_or_value_array) = new VariableRefOrValueArray();
(yyval.var_or_value_array)->PushBack((yyvsp[0].var_or_value));
}
#line 1719 "./ortools/flatzinc/parser.tab.cc"
#line 1721 "./ortools/flatzinc/parser.tab.cc"
break;
case 34:
@@ -1615,7 +1617,7 @@ yyreduce:
(yyval.var_or_value) =
VariableRefOrValue::Value((yyvsp[0].integer_value));
}
#line 1725 "./ortools/flatzinc/parser.tab.cc"
#line 1727 "./ortools/flatzinc/parser.tab.cc"
break;
case 35:
@@ -1635,7 +1637,7 @@ yyreduce:
*ok = false;
}
}
#line 1743 "./ortools/flatzinc/parser.tab.cc"
#line 1745 "./ortools/flatzinc/parser.tab.cc"
break;
case 36:
@@ -1656,7 +1658,7 @@ yyreduce:
*ok = false;
}
}
#line 1764 "./ortools/flatzinc/parser.tab.cc"
#line 1766 "./ortools/flatzinc/parser.tab.cc"
break;
case 37:
@@ -1664,7 +1666,7 @@ yyreduce:
{
(yyval.domain) = Domain::Boolean();
}
#line 1770 "./ortools/flatzinc/parser.tab.cc"
#line 1772 "./ortools/flatzinc/parser.tab.cc"
break;
case 38:
@@ -1672,7 +1674,7 @@ yyreduce:
{
(yyval.domain) = Domain::AllInt64();
}
#line 1776 "./ortools/flatzinc/parser.tab.cc"
#line 1778 "./ortools/flatzinc/parser.tab.cc"
break;
case 39:
@@ -1681,7 +1683,7 @@ yyreduce:
(yyval.domain) =
Domain::Interval((yyvsp[-2].integer_value), (yyvsp[0].integer_value));
}
#line 1782 "./ortools/flatzinc/parser.tab.cc"
#line 1784 "./ortools/flatzinc/parser.tab.cc"
break;
case 40:
@@ -1691,7 +1693,7 @@ yyreduce:
(yyval.domain) = Domain::IntegerList(std::move(*(yyvsp[-1].integers)));
delete (yyvsp[-1].integers);
}
#line 1792 "./ortools/flatzinc/parser.tab.cc"
#line 1794 "./ortools/flatzinc/parser.tab.cc"
break;
case 41:
@@ -1699,7 +1701,7 @@ yyreduce:
{
(yyval.domain) = Domain::SetOfBoolean();
}
#line 1798 "./ortools/flatzinc/parser.tab.cc"
#line 1800 "./ortools/flatzinc/parser.tab.cc"
break;
case 42:
@@ -1707,7 +1709,7 @@ yyreduce:
{
(yyval.domain) = Domain::SetOfAllInt64();
}
#line 1804 "./ortools/flatzinc/parser.tab.cc"
#line 1806 "./ortools/flatzinc/parser.tab.cc"
break;
case 43:
@@ -1716,7 +1718,7 @@ yyreduce:
(yyval.domain) = Domain::SetOfInterval((yyvsp[-2].integer_value),
(yyvsp[0].integer_value));
}
#line 1810 "./ortools/flatzinc/parser.tab.cc"
#line 1812 "./ortools/flatzinc/parser.tab.cc"
break;
case 44:
@@ -1727,7 +1729,7 @@ yyreduce:
Domain::SetOfIntegerList(std::move(*(yyvsp[-1].integers)));
delete (yyvsp[-1].integers);
}
#line 1820 "./ortools/flatzinc/parser.tab.cc"
#line 1822 "./ortools/flatzinc/parser.tab.cc"
break;
case 45:
@@ -1735,7 +1737,7 @@ yyreduce:
{
(yyval.domain) = Domain::AllInt64();
}
#line 1826 "./ortools/flatzinc/parser.tab.cc"
#line 1828 "./ortools/flatzinc/parser.tab.cc"
break;
case 46:
@@ -1745,7 +1747,7 @@ yyreduce:
const int64 ub = ConvertAsIntegerOrDie((yyvsp[0].double_value));
(yyval.domain) = Domain::Interval(lb, ub);
}
#line 1836 "./ortools/flatzinc/parser.tab.cc"
#line 1838 "./ortools/flatzinc/parser.tab.cc"
break;
case 47:
@@ -1753,7 +1755,7 @@ yyreduce:
{
(yyval.domain) = (yyvsp[0].domain);
}
#line 1842 "./ortools/flatzinc/parser.tab.cc"
#line 1844 "./ortools/flatzinc/parser.tab.cc"
break;
case 48:
@@ -1761,7 +1763,7 @@ yyreduce:
{
(yyval.domain) = (yyvsp[0].domain);
}
#line 1848 "./ortools/flatzinc/parser.tab.cc"
#line 1850 "./ortools/flatzinc/parser.tab.cc"
break;
case 49:
@@ -1769,7 +1771,7 @@ yyreduce:
{
(yyval.domain) = (yyvsp[0].domain);
}
#line 1854 "./ortools/flatzinc/parser.tab.cc"
#line 1856 "./ortools/flatzinc/parser.tab.cc"
break;
case 50:
@@ -1778,7 +1780,7 @@ yyreduce:
(yyval.integers) = (yyvsp[-2].integers);
(yyval.integers)->emplace_back((yyvsp[0].integer_value));
}
#line 1860 "./ortools/flatzinc/parser.tab.cc"
#line 1862 "./ortools/flatzinc/parser.tab.cc"
break;
case 51:
@@ -1787,7 +1789,7 @@ yyreduce:
(yyval.integers) = new std::vector<int64>();
(yyval.integers)->emplace_back((yyvsp[0].integer_value));
}
#line 1866 "./ortools/flatzinc/parser.tab.cc"
#line 1868 "./ortools/flatzinc/parser.tab.cc"
break;
case 52:
@@ -1795,7 +1797,7 @@ yyreduce:
{
(yyval.integer_value) = (yyvsp[0].integer_value);
}
#line 1872 "./ortools/flatzinc/parser.tab.cc"
#line 1874 "./ortools/flatzinc/parser.tab.cc"
break;
case 53:
@@ -1804,7 +1806,7 @@ yyreduce:
(yyval.integer_value) =
gtl::FindOrDie(context->integer_map, (yyvsp[0].string_value));
}
#line 1878 "./ortools/flatzinc/parser.tab.cc"
#line 1880 "./ortools/flatzinc/parser.tab.cc"
break;
case 54:
@@ -1814,7 +1816,7 @@ yyreduce:
gtl::FindOrDie(context->integer_array_map, (yyvsp[-3].string_value)),
(yyvsp[-1].integer_value));
}
#line 1886 "./ortools/flatzinc/parser.tab.cc"
#line 1888 "./ortools/flatzinc/parser.tab.cc"
break;
case 55:
@@ -1823,7 +1825,7 @@ yyreduce:
(yyval.doubles) = (yyvsp[-2].doubles);
(yyval.doubles)->emplace_back((yyvsp[0].double_value));
}
#line 1892 "./ortools/flatzinc/parser.tab.cc"
#line 1894 "./ortools/flatzinc/parser.tab.cc"
break;
case 56:
@@ -1832,7 +1834,7 @@ yyreduce:
(yyval.doubles) = new std::vector<double>();
(yyval.doubles)->emplace_back((yyvsp[0].double_value));
}
#line 1898 "./ortools/flatzinc/parser.tab.cc"
#line 1900 "./ortools/flatzinc/parser.tab.cc"
break;
case 57:
@@ -1840,7 +1842,7 @@ yyreduce:
{
(yyval.double_value) = (yyvsp[0].double_value);
}
#line 1904 "./ortools/flatzinc/parser.tab.cc"
#line 1906 "./ortools/flatzinc/parser.tab.cc"
break;
case 58:
@@ -1849,7 +1851,7 @@ yyreduce:
(yyval.double_value) =
gtl::FindOrDie(context->float_map, (yyvsp[0].string_value));
}
#line 1910 "./ortools/flatzinc/parser.tab.cc"
#line 1912 "./ortools/flatzinc/parser.tab.cc"
break;
case 59:
@@ -1859,7 +1861,7 @@ yyreduce:
gtl::FindOrDie(context->float_array_map, (yyvsp[-3].string_value)),
(yyvsp[-1].integer_value));
}
#line 1918 "./ortools/flatzinc/parser.tab.cc"
#line 1920 "./ortools/flatzinc/parser.tab.cc"
break;
case 60:
@@ -1867,7 +1869,7 @@ yyreduce:
{
(yyval.domain) = Domain::IntegerValue((yyvsp[0].integer_value));
}
#line 1924 "./ortools/flatzinc/parser.tab.cc"
#line 1926 "./ortools/flatzinc/parser.tab.cc"
break;
case 61:
@@ -1876,7 +1878,7 @@ yyreduce:
(yyval.domain) =
Domain::Interval((yyvsp[-2].integer_value), (yyvsp[0].integer_value));
}
#line 1930 "./ortools/flatzinc/parser.tab.cc"
#line 1932 "./ortools/flatzinc/parser.tab.cc"
break;
case 62:
@@ -1886,7 +1888,7 @@ yyreduce:
(yyval.domain) = Domain::IntegerList(std::move(*(yyvsp[-1].integers)));
delete (yyvsp[-1].integers);
}
#line 1940 "./ortools/flatzinc/parser.tab.cc"
#line 1942 "./ortools/flatzinc/parser.tab.cc"
break;
case 63:
@@ -1894,7 +1896,7 @@ yyreduce:
{
(yyval.domain) = Domain::EmptyDomain();
}
#line 1946 "./ortools/flatzinc/parser.tab.cc"
#line 1948 "./ortools/flatzinc/parser.tab.cc"
break;
case 64:
@@ -1904,7 +1906,7 @@ yyreduce:
(yyval.domain) =
Domain::IntegerValue(static_cast<int64>((yyvsp[0].double_value)));
}
#line 1955 "./ortools/flatzinc/parser.tab.cc"
#line 1957 "./ortools/flatzinc/parser.tab.cc"
break;
case 65:
@@ -1913,7 +1915,7 @@ yyreduce:
(yyval.domain) = Domain::IntegerValue(
gtl::FindOrDie(context->integer_map, (yyvsp[0].string_value)));
}
#line 1961 "./ortools/flatzinc/parser.tab.cc"
#line 1963 "./ortools/flatzinc/parser.tab.cc"
break;
case 66:
@@ -1923,7 +1925,7 @@ yyreduce:
gtl::FindOrDie(context->integer_array_map, (yyvsp[-3].string_value)),
(yyvsp[-1].integer_value)));
}
#line 1970 "./ortools/flatzinc/parser.tab.cc"
#line 1972 "./ortools/flatzinc/parser.tab.cc"
break;
case 67:
@@ -1932,7 +1934,7 @@ yyreduce:
(yyval.domains) = (yyvsp[-2].domains);
(yyval.domains)->emplace_back((yyvsp[0].domain));
}
#line 1979 "./ortools/flatzinc/parser.tab.cc"
#line 1981 "./ortools/flatzinc/parser.tab.cc"
break;
case 68:
@@ -1941,7 +1943,7 @@ yyreduce:
(yyval.domains) = new std::vector<Domain>();
(yyval.domains)->emplace_back((yyvsp[0].domain));
}
#line 1985 "./ortools/flatzinc/parser.tab.cc"
#line 1987 "./ortools/flatzinc/parser.tab.cc"
break;
case 71:
@@ -1957,7 +1959,7 @@ yyreduce:
delete annotations;
delete (yyvsp[-2].args);
}
#line 2000 "./ortools/flatzinc/parser.tab.cc"
#line 2002 "./ortools/flatzinc/parser.tab.cc"
break;
case 72:
@@ -1966,7 +1968,7 @@ yyreduce:
(yyval.args) = (yyvsp[-2].args);
(yyval.args)->emplace_back((yyvsp[0].arg));
}
#line 2006 "./ortools/flatzinc/parser.tab.cc"
#line 2008 "./ortools/flatzinc/parser.tab.cc"
break;
case 73:
@@ -1975,7 +1977,7 @@ yyreduce:
(yyval.args) = new std::vector<Argument>();
(yyval.args)->emplace_back((yyvsp[0].arg));
}
#line 2012 "./ortools/flatzinc/parser.tab.cc"
#line 2014 "./ortools/flatzinc/parser.tab.cc"
break;
case 74:
@@ -1983,7 +1985,7 @@ yyreduce:
{
(yyval.arg) = Argument::IntegerValue((yyvsp[0].integer_value));
}
#line 2018 "./ortools/flatzinc/parser.tab.cc"
#line 2020 "./ortools/flatzinc/parser.tab.cc"
break;
case 75:
@@ -1992,7 +1994,7 @@ yyreduce:
(yyval.arg) = Argument::IntegerValue(
ConvertAsIntegerOrDie((yyvsp[0].double_value)));
}
#line 2024 "./ortools/flatzinc/parser.tab.cc"
#line 2026 "./ortools/flatzinc/parser.tab.cc"
break;
case 76:
@@ -2000,7 +2002,7 @@ yyreduce:
{
(yyval.arg) = Argument::VoidArgument();
}
#line 2030 "./ortools/flatzinc/parser.tab.cc"
#line 2032 "./ortools/flatzinc/parser.tab.cc"
break;
case 77:
@@ -2009,7 +2011,7 @@ yyreduce:
(yyval.arg) = Argument::Interval((yyvsp[-2].integer_value),
(yyvsp[0].integer_value));
}
#line 2036 "./ortools/flatzinc/parser.tab.cc"
#line 2038 "./ortools/flatzinc/parser.tab.cc"
break;
case 78:
@@ -2019,7 +2021,7 @@ yyreduce:
(yyval.arg) = Argument::IntegerList(std::move(*(yyvsp[-1].integers)));
delete (yyvsp[-1].integers);
}
#line 2046 "./ortools/flatzinc/parser.tab.cc"
#line 2048 "./ortools/flatzinc/parser.tab.cc"
break;
case 79:
@@ -2061,7 +2063,7 @@ yyreduce:
(yyval.arg) = Argument::DomainList(d);
}
}
#line 2082 "./ortools/flatzinc/parser.tab.cc"
#line 2084 "./ortools/flatzinc/parser.tab.cc"
break;
case 80:
@@ -2083,7 +2085,7 @@ yyreduce:
(yyval.arg) = Argument::FromDomain(d);
}
}
#line 2104 "./ortools/flatzinc/parser.tab.cc"
#line 2106 "./ortools/flatzinc/parser.tab.cc"
break;
case 81:
@@ -2114,7 +2116,7 @@ yyreduce:
}
delete arguments;
}
#line 2134 "./ortools/flatzinc/parser.tab.cc"
#line 2136 "./ortools/flatzinc/parser.tab.cc"
break;
case 82:
@@ -2122,7 +2124,7 @@ yyreduce:
{
(yyval.arg) = Argument::VoidArgument();
}
#line 2142 "./ortools/flatzinc/parser.tab.cc"
#line 2144 "./ortools/flatzinc/parser.tab.cc"
break;
case 83:
@@ -2133,7 +2135,7 @@ yyreduce:
: new std::vector<Annotation>();
(yyval.annotations)->emplace_back((yyvsp[0].annotation));
}
#line 2151 "./ortools/flatzinc/parser.tab.cc"
#line 2153 "./ortools/flatzinc/parser.tab.cc"
break;
case 84:
@@ -2141,7 +2143,7 @@ yyreduce:
{
(yyval.annotations) = nullptr;
}
#line 2157 "./ortools/flatzinc/parser.tab.cc"
#line 2159 "./ortools/flatzinc/parser.tab.cc"
break;
case 85:
@@ -2150,7 +2152,7 @@ yyreduce:
(yyval.annotations) = (yyvsp[-2].annotations);
(yyval.annotations)->emplace_back((yyvsp[0].annotation));
}
#line 2163 "./ortools/flatzinc/parser.tab.cc"
#line 2165 "./ortools/flatzinc/parser.tab.cc"
break;
case 86:
@@ -2159,7 +2161,7 @@ yyreduce:
(yyval.annotations) = new std::vector<Annotation>();
(yyval.annotations)->emplace_back((yyvsp[0].annotation));
}
#line 2169 "./ortools/flatzinc/parser.tab.cc"
#line 2171 "./ortools/flatzinc/parser.tab.cc"
break;
case 87:
@@ -2168,7 +2170,7 @@ yyreduce:
(yyval.annotation) = Annotation::Interval((yyvsp[-2].integer_value),
(yyvsp[0].integer_value));
}
#line 2175 "./ortools/flatzinc/parser.tab.cc"
#line 2177 "./ortools/flatzinc/parser.tab.cc"
break;
case 88:
@@ -2176,7 +2178,7 @@ yyreduce:
{
(yyval.annotation) = Annotation::IntegerValue((yyvsp[0].integer_value));
}
#line 2181 "./ortools/flatzinc/parser.tab.cc"
#line 2183 "./ortools/flatzinc/parser.tab.cc"
break;
case 89:
@@ -2184,7 +2186,7 @@ yyreduce:
{
(yyval.annotation) = Annotation::String((yyvsp[0].string_value));
}
#line 2187 "./ortools/flatzinc/parser.tab.cc"
#line 2189 "./ortools/flatzinc/parser.tab.cc"
break;
case 90:
@@ -2201,7 +2203,7 @@ yyreduce:
(yyval.annotation) = Annotation::Identifier(id);
}
}
#line 2202 "./ortools/flatzinc/parser.tab.cc"
#line 2204 "./ortools/flatzinc/parser.tab.cc"
break;
case 91:
@@ -2216,7 +2218,7 @@ yyreduce:
(yyval.annotation) = Annotation::FunctionCall((yyvsp[-3].string_value));
}
}
#line 2216 "./ortools/flatzinc/parser.tab.cc"
#line 2218 "./ortools/flatzinc/parser.tab.cc"
break;
case 92:
@@ -2229,7 +2231,7 @@ yyreduce:
gtl::FindOrDie(context->variable_array_map, (yyvsp[-3].string_value)),
(yyvsp[-1].integer_value)));
}
#line 2227 "./ortools/flatzinc/parser.tab.cc"
#line 2229 "./ortools/flatzinc/parser.tab.cc"
break;
case 93:
@@ -2244,7 +2246,7 @@ yyreduce:
(yyval.annotation) = Annotation::Empty();
}
}
#line 2241 "./ortools/flatzinc/parser.tab.cc"
#line 2243 "./ortools/flatzinc/parser.tab.cc"
break;
case 94:
@@ -2257,7 +2259,7 @@ yyreduce:
model->Satisfy(std::vector<Annotation>());
}
}
#line 2254 "./ortools/flatzinc/parser.tab.cc"
#line 2256 "./ortools/flatzinc/parser.tab.cc"
break;
case 95:
@@ -2272,7 +2274,7 @@ yyreduce:
model->Minimize((yyvsp[0].arg).Var(), std::vector<Annotation>());
}
}
#line 2268 "./ortools/flatzinc/parser.tab.cc"
#line 2270 "./ortools/flatzinc/parser.tab.cc"
break;
case 96:
@@ -2287,10 +2289,10 @@ yyreduce:
model->Maximize((yyvsp[0].arg).Var(), std::vector<Annotation>());
}
}
#line 2282 "./ortools/flatzinc/parser.tab.cc"
#line 2284 "./ortools/flatzinc/parser.tab.cc"
break;
#line 2286 "./ortools/flatzinc/parser.tab.cc"
#line 2288 "./ortools/flatzinc/parser.tab.cc"
default:
break;

2
ortools/flatzinc/parser.tab.hh
View File

@@ -1,4 +1,4 @@
/* A Bison parser, made by GNU Bison 3.4.1. */
/* A Bison parser, made by GNU Bison 3.4.2. */
/* Bison interface for Yacc-like parsers in C

32
ortools/sat/cp_model.proto
View File

@@ -511,6 +511,21 @@ message CpModelProto {
// try to return a solution "close" to this assignment in case of multiple
// optimal solutions.
PartialVariableAssignment solution_hint = 6;
// A list of literals. The model will be solved assuming all these literals
// are true. Compared to just fixing the domain of these literals, using this
// mechanism is slower but allows in case the model is INFEASIBLE to get a
// potentially small subset of them that can be used to explain the
// infeasibility.
//
// Think (IIS), except when you are only concerned by the provided
// assumptions. This is powerful as it allows to group a set of logicially
// related constraint under only one enforcement literal which can potentially
// give you a good and interpretable explanation for infeasiblity.
//
// Such infeasibility explanation will be available in the
// sufficient_assumptions_for_infeasibility response field.
repeated int32 assumptions = 7;
}
// The status returned by a solver trying to solve a CpModelProto.
@@ -540,7 +555,7 @@ enum CpSolverStatus {
//
// TODO(user): support returning multiple solutions. Look at the Stubby
// streaming API as we probably wants to get them as they are found.
// Next id: 23
// Next id: 24
message CpSolverResponse {
// The status of the solve.
CpSolverStatus status = 1;
@@ -586,6 +601,21 @@ message CpSolverResponse {
// sub-optimal feasible ones.
repeated IntegerVariableProto tightened_variables = 21;
// A subset of the model "assumptions" field. This will only be filled if the
// status is INFEASIBLE. This subset of assumption will be enough to still get
// an infeasible problem.
//
// This is related to what is called the irreducible inconsistent subsystem or
// IIS. Except one is only concerned by the provided assumptions. There is
// also no guarantee that we return an irreducible (aka minimal subset).
// However, this is based on SAT explanation and there is a good chance it is
// not too large.
//
// If you really want a minimal subset, a possible way to get one is by
// changing your model to minimize the number of assumptions at false, but
// this is likely an harder problem to solve.
repeated int32 sufficient_assumptions_for_infeasibility = 23;
// This will be true iff the solver was asked to find all solutions to a
// satisfiability problem (or all optimal solutions to an optimization
// problem), and it was successful in doing so.

6
ortools/sat/cp_model_checker.cc
View File

@@ -486,6 +486,12 @@ std::string ValidateCpModel(const CpModelProto& model) {
}
RETURN_IF_NOT_EMPTY(ValidateSearchStrategies(model));
RETURN_IF_NOT_EMPTY(ValidateSolutionHint(model));
for (const int ref : model.assumptions()) {
if (!LiteralReferenceIsValid(model, ref)) {
return absl::StrCat("Invalid literal reference ", ref,
" in the 'assumptions' field.");
}
}
return "";
}

33
ortools/sat/cp_model_presolve.cc
View File

@@ -4154,6 +4154,7 @@ void CpModelPresolver::TryToSimplifyDomain(int var) {
CHECK(RefIsPositive(var));
if (context_->ModelIsUnsat()) return;
if (context_->IsFixed(var)) return;
if (context_->VariableIsNotUsedAnymore(var)) return;
const AffineRelation::Relation r = context_->GetAffineRelation(var);
if (r.representative != var) return;
@@ -4163,7 +4164,7 @@ void CpModelPresolver::TryToSimplifyDomain(int var) {
// Special case for non-Boolean domain of size 2.
if (domain.Size() == 2 && (domain.Min() != 0 || domain.Max() != 1)) {
// Shifted Boolean variable.
// Shifted and/or scaled Boolean variable.
const int new_var_index = context_->NewBoolVar();
context_->InsertVarValueEncoding(new_var_index, var, domain.Max());
context_->UpdateRuleStats("variables: canonicalize size two domain");
@@ -4294,11 +4295,16 @@ void CpModelPresolver::PresolveToFixPoint() {
}
// Re-add to the queue the constraints that touch a variable that changed.
// Note that it is important to use indices in the loop below because
// TryToSimplifyDomain() might create new variables which will change
// the set of modified domains.
//
// TODO(user): Avoid reprocessing the constraints that changed the variables
// with the use of timestamp.
if (context_->ModelIsUnsat()) return;
for (const int v : context_->modified_domains.PositionsSetAtLeastOnce()) {
for (int i = 0;
i < context_->modified_domains.PositionsSetAtLeastOnce().size(); ++i) {
const int v = context_->modified_domains.PositionsSetAtLeastOnce()[i];
if (context_->IsFixed(v)) {
context_->ExploitFixedDomain(v);
} else {
@@ -4787,7 +4793,7 @@ bool CpModelPresolver::Presolve() {
mapping[i] = postsolve_mapping_->size();
postsolve_mapping_->push_back(i);
}
ApplyVariableMapping(mapping, context_->working_model);
ApplyVariableMapping(mapping, *context_);
// Hack to display the number of deductions stored.
if (context_->deductions.NumDeductions() > 0) {
@@ -4808,7 +4814,9 @@ bool CpModelPresolver::Presolve() {
}
void ApplyVariableMapping(const std::vector<int>& mapping,
CpModelProto* proto) {
const PresolveContext& context) {
CpModelProto* proto = context.working_model;
// Remap all the variable/literal references in the constraints and the
// enforcement literals in the variables.
auto mapping_function = [&mapping](int* ref) {
@@ -4856,12 +4864,19 @@ void ApplyVariableMapping(const std::vector<int>& mapping,
auto* mutable_hint = proto->mutable_solution_hint();
int new_size = 0;
for (int i = 0; i < mutable_hint->vars_size(); ++i) {
const int ref = mutable_hint->vars(i);
const int image = mapping[PositiveRef(ref)];
const int old_ref = mutable_hint->vars(i);
const int64 old_value = mutable_hint->values(i);
// Note that if (old_value - r.offset) is not divisible by r.coeff, then
// the hint is clearly infeasible, but we still set it to a "close" value.
const AffineRelation::Relation r = context.GetAffineRelation(old_ref);
const int var = r.representative;
const int64 value = (old_value - r.offset) / r.coeff;
const int image = mapping[var];
if (image >= 0) {
mutable_hint->set_vars(new_size,
RefIsPositive(ref) ? image : NegatedRef(image));
mutable_hint->set_values(new_size, mutable_hint->values(i));
mutable_hint->set_vars(new_size, image);
mutable_hint->set_values(new_size, value);
++new_size;
}
}

3
ortools/sat/cp_model_presolve.h
View File

@@ -36,7 +36,8 @@ namespace sat {
//
// The image of the mapping should be dense in [0, new_num_variables), this is
// also CHECKed.
void ApplyVariableMapping(const std::vector<int>& mapping, CpModelProto* proto);
void ApplyVariableMapping(const std::vector<int>& mapping,
const PresolveContext& context);
// Presolves the initial content of presolved_model.
//

28
ortools/sat/cp_model_solver.cc
View File

@@ -1484,7 +1484,7 @@ void QuickSolveWithHint(const CpModelProto& model_proto,
// Temporarily change the parameters.
auto* parameters = model->GetOrCreate<SatParameters>();
const SatParameters saved_params = *parameters;
parameters->set_max_number_of_conflicts(10);
parameters->set_max_number_of_conflicts(parameters->hint_conflict_limit());
parameters->set_search_branching(SatParameters::HINT_SEARCH);
parameters->set_optimize_with_core(false);
auto cleanup = ::absl::MakeCleanup(
@@ -2430,7 +2430,8 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
// TODO(user): Support solution hint, but then the first TODO will make it
// automatic.
if (!model_proto.has_objective() && !model_proto.has_solution_hint() &&
!params.enumerate_all_solutions() && !params.use_lns_only()) {
!params.enumerate_all_solutions() && !params.use_lns_only() &&
model_proto.assumptions().empty()) {
bool is_pure_sat = true;
for (const IntegerVariableProto& var : model_proto.variables()) {
if (var.domain_size() != 2 || var.domain(0) < 0 || var.domain(1) > 1) {
@@ -2469,6 +2470,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
LOG_IF(INFO, log_search) << absl::StrFormat(
"*** starting model presolve at %.2fs", wall_timer.Get());
CpModelProto new_cp_model_proto = model_proto; // Copy.
CpModelProto mapping_proto;
PresolveOptions options;
options.log_info = log_search;
@@ -2477,6 +2479,20 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
auto context =
absl::make_unique<PresolveContext>(&new_cp_model_proto, &mapping_proto);
// Load the assumptions if any. For now we just fix the variables.
//
// TODO(user): Handle this properly.
context->InitializeNewDomains();
for (const int ref : model_proto.assumptions()) {
if (!context->SetLiteralToTrue(ref)) {
CpSolverResponse response;
response.set_status(CpSolverStatus::INFEASIBLE);
response.add_sufficient_assumptions_for_infeasibility(ref);
LOG_IF(INFO, log_search) << CpSolverResponseStats(response);
return response;
}
}
// This function will be called before any CpSolverResponse is returned
// to the user (at the end and in callbacks).
std::function<void(CpSolverResponse * response)> postprocess_solution;
@@ -2654,6 +2670,14 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
response.solution().end())));
}
LOG_IF(INFO, log_search) << CpSolverResponseStats(response);
// TODO(user): Handle this properly.
if (response.status() == CpSolverStatus::INFEASIBLE) {
// For now, just pass in all assumptions.
*response.mutable_sufficient_assumptions_for_infeasibility() =
model_proto.assumptions();
}
return response;
}

26
ortools/sat/cuts.cc
View File

@@ -1415,17 +1415,6 @@ CutGenerator CreateAllDifferentCutGenerator(
}
namespace {
IntegerValue GetCoefficient(const IntegerVariable var,
const LinearExpression& expr) {
for (int i = 0; i < expr.vars.size(); ++i) {
if (expr.vars[i] == var) {
return expr.coeffs[i];
}
}
return IntegerValue(0);
}
// Returns max((w2i - w1i)*Li, (w2i - w1i)*Ui).
IntegerValue MaxCornerDifference(const IntegerVariable var,
const IntegerValue w1_i,
@@ -1448,14 +1437,14 @@ IntegerValue MPlusCoefficient(
const gtl::ITIVector<IntegerVariable, int>& variable_partition,
const int max_index, const IntegerTrail& integer_trail) {
IntegerValue coeff = exprs[max_index].offset;
// TODO(user): This algo is quadratic since GetCoefficient() is linear.
// This can be optimized (better complexity) if needed.
// TODO(user): This algo is quadratic since GetCoefficientOfPositiveVar()
// is linear. This can be optimized (better complexity) if needed.
for (const IntegerVariable var : x_vars) {
const int target_index = variable_partition[var];
if (max_index != target_index) {
coeff += MaxCornerDifference(
var, GetCoefficient(var, exprs[target_index]),
GetCoefficient(var, exprs[max_index]), integer_trail);
var, GetCoefficientOfPositiveVar(var, exprs[target_index]),
GetCoefficientOfPositiveVar(var, exprs[max_index]), integer_trail);
}
}
return coeff;
@@ -1473,14 +1462,15 @@ double ComputeContribution(
CHECK_LT(target_index, exprs.size());
const LinearExpression& target_expr = exprs[target_index];
const double xi_value = lp_values[xi_var];
const IntegerValue wt_i = GetCoefficient(xi_var, target_expr);
const IntegerValue wt_i = GetCoefficientOfPositiveVar(xi_var, target_expr);
double contrib = wt_i.value() * xi_value;
for (int expr_index = 0; expr_index < exprs.size(); ++expr_index) {
if (expr_index == target_index) continue;
const LinearExpression& max_expr = exprs[expr_index];
const double z_max_value = lp_values[z_vars[expr_index]];
const IntegerValue corner_value = MaxCornerDifference(
xi_var, wt_i, GetCoefficient(xi_var, max_expr), integer_trail);
xi_var, wt_i, GetCoefficientOfPositiveVar(xi_var, max_expr),
integer_trail);
contrib += corner_value.value() * z_max_value;
}
return contrib;
@@ -1534,7 +1524,7 @@ CutGenerator CreateLinMaxCutGenerator(
for (const IntegerVariable xi_var : x_vars) {
const int input_index = variable_partition[xi_var];
const LinearExpression& expr = exprs[input_index];
const IntegerValue coeff = GetCoefficient(xi_var, expr);
const IntegerValue coeff = GetCoefficientOfPositiveVar(xi_var, expr);
if (coeff != IntegerValue(0)) {
cut.AddTerm(xi_var, coeff);
}

90
ortools/sat/disjunctive.cc
View File

@@ -173,6 +173,12 @@ void TaskSet::AddEntry(const Entry& e) {
if (j <= optimized_restart_) optimized_restart_ = 0;
}
void TaskSet::AddShiftedStartMinEntry(const SchedulingConstraintHelper& helper,
int t) {
const IntegerValue dmin = helper.DurationMin(t);
AddEntry({t, std::max(helper.StartMin(t), helper.EndMin(t) - dmin), dmin});
}
void TaskSet::NotifyEntryIsNowLastIfPresent(const Entry& e) {
const int size = sorted_tasks_.size();
for (int i = 0;; ++i) {
@@ -645,50 +651,54 @@ bool DisjunctiveDetectablePrecedences::Propagate() {
// window_end]. So any task to the left of the window cannot push such
// task start_min, and any task to the right of the window will have a
// start_max >= end_min, so wouldn't be in detectable precedence.
window_.clear();
task_by_increasing_end_min_.clear();
IntegerValue window_end = kMinIntegerValue;
IntegerValue window_max_of_end_min = kMinIntegerValue;
for (const TaskTime task_time : helper_->TaskByIncreasingShiftedStartMin()) {
const int task = task_time.task_index;
if (helper_->IsAbsent(task)) continue;
// TODO(user): It should actually be the real start_min here not the shifted
// one. Otherwise we might miss some propagation. Try to unit-test this!
const IntegerValue start_min = task_time.time;
if (start_min < window_end) {
const IntegerValue duration_min = helper_->DurationMin(task);
const IntegerValue end_min = helper_->EndMin(task);
window_.push_back({task, end_min});
window_end += duration_min;
window_max_of_end_min = std::max(window_max_of_end_min, end_min);
const IntegerValue shifted_smin = task_time.time;
const IntegerValue duration_min = helper_->DurationMin(task);
const IntegerValue end_min_if_present = shifted_smin + duration_min;
// Note that we use the real StartMin() here, as this is the one we will
// push.
if (helper_->StartMin(task) < window_end) {
task_by_increasing_end_min_.push_back({task, end_min_if_present});
window_end = std::max(window_end, task_time.time) + duration_min;
continue;
}
// Process current window.
if (window_.size() > 1 && !PropagateSubwindow(window_max_of_end_min)) {
if (task_by_increasing_end_min_.size() > 1 && !PropagateSubwindow()) {
return false;
}
// Start of the next window.
window_.clear();
const IntegerValue duration_min = helper_->DurationMin(task);
const IntegerValue end_min = helper_->EndMin(task);
window_.push_back({task, end_min});
window_end = start_min + duration_min;
window_max_of_end_min = end_min;
task_by_increasing_end_min_.clear();
task_by_increasing_end_min_.push_back({task, end_min_if_present});
window_end = end_min_if_present;
}
if (window_.size() > 1 && !PropagateSubwindow(window_max_of_end_min)) {
if (task_by_increasing_end_min_.size() > 1 && !PropagateSubwindow()) {
return false;
}
return true;
}
bool DisjunctiveDetectablePrecedences::PropagateSubwindow(
IntegerValue max_end_min) {
bool DisjunctiveDetectablePrecedences::PropagateSubwindow() {
DCHECK(!task_by_increasing_end_min_.empty());
// The vector is already sorted by shifted_start_min, so there is likely a
// good correlation, hence the incremental sort.
IncrementalSort(task_by_increasing_end_min_.begin(),
task_by_increasing_end_min_.end());
const IntegerValue max_end_min = task_by_increasing_end_min_.back().time;
// Fill and sort task_by_increasing_start_max_.
task_by_increasing_start_max_.clear();
for (const TaskTime entry : window_) {
for (const TaskTime entry : task_by_increasing_end_min_) {
const int task = entry.task_index;
const IntegerValue start_max = helper_->StartMax(task);
if (start_max < max_end_min && helper_->IsPresent(task)) {
@@ -699,15 +709,6 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow(
std::sort(task_by_increasing_start_max_.begin(),
task_by_increasing_start_max_.end());
// The window is already sorted by shifted_start_min, so there is likely a
// good correlation, hence the incremental sort.
//
// TODO(user): Instead of end-min, we should use end-min if present. Same in
// other places.
auto& task_by_increasing_end_min = window_;
IncrementalSort(task_by_increasing_end_min.begin(),
task_by_increasing_end_min.end());
// Invariant: need_update is false implies that task_set_end_min is equal to
// task_set_.ComputeEndMin().
//
@@ -720,9 +721,14 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow(
int queue_index = 0;
int blocking_task = -1;
const int queue_size = task_by_increasing_start_max_.size();
for (const auto task_time : task_by_increasing_end_min) {
for (const auto task_time : task_by_increasing_end_min_) {
// Note that we didn't put absent task in task_by_increasing_end_min_, but
// the absence might have been pushed while looping here. This is fine since
// any push we do on this task should handle this case correctly.
//
// TODO(user): Still test and continue the status even if in most cases the
// task will not be absent?
const int current_task = task_time.task_index;
DCHECK(!helper_->IsAbsent(current_task));
for (; queue_index < queue_size; ++queue_index) {
const auto to_insert = task_by_increasing_start_max_[queue_index];
@@ -754,14 +760,14 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow(
helper_->AddReasonForBeingBefore(t, blocking_task);
return helper_->ReportConflict();
}
DCHECK_LT(start_max, helper_->EndMin(t));
DCHECK_LT(start_max,
helper_->ShiftedStartMin(t) + helper_->DurationMin(t));
DCHECK(to_propagate_.empty());
blocking_task = t;
to_propagate_.push_back(t);
} else {
need_update = true;
task_set_.AddEntry(
{t, helper_->ShiftedStartMin(t), helper_->DurationMin(t)});
task_set_.AddShiftedStartMinEntry(*helper_, t);
}
}
@@ -797,7 +803,8 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow(
// We need:
// - StartMax(ct) < EndMin(t) for the detectable precedence.
// - StartMin(ct) >= window_start for the value of task_set_end_min.
const IntegerValue end_min = helper_->EndMin(t);
const IntegerValue end_min_if_present =
helper_->ShiftedStartMin(t) + helper_->DurationMin(t);
const IntegerValue window_start =
sorted_tasks[critical_index].start_min;
for (int i = critical_index; i < sorted_tasks.size(); ++i) {
@@ -806,11 +813,11 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow(
helper_->AddPresenceReason(ct);
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].duration_min,
window_start);
helper_->AddStartMaxReason(ct, end_min - 1);
helper_->AddStartMaxReason(ct, end_min_if_present - 1);
}
// Add the reason for t (we only need the end-min).
helper_->AddEndMinReason(t, end_min);
helper_->AddEndMinReason(t, end_min_if_present);
// This augment the start-min of t. Note that t is not in task set
// yet, so we will use this updated start if we ever add it there.
@@ -827,8 +834,7 @@ bool DisjunctiveDetectablePrecedences::PropagateSubwindow(
// equal to the end_min of the task we push.
need_update = true;
blocking_task = -1;
task_set_.AddEntry(
{t, helper_->ShiftedStartMin(t), helper_->DurationMin(t)});
task_set_.AddShiftedStartMinEntry(*helper_, t);
}
}
to_propagate_.clear();
@@ -1075,7 +1081,7 @@ bool DisjunctiveNotLast::PropagateSubwindow() {
// So we can deduce that the end-max of t is smaller than or equal to the
// largest start-max of the critical tasks.
//
// Note that this works as well when task_is_currently_present_[t] is false.
// Note that this works as well when the presence of t is still unknown.
int critical_index = 0;
const IntegerValue end_min_of_critical_tasks =
task_set_.ComputeEndMin(/*task_to_ignore=*/t, &critical_index);

8
ortools/sat/disjunctive.h
View File

@@ -74,6 +74,10 @@ class TaskSet {
void AddEntry(const Entry& e);
void RemoveEntryWithIndex(int index);
// Same as AddEntry({t, helper->ShiftedStartMin(t), helper->DurationMin(t)}).
// This is a minor optimization to not call DurationMin(t) twice.
void AddShiftedStartMinEntry(const SchedulingConstraintHelper& helper, int t);
// Advanced usage, if the entry is present, this assumes that its start_min is
// >= the end min without it, and update the datastructure accordingly.
void NotifyEntryIsNowLastIfPresent(const Entry& e);
@@ -162,9 +166,9 @@ class DisjunctiveDetectablePrecedences : public PropagatorInterface {
int RegisterWith(GenericLiteralWatcher* watcher);
private:
bool PropagateSubwindow(IntegerValue max_end_min);
bool PropagateSubwindow();
std::vector<TaskTime> window_;
std::vector<TaskTime> task_by_increasing_end_min_;
std::vector<TaskTime> task_by_increasing_start_max_;
std::vector<bool> processed_;

1
ortools/sat/integer.cc
View File

@@ -543,6 +543,7 @@ bool IntegerTrail::Propagate(Trail* trail) {
}
void IntegerTrail::Untrail(const Trail& trail, int literal_trail_index) {
++num_untrails_;
const int level = trail.CurrentDecisionLevel();
for (ReversibleInterface* rev : reversible_classes_) rev->SetLevel(level);
var_to_current_lb_interval_index_.SetLevel(level);

3
ortools/sat/integer.h
View File

@@ -525,7 +525,6 @@ class IntegerTrail : public SatPropagator {
public:
explicit IntegerTrail(Model* model)
: SatPropagator("IntegerTrail"),
num_enqueues_(0),
domains_(model->GetOrCreate<IntegerDomains>()),
encoder_(model->GetOrCreate<IntegerEncoder>()),
trail_(model->GetOrCreate<Trail>()) {
@@ -757,6 +756,7 @@ class IntegerTrail : public SatPropagator {
// looking at the integer trail index is not enough because at level zero it
// doesn't change since we directly update the "fixed" bounds.
int64 num_enqueues() const { return num_enqueues_; }
int64 timestamp() const { return num_enqueues_ + num_untrails_; }
// Same as num_enqueues but only count the level zero changes.
int64 num_level_zero_enqueues() const { return num_level_zero_enqueues_; }
@@ -976,6 +976,7 @@ class IntegerTrail : public SatPropagator {
std::vector<int> boolean_trail_index_to_integer_one_;
int64 num_enqueues_ = 0;
int64 num_untrails_ = 0;
int64 num_level_zero_enqueues_ = 0;
std::vector<SparseBitset<IntegerVariable>*> watchers_;

12
ortools/sat/integer_search.cc
View File

@@ -417,20 +417,16 @@ std::function<LiteralIndex()> FollowHint(
for (int i = 0; i < vars.size(); ++i) {
const IntegerValue value = values[i];
if (vars[i].bool_var != kNoBooleanVariable) {
if (trail->Assignment().VariableIsAssigned(vars[i].bool_var)) {
continue;
}
if (trail->Assignment().VariableIsAssigned(vars[i].bool_var)) continue;
return Literal(vars[i].bool_var, value == 1).Index();
} else {
const IntegerVariable integer_var = vars[i].int_var;
if (integer_trail->IsCurrentlyIgnored(integer_var)) continue;
const IntegerValue lb = integer_trail->LowerBound(integer_var);
const IntegerValue ub = integer_trail->UpperBound(integer_var);
if (lb == ub) continue;
if (integer_trail->IsFixed(integer_var)) continue;
const IntegerVariable positive_var = PositiveVariable(integer_var);
const LiteralIndex decision =
SplitAroundGivenValue(positive_var, value, model);
const LiteralIndex decision = SplitAroundGivenValue(
positive_var, positive_var != integer_var ? -value : value, model);
if (decision != kNoLiteralIndex) return decision;
// If the value is outside the current possible domain, we skip it.

87
ortools/sat/intervals.cc
View File

@@ -121,20 +121,22 @@ void SchedulingConstraintHelper::ResetFromSubset(
void SchedulingConstraintHelper::InitSortedVectors() {
const int num_tasks = start_vars_.size();
task_by_increasing_min_start_.resize(num_tasks);
task_by_increasing_min_end_.resize(num_tasks);
task_by_decreasing_max_start_.resize(num_tasks);
task_by_decreasing_max_end_.resize(num_tasks);
task_by_increasing_start_min_.resize(num_tasks);
task_by_increasing_end_min_.resize(num_tasks);
task_by_decreasing_start_max_.resize(num_tasks);
task_by_decreasing_end_max_.resize(num_tasks);
task_by_increasing_shifted_start_min_.resize(num_tasks);
task_by_decreasing_shifted_end_max_.resize(num_tasks);
task_by_negated_shifted_end_max_.resize(num_tasks);
for (int t = 0; t < num_tasks; ++t) {
task_by_increasing_min_start_[t].task_index = t;
task_by_increasing_min_end_[t].task_index = t;
task_by_decreasing_max_start_[t].task_index = t;
task_by_decreasing_max_end_[t].task_index = t;
task_by_increasing_start_min_[t].task_index = t;
task_by_increasing_end_min_[t].task_index = t;
task_by_decreasing_start_max_[t].task_index = t;
task_by_decreasing_end_max_[t].task_index = t;
task_by_increasing_shifted_start_min_[t].task_index = t;
task_by_decreasing_shifted_end_max_[t].task_index = t;
task_by_negated_shifted_end_max_[t].task_index = t;
}
shifted_start_min_timestamp_ = -1;
negated_shifted_end_max_timestamp_ = -1;
}
void SchedulingConstraintHelper::SetTimeDirection(bool is_forward) {
@@ -143,75 +145,80 @@ void SchedulingConstraintHelper::SetTimeDirection(bool is_forward) {
std::swap(start_vars_, minus_end_vars_);
std::swap(end_vars_, minus_start_vars_);
std::swap(task_by_increasing_min_start_, task_by_decreasing_max_end_);
std::swap(task_by_increasing_min_end_, task_by_decreasing_max_start_);
std::swap(task_by_increasing_start_min_, task_by_decreasing_end_max_);
std::swap(task_by_increasing_end_min_, task_by_decreasing_start_max_);
std::swap(task_by_increasing_shifted_start_min_,
task_by_decreasing_shifted_end_max_);
task_by_negated_shifted_end_max_);
std::swap(shifted_start_min_timestamp_, negated_shifted_end_max_timestamp_);
}
const std::vector<TaskTime>&
SchedulingConstraintHelper::TaskByIncreasingStartMin() {
const int num_tasks = NumTasks();
for (int i = 0; i < num_tasks; ++i) {
TaskTime& ref = task_by_increasing_min_start_[i];
TaskTime& ref = task_by_increasing_start_min_[i];
ref.time = StartMin(ref.task_index);
}
IncrementalSort(task_by_increasing_min_start_.begin(),
task_by_increasing_min_start_.end());
return task_by_increasing_min_start_;
IncrementalSort(task_by_increasing_start_min_.begin(),
task_by_increasing_start_min_.end());
return task_by_increasing_start_min_;
}
const std::vector<TaskTime>&
SchedulingConstraintHelper::TaskByIncreasingEndMin() {
const int num_tasks = NumTasks();
for (int i = 0; i < num_tasks; ++i) {
TaskTime& ref = task_by_increasing_min_end_[i];
TaskTime& ref = task_by_increasing_end_min_[i];
ref.time = EndMin(ref.task_index);
}
IncrementalSort(task_by_increasing_min_end_.begin(),
task_by_increasing_min_end_.end());
return task_by_increasing_min_end_;
IncrementalSort(task_by_increasing_end_min_.begin(),
task_by_increasing_end_min_.end());
return task_by_increasing_end_min_;
}
const std::vector<TaskTime>&
SchedulingConstraintHelper::TaskByDecreasingStartMax() {
const int num_tasks = NumTasks();
for (int i = 0; i < num_tasks; ++i) {
TaskTime& ref = task_by_decreasing_max_start_[i];
TaskTime& ref = task_by_decreasing_start_max_[i];
ref.time = StartMax(ref.task_index);
}
IncrementalSort(task_by_decreasing_max_start_.begin(),
task_by_decreasing_max_start_.end(),
IncrementalSort(task_by_decreasing_start_max_.begin(),
task_by_decreasing_start_max_.end(),
std::greater<TaskTime>());
return task_by_decreasing_max_start_;
return task_by_decreasing_start_max_;
}
const std::vector<TaskTime>&
SchedulingConstraintHelper::TaskByDecreasingEndMax() {
const int num_tasks = NumTasks();
for (int i = 0; i < num_tasks; ++i) {
TaskTime& ref = task_by_decreasing_max_end_[i];
TaskTime& ref = task_by_decreasing_end_max_[i];
ref.time = EndMax(ref.task_index);
}
IncrementalSort(task_by_decreasing_max_end_.begin(),
task_by_decreasing_max_end_.end(), std::greater<TaskTime>());
return task_by_decreasing_max_end_;
IncrementalSort(task_by_decreasing_end_max_.begin(),
task_by_decreasing_end_max_.end(), std::greater<TaskTime>());
return task_by_decreasing_end_max_;
}
const std::vector<TaskTime>&
SchedulingConstraintHelper::TaskByIncreasingShiftedStartMin() {
const int num_tasks = NumTasks();
bool is_sorted = true;
IntegerValue previous = kMinIntegerValue;
for (int i = 0; i < num_tasks; ++i) {
TaskTime& ref = task_by_increasing_shifted_start_min_[i];
ref.time = ShiftedStartMin(ref.task_index);
is_sorted = is_sorted && ref.time >= previous;
previous = ref.time;
const int64 new_timestamp = integer_trail_->timestamp();
if (new_timestamp > shifted_start_min_timestamp_) {
shifted_start_min_timestamp_ = new_timestamp;
const int num_tasks = NumTasks();
bool is_sorted = true;
IntegerValue previous = kMinIntegerValue;
for (int i = 0; i < num_tasks; ++i) {
TaskTime& ref = task_by_increasing_shifted_start_min_[i];
ref.time = ShiftedStartMin(ref.task_index);
is_sorted = is_sorted && ref.time >= previous;
previous = ref.time;
}
if (is_sorted) return task_by_increasing_shifted_start_min_;
IncrementalSort(task_by_increasing_shifted_start_min_.begin(),
task_by_increasing_shifted_start_min_.end());
}
if (is_sorted) return task_by_increasing_shifted_start_min_;
IncrementalSort(task_by_increasing_shifted_start_min_.begin(),
task_by_increasing_shifted_start_min_.end());
return task_by_increasing_shifted_start_min_;
}

38
ortools/sat/intervals.h
View File

@@ -320,13 +320,15 @@ class SchedulingConstraintHelper {
std::vector<IntegerVariable> minus_end_vars_;
// Sorted vectors returned by the TasksBy*() functions.
std::vector<TaskTime> task_by_increasing_min_start_;
std::vector<TaskTime> task_by_increasing_min_end_;
std::vector<TaskTime> task_by_decreasing_max_start_;
std::vector<TaskTime> task_by_decreasing_max_end_;
std::vector<TaskTime> task_by_increasing_start_min_;
std::vector<TaskTime> task_by_increasing_end_min_;
std::vector<TaskTime> task_by_decreasing_start_max_;
std::vector<TaskTime> task_by_decreasing_end_max_;
std::vector<TaskTime> task_by_increasing_shifted_start_min_;
std::vector<TaskTime> task_by_decreasing_shifted_end_max_;
std::vector<TaskTime> task_by_negated_shifted_end_max_;
int64 shifted_start_min_timestamp_ = -1;
int64 negated_shifted_end_max_timestamp_ = -1;
// Reason vectors.
std::vector<Literal> literal_reason_;
@@ -450,8 +452,20 @@ inline void SchedulingConstraintHelper::AddStartMaxReason(
inline void SchedulingConstraintHelper::AddEndMinReason(
int t, IntegerValue lower_bound) {
DCHECK_GE(EndMin(t), lower_bound);
AddOtherReason(t);
if (EndMin(t) < lower_bound) {
// This might happen if we used for the end_min the max between end_min
// and start_min + duration_min. That is, the end_min assuming the task is
// present.
const IntegerValue duration_min = DurationMin(t);
if (duration_vars_[t] != kNoIntegerVariable) {
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(duration_vars_[t], duration_min));
}
integer_reason_.push_back(IntegerLiteral::GreaterOrEqual(
start_vars_[t], lower_bound - duration_min));
return;
}
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(end_vars_[t], lower_bound));
}
@@ -466,12 +480,18 @@ inline void SchedulingConstraintHelper::AddEndMaxReason(
inline void SchedulingConstraintHelper::AddEnergyAfterReason(
int t, IntegerValue energy_min, IntegerValue time) {
AddOtherReason(t);
if (StartMin(t) >= time) {
AddStartMinReason(t, time);
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(start_vars_[t], time));
} else {
AddEndMinReason(t, time + energy_min);
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(end_vars_[t], time + energy_min));
}
if (duration_vars_[t] != kNoIntegerVariable) {
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(duration_vars_[t], energy_min));
}
AddDurationMinReason(t, energy_min);
}
// =============================================================================

23
ortools/sat/linear_constraint.cc
View File

@@ -326,5 +326,28 @@ LinearExpression PositiveVarExpr(const LinearExpression& expr) {
return result;
}
IntegerValue GetCoefficient(const IntegerVariable var,
const LinearExpression& expr) {
for (int i = 0; i < expr.vars.size(); ++i) {
if (expr.vars[i] == var) {
return expr.coeffs[i];
} else if (expr.vars[i] == NegationOf(var)) {
return -expr.coeffs[i];
}
}
return IntegerValue(0);
}
IntegerValue GetCoefficientOfPositiveVar(const IntegerVariable var,
const LinearExpression& expr) {
CHECK(VariableIsPositive(var));
for (int i = 0; i < expr.vars.size(); ++i) {
if (expr.vars[i] == var) {
return expr.coeffs[i];
}
}
return IntegerValue(0);
}
} // namespace sat
} // namespace operations_research

8
ortools/sat/linear_constraint.h
View File

@@ -188,6 +188,14 @@ LinearExpression NegationOf(const LinearExpression& expr);
// Returns the same expression with positive variables.
LinearExpression PositiveVarExpr(const LinearExpression& expr);
// Returns the coefficient of the variable in the expression. Works in linear
// time.
// Note: GetCoefficient(NegationOf(var, expr)) == -GetCoefficient(var, expr).
IntegerValue GetCoefficient(const IntegerVariable var,
const LinearExpression& expr);
IntegerValue GetCoefficientOfPositiveVar(const IntegerVariable var,
const LinearExpression& expr);
} // namespace sat
} // namespace operations_research

56
ortools/sat/linear_relaxation.cc
View File

@@ -13,8 +13,11 @@
#include "ortools/sat/linear_relaxation.h"
#include <vector>
#include "absl/container/flat_hash_set.h"
#include "ortools/base/iterator_adaptors.h"
#include "ortools/base/stl_util.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_loader.h"
#include "ortools/sat/integer.h"
@@ -610,8 +613,8 @@ void AppendMaxRelaxation(IntegerVariable target,
std::vector<IntegerVariable> AppendLinMaxRelaxation(
IntegerVariable target, const std::vector<LinearExpression>& exprs,
Model* model, LinearRelaxation* relaxation) {
// Case X = max(X_1, X_2, ..., X_N)
// Part 1: Encode X >= max(X_1, X_2, ..., X_N)
// We want to linearize X = max(exprs[1], exprs[2], ..., exprs[d]).
// Part 1: Encode X >= max(exprs[1], exprs[2], ..., exprs[d])
for (const LinearExpression& expr : exprs) {
LinearConstraintBuilder lc(model, kMinIntegerValue, -expr.offset);
for (int i = 0; i < expr.vars.size(); ++i) {
@@ -622,6 +625,9 @@ std::vector<IntegerVariable> AppendLinMaxRelaxation(
}
// Part 2: Encode upper bound on X.
// Add linking constraint to the CP solver
// sum zi = 1 and for all i, zi => max = expr_i.
const int num_exprs = exprs.size();
IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
GenericLiteralWatcher* watcher = model->GetOrCreate<GenericLiteralWatcher>();
@@ -650,13 +656,53 @@ std::vector<IntegerVariable> AppendLinMaxRelaxation(
upper_bound->RegisterWith(watcher);
model->TakeOwnership(upper_bound);
AppendEnforcedLinearExpression({z_lit}, local_expr, kMinIntegerValue,
exprs[i].offset, *model, relaxation);
CHECK(lc_exactly_one.AddLiteralTerm(z_lit, IntegerValue(1)));
}
model->Add(ExactlyOneConstraint(z_lits));
// For the relaxation, we use different constraints with a stronger linear
// relaxation as explained in the .h
// TODO(user): Consider passing the x_vars to this method instead of
// computing it here.
std::vector<IntegerVariable> x_vars;
for (int i = 0; i < num_exprs; ++i) {
x_vars.insert(x_vars.end(), exprs[i].vars.begin(), exprs[i].vars.end());
}
gtl::STLSortAndRemoveDuplicates(&x_vars);
// All expressions should only contain positive variables.
DCHECK(std::all_of(x_vars.begin(), x_vars.end(), [](IntegerVariable var) {
return VariableIsPositive(var);
}));
std::vector<std::vector<IntegerValue>> sum_of_max_corner_diff(
num_exprs, std::vector<IntegerValue>(num_exprs, IntegerValue(0)));
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
for (int i = 0; i < num_exprs; ++i) {
for (int j = 0; j < num_exprs; ++j) {
if (i == j) continue;
for (const IntegerVariable x_var : x_vars) {
const IntegerValue lb = integer_trail->LevelZeroLowerBound(x_var);
const IntegerValue ub = integer_trail->LevelZeroUpperBound(x_var);
const IntegerValue diff =
GetCoefficient(x_var, exprs[j]) - GetCoefficient(x_var, exprs[i]);
sum_of_max_corner_diff[i][j] += std::max(diff * lb, diff * ub);
}
}
}
for (int i = 0; i < num_exprs; ++i) {
LinearConstraintBuilder lc(model, kMinIntegerValue, IntegerValue(0));
lc.AddTerm(target, IntegerValue(1));
for (int j = 0; j < exprs[i].vars.size(); ++j) {
lc.AddTerm(exprs[i].vars[j], -exprs[i].coeffs[j]);
}
for (int j = 0; j < num_exprs; ++j) {
CHECK(lc.AddLiteralTerm(z_lits[j],
-exprs[j].offset - sum_of_max_corner_diff[i][j]));
}
relaxation->linear_constraints.push_back(lc.Build());
}
relaxation->linear_constraints.push_back(lc_exactly_one.Build());
return z_vars;
}

18
ortools/sat/linear_relaxation.h
View File

@@ -95,7 +95,23 @@ void AppendMaxRelaxation(IntegerVariable target,
LinearRelaxation* relaxation);
// Adds linearization of int max constraints. Returns a vector of z vars such
// that: z_vars[i] == 1 <=> target = exprs[i].
// that: z_vars[l] == 1 <=> target = exprs[l].
//
// Consider the Lin Max constraint with d expressions and n variables in the
// form: target = max {exprs[l] = Sum (wli * xi + bl)}. l in {1,..,d}.
// Li = lower bound of xi
// Ui = upper bound of xi.
// Let zl be in {0,1} for all l in {1,..,d}.
// The target = exprs[l] when zl = 1.
//
// The following is a valid linearization for Lin Max.
// target >= exprs[l], for all l in {1,..,d}
// target <= Sum_i(wki * xi) + Sum_l((Nkl + bl) * zl), for all k in {1,..,d}
// Where Nkl is a large number defined as:
// Nkl = Sum_i(max((wli - wki)*Li, (wli - wki)*Ui))
// = Sum (max corner difference for variable i, target expr k, max expr l)
// Reference: "Strong mixed-integer programming formulations for trained neural
// networks" by Ross Anderson et. (https://arxiv.org/pdf/1811.01988.pdf).
// TODO(user): Support linear expression as target.
std::vector<IntegerVariable> AppendLinMaxRelaxation(
IntegerVariable target, const std::vector<LinearExpression>& exprs,

33
ortools/sat/presolve_context.cc
View File

@@ -147,6 +147,12 @@ bool PresolveContext::VariableIsUniqueAndRemovable(int ref) const {
!keep_all_feasible_solutions;
}
bool PresolveContext::VariableIsNotUsedAnymore(int ref) const {
if (!ConstraintVariableGraphIsUpToDate()) return false;
return var_to_constraints[PositiveRef(ref)].empty() &&
VariableIsNotRepresentativeOfEquivalenceClass(ref);
}
bool PresolveContext::VariableWithCostIsUniqueAndRemovable(int ref) const {
if (!ConstraintVariableGraphIsUpToDate()) return false;
const int var = PositiveRef(ref);
@@ -359,6 +365,14 @@ void PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) {
return;
}
const int var_a = PositiveRef(ref_a);
const int var_b = PositiveRef(ref_b);
if (GetAffineRelation(var_a).representative == var_b ||
GetAffineRelation(var_b).representative == var_a) {
return;
}
// For now, we do need to add the relation ref_a == ref_b so we have a
// proper variable usage count and propagation between ref_a and ref_b.
//
@@ -367,24 +381,21 @@ void PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) {
// define them around.
ConstraintProto* ct = working_model->add_constraints();
auto* arg = ct->mutable_linear();
arg->add_vars(PositiveRef(ref_a));
arg->add_vars(PositiveRef(ref_b));
arg->add_vars(var_a);
arg->add_coeffs(1);
arg->add_vars(var_b);
if (RefIsPositive(ref_a) == RefIsPositive(ref_b)) {
// a = b
arg->add_coeffs(1);
arg->add_coeffs(-1);
arg->add_domain(0);
arg->add_domain(0);
StoreAffineRelation(*ct, PositiveRef(ref_a), PositiveRef(ref_b), 1,
/*offset=*/0);
StoreAffineRelation(*ct, var_a, var_b, /*coeff=*/1, /*offset=*/0);
} else {
// a = 1 - b
arg->add_coeffs(1);
arg->add_coeffs(1);
arg->add_domain(1);
arg->add_domain(1);
StoreAffineRelation(*ct, PositiveRef(ref_a), PositiveRef(ref_b), -1,
/*offset=*/1);
StoreAffineRelation(*ct, var_a, var_b, /*coeff=*/-1, /*offset=*/1);
}
UpdateNewConstraintsVariableUsage();
}
@@ -480,6 +491,10 @@ void PresolveContext::InsertVarValueEncoding(int literal, int ref,
} else {
encoding[other_key] = NegatedRef(literal);
// Add affine relation.
// TODO(user): In linear presolve, recover var-value encoding from
// linear constraints like the one created below. This would be
// useful in case the variable has an affine representative, and the
// below constraint is rewritten.
ConstraintProto* const ct = working_model->add_constraints();
LinearConstraintProto* const lin = ct->mutable_linear();
lin->add_vars(var);
@@ -578,7 +593,7 @@ bool PresolveContext::HasVarValueEncoding(int ref, int64 value, int* literal) {
const auto& it = encoding.find(key);
if (it != encoding.end()) {
if (literal != nullptr) {
*literal = it->second;
*literal = GetLiteralRepresentative(it->second);
}
return true;
} else {

3
ortools/sat/presolve_context.h
View File

@@ -80,6 +80,9 @@ class PresolveContext {
// Returns true if this ref only appear in one constraint.
bool VariableIsUniqueAndRemovable(int ref) const;
// Returns true if this ref no longer appears in the model.
bool VariableIsNotUsedAnymore(int ref) const;
// Same as VariableIsUniqueAndRemovable() except that in this case the
// variable also appear in the objective in addition to a single constraint.
bool VariableWithCostIsUniqueAndRemovable(int ref) const;

6
ortools/sat/sat_parameters.proto
View File

@@ -21,7 +21,7 @@ option java_multiple_files = true;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 153
// NEXT TAG: 154
message SatParameters {
// ==========================================================================
// Branching and polarity
@@ -643,6 +643,10 @@ message SatParameters {
}
optional SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH];
// When we try to follow the hint, we do a FIXED_SEARCH using the hint until
// this number of conflict is reached.
optional int32 hint_conflict_limit = 153 [default = 10];
// All the "exploit_*" parameters below work in the same way: when branching
// on an IntegerVariable, these parameters affect the value the variable is
// branched on. Currently the first heuristic that triggers win in the order

9
ortools/sat/synchronization.cc
View File

@@ -322,7 +322,6 @@ void SharedResponseManager::FillObjectiveValuesInBestResponse() {
void SharedResponseManager::NewSolution(const CpSolverResponse& response,
Model* model) {
absl::MutexLock mutex_lock(&mutex_);
CHECK_NE(best_response_.status(), CpSolverStatus::INFEASIBLE);
if (model_proto_.has_objective()) {
const int64 objective_value =
@@ -338,10 +337,14 @@ void SharedResponseManager::NewSolution(const CpSolverResponse& response,
}
// Ignore any non-strictly improving solution.
// We also perform some basic checks on the inner bounds.
DCHECK_GE(objective_value, inner_objective_lower_bound_);
if (objective_value > inner_objective_upper_bound_) return;
// Our inner_objective_upper_bound_ should be a globaly valid bound, until
// the problem become infeasible (i.e the lb > ub) in which case the bound
// is no longer globally valid. Here, because we have a strictly improving
// solution, we shouldn't be in the infeasible setting yet.
DCHECK_GE(objective_value, inner_objective_lower_bound_);
DCHECK_LT(objective_value, best_solution_objective_value_);
DCHECK_NE(best_response_.status(), CpSolverStatus::OPTIMAL);
best_solution_objective_value_ = objective_value;

130
ortools/sat/timetable.cc
View File

@@ -43,31 +43,18 @@ TimeTablingPerTask::TimeTablingPerTask(
backward_num_tasks_to_sweep_ = num_tasks_;
backward_tasks_to_sweep_.resize(num_tasks_);
num_active_tasks_ = num_tasks_;
active_tasks_.resize(num_tasks_);
num_profile_tasks_ = 0;
profile_tasks_.resize(num_tasks_);
positions_in_profile_tasks_.resize(num_tasks_);
// Reversible bounds and starting height of the profile.
starting_profile_height_ = IntegerValue(0);
left_start_ = 0;
left_end_ = 0;
right_start_ = num_tasks_;
right_end_ = num_tasks_;
// Vector of tasks to sort to build the profile.
by_start_max_.resize(num_tasks_);
by_end_min_.resize(num_tasks_);
for (int t = 0; t < num_tasks_; ++t) {
forward_tasks_to_sweep_[t] = t;
backward_tasks_to_sweep_[t] = t;
active_tasks_[t] = t;
profile_tasks_[t] = t;
positions_in_profile_tasks_[t] = t;
by_start_max_[t].task_index = t;
by_end_min_[t].task_index = t;
}
}
@@ -78,18 +65,12 @@ void TimeTablingPerTask::RegisterWith(GenericLiteralWatcher* watcher) {
for (int t = 0; t < num_tasks_; t++) {
watcher->WatchLowerBound(demands_[t].var, id);
}
// Repositories responsible for restoring the reversible values.
watcher->RegisterReversibleClass(id, &rev_repository_int_);
watcher->RegisterReversibleClass(id, &rev_repository_integer_value_);
watcher->RegisterReversibleInt(id, &forward_num_tasks_to_sweep_);
watcher->RegisterReversibleInt(id, &backward_num_tasks_to_sweep_);
watcher->RegisterReversibleInt(id, &num_profile_tasks_);
}
bool TimeTablingPerTask::Propagate() {
// Save the current state of the set of tasks.
rev_repository_int_.SaveState(&forward_num_tasks_to_sweep_);
rev_repository_int_.SaveState(&backward_num_tasks_to_sweep_);
rev_repository_int_.SaveState(&num_active_tasks_);
rev_repository_int_.SaveState(&num_profile_tasks_);
// Repeat until the propagator does not filter anymore.
profile_changed_ = true;
while (profile_changed_) {
@@ -104,11 +85,6 @@ bool TimeTablingPerTask::Propagate() {
if (!SweepAllTasks(/*is_forward=*/false)) return false;
}
// Reduce the profile now that we know that it is stable.
// TODO(user): something seems to be wrong we the reduction. To reactivate
// once we'll have understood (and fixed) the behavior.
if (false) ReduceProfile();
return true;
}
@@ -131,21 +107,8 @@ bool TimeTablingPerTask::BuildProfile() {
}
}
// Update start value of active tasks.
for (int i = left_start_; i < right_start_; ++i) {
by_start_max_[i].time = helper_->StartMax(by_start_max_[i].task_index);
}
// Likely to be already or almost sorted.
IncrementalSort(by_start_max_.begin() + left_start_,
by_start_max_.begin() + right_start_);
// Update end value of active tasks.
for (int i = left_end_; i < right_end_; ++i) {
by_end_min_[i].time = helper_->EndMin(by_end_min_[i].task_index);
}
// Likely to be already or almost sorted.
IncrementalSort(by_end_min_.begin() + left_end_,
by_end_min_.begin() + right_end_);
const auto& by_decreasing_start_max = helper_->TaskByDecreasingStartMax();
const auto& by_end_min = helper_->TaskByIncreasingEndMin();
// Build the profile.
// ------------------
@@ -164,26 +127,26 @@ bool TimeTablingPerTask::BuildProfile() {
// Next start/end of the compulsory parts to be processed. Note that only the
// task for which IsInProfile() is true must be considered.
int next_start = left_start_;
int next_end = left_end_;
while (next_end < right_end_) {
int next_start = num_tasks_ - 1;
int next_end = 0;
while (next_end < num_tasks_) {
const IntegerValue old_height = current_height;
IntegerValue t = by_end_min_[next_end].time;
if (next_start < right_start_) {
t = std::min(t, by_start_max_[next_start].time);
IntegerValue t = by_end_min[next_end].time;
if (next_start >= 0) {
t = std::min(t, by_decreasing_start_max[next_start].time);
}
// Process the starting compulsory parts.
while (next_start < right_start_ && by_start_max_[next_start].time == t) {
const int task_index = by_start_max_[next_start].task_index;
while (next_start >= 0 && by_decreasing_start_max[next_start].time == t) {
const int task_index = by_decreasing_start_max[next_start].task_index;
if (IsInProfile(task_index)) current_height += DemandMin(task_index);
++next_start;
--next_start;
}
// Process the ending compulsory parts.
while (next_end < right_end_ && by_end_min_[next_end].time == t) {
const int task_index = by_end_min_[next_end].task_index;
while (next_end < num_tasks_ && by_end_min[next_end].time == t) {
const int task_index = by_end_min[next_end].task_index;
if (IsInProfile(task_index)) current_height -= DemandMin(task_index);
++next_end;
}
@@ -210,67 +173,6 @@ bool TimeTablingPerTask::BuildProfile() {
return IncreaseCapacity(max_height_start, profile_max_height_);
}
// TODO(user): calling this function currently have an impact on the search.
// This should not be the case and might be the symptom of a larger bug.
void TimeTablingPerTask::ReduceProfile() {
helper_->SetTimeDirection(true); // forward
IntegerValue min_start_min = kMaxIntegerValue;
IntegerValue max_end_max = kMinIntegerValue;
// TODO(user): we could probably go a step further by considering tasks
// that only have a fixed demand and start (resp. end) variables. The idea is
// that the start of their mandatory part is not going to change and could
// already be aggregated in starting_profile_height_.
for (int i = num_active_tasks_ - 1; i >= 0; --i) {
const int t = active_tasks_[i];
// Discard absent and fixed tasks.
if (helper_->IsAbsent(t) ||
(helper_->StartMin(t) == helper_->StartMax(t) &&
helper_->EndMin(t) == helper_->EndMax(t) &&
DemandMin(t) == DemandMax(t) && helper_->IsPresent(t))) {
std::swap(active_tasks_[i], active_tasks_[--num_active_tasks_]);
continue;
}
min_start_min = std::min(min_start_min, helper_->StartMin(t));
max_end_max = std::max(max_end_max, helper_->EndMax(t));
}
// Save the current state of the reversible values.
rev_repository_integer_value_.SaveState(&starting_profile_height_);
rev_repository_int_.SaveState(&left_start_);
rev_repository_int_.SaveState(&left_end_);
rev_repository_int_.SaveState(&right_start_);
rev_repository_int_.SaveState(&right_end_);
// Update the range of active tasks in their corresponding sorted vectors.
while (left_start_ < right_start_ &&
by_start_max_[left_start_].time < min_start_min) {
const int t = by_start_max_[left_start_].task_index;
if (helper_->IsPresent(t)) starting_profile_height_ += DemandMin(t);
left_start_++;
}
while (left_end_ < right_end_ &&
by_end_min_[left_end_].time < min_start_min) {
const int t = by_end_min_[left_end_].task_index;
if (helper_->IsPresent(t)) starting_profile_height_ -= DemandMin(t);
left_end_++;
}
while (left_start_ < right_start_ &&
max_end_max < by_start_max_[right_start_ - 1].time) {
right_start_--;
}
while (left_end_ < right_end_ &&
max_end_max < by_end_min_[right_end_ - 1].time) {
right_end_--;
}
DCHECK_GE(starting_profile_height_, 0);
}
void TimeTablingPerTask::ReverseProfile() {
helper_->SetTimeDirection(false); // backward

32
ortools/sat/timetable.h
View File

@@ -55,14 +55,6 @@ class TimeTablingPerTask : public PropagatorInterface {
// variable accordingly.
bool BuildProfile();
// Reduces the set of tasks to be considered by BuildProfile(). This is done
// by not considering parts of mandatory part that are overlaped by no task.
// The set of tasks to consider is restored to its previous state each time a
// backtrack occurs. This function must be called only if the by_start_max_
// and by_end_min_ vectors are up to date and if the profile contains no
// profile rectangle that can exceed the capacity of the resource.
void ReduceProfile();
// Reverses the profile. This is needed to reuse a given profile to update
// both the start and end times.
void ReverseProfile();
@@ -121,25 +113,6 @@ class TimeTablingPerTask : public PropagatorInterface {
IntegerTrail* integer_trail_;
SchedulingConstraintHelper* helper_;
RevRepository<int> rev_repository_int_;
RevRepository<IntegerValue> rev_repository_integer_value_;
// Vector of tasks sorted by maximum starting (resp. minimum ending) time.
std::vector<TaskTime> by_start_max_;
std::vector<TaskTime> by_end_min_;
// Tasks contained in the range [left_start_, right_start_) of by_start_max_
// must be sorted and considered when building the profile. The state of these
// bounds is restored when a backtrack occurs.
int left_start_;
int right_start_;
// Tasks contained in the range [left_end_, right_end_) of by_end_min_ must be
// sorted and considered when building the profile. The state of these bounds
// is restored when a backtrack occurs.
int left_end_;
int right_end_;
// Optimistic profile of the resource consumption over time.
std::vector<ProfileRectangle> profile_;
IntegerValue profile_max_height_;
@@ -161,11 +134,6 @@ class TimeTablingPerTask : public PropagatorInterface {
int forward_num_tasks_to_sweep_;
int backward_num_tasks_to_sweep_;
// Reversible set of tasks to consider for reducing the profile. The set
// contains the [0, num_active_tasks_) prefix of active_tasks_.
std::vector<int> active_tasks_;
int num_active_tasks_;
// Reversible set (with random access) of tasks to consider for building the
// profile. The set contains the tasks in the [0, num_profile_tasks_) prefix
// of profile_tasks_. The positions of a task in profile_tasks_ is contained