CP-SAT and incremental usage under assumptions: possible?

[s schnug]

Task

Let's assume i got some CP-SAT model, which is not pure boolean and contains for example *NoOverlap* and other *global* constraints (e.g. *Circuit*). 

The problem to tackle might look like some jobshop problem (as feasibility problem) and we have some selector-variable for all of our jobs: the model is basically only enforcing the jobshop constraints if the selector-variable is true; a bit hacky, non-selected jobs are allowed to be pushed outside the time-windows.

The task, after recognizing unfeasibility is to obtain a variable-MUS in terms of our selector variables.

General approach

The naive idea/approach could be a deletion-based algorithm working on the assumption-paradigm. We incrementally check each variable for necessity (variable-selector is assumed) and fix this assumption or it's negation depending on the Solver-Status.

The hope is to gain from incremental-usage.

(If working, a later version could also re-use unsat-cores as done in other parts of or-tools)

Feasibility and Implementation

The question is now: is this something doable (or invalidating all kinds of assumptions of the LCG-core)? It should be on a pure SAT-problem, but things get more complex in the LCG-world i assume.

In terms of or-tools code i would assume we would work on a general model and not for example on some *LinearBooleanProblem* (like the Fu-Malik implementation and many others).

On one hand, *MinimizeIntegerVariableWithLinearScanAndLazyEncoding* (general problem) looks similar and incremental, on the other hand, *MinimizeWithHittingSetAndLazyEncoding*'s implementation states:

     // TODO(user): Even though we keep the same solver, currently the solve is
     // not really done incrementally. It might be hard to improve though

So i'm unsure about the general feasibility.

Things tried

(working on ff93cfbb9781b9ae31ef9b511f450aee3d1d27cc; master from Jun 18, 2019)

I'm still early in my experiments and prepared the model (through Proto) to introduce some new model-component: variable-mus. This mimics an objective, but consumes Boolean Variables / Literals.

The basic outer-layer (caring about presolve) machinery works, so that the model is now hitting my custom optimizer in *optimization.cc*.

Then things start to fall apart, maybe because i'm invalidating invariants. Maybe it's just something more simple (resulting in segfaults).

The code, as simple as:

    SatSolver::Status FindVmusDeletion(
            const std::vector<Literal>& boolean_vars,
            const std::function<void()>& feasible_solution_observer,
            Model* model) {
       
        LOG(INFO) << "VMUS";


        // pass 1: solve under assumption: all Vmus-vars true
        //    -> reasoning about general SAT / UNSAT nature
        SatSolver* sat_solver = model->GetOrCreate<SatSolver>();


        sat_solver->SetAssumptionLevel(0);


        std::vector<Literal> assumptions(boolean_vars);


        std::string s;
        for(int i=0; i<assumptions.size(); ++i) {
            s += assumptions[i].DebugString();
        }
        LOG(INFO) << "assumptions: " << s;
        // remark: correct literals seen here


        const SatSolver::Status result =
                sat_solver->ResetAndSolveWithGivenAssumptions(assumptions);


        LOG(INFO) << "solve ok " << s;
       //remark: not reached due to crash

will crash within *ReapplyDecisionsUpTo* or later.

Replacing it with 

    const SatSolver::Status result = sat_solver->Solve();

works (at least not crashing) although my missing work in *synchronization.h* results in some wrong propagation of the status. 

Interesting fact: doing the same with for example the first literal only (assumption size = 1) of *assumptions* will run. But using all (20; in this case) will crash.

What worries me, is that the crash emerges deeply in the SAT-core. The trace looks like:

SolveWithParameters(...)
SolveCpModel(...)
SolveLoadedCpModel(...)
FindVmusDeletion(...)
SatSolver::ResetAndSolveWithGivenAssumptions(...)
SatSolver::ResetWithGivenAssumptions(...)
SatSolver::ReapplyAssumptionsIfNeeded(...)
SatSolver::ReapplyDecisionsUpTo(...)
SatSolver::EnqueueDecisionsAndBackjumpOnConflictResolution(...)
SatSolver::PropagateAndStopAfterOneConflictResolution(...)
SatSolver::Propagate()
LiteralWatchers::Propagate(...)
LiteralWatchers::PropagateOnFalse(...)
- crash -

This code is called from *cp_model_solver.cc* which was modified like (partial code):

    SatSolver::Status status;

    ConfigureSearchHeuristics(fixed_search, model);

    // MY CHANGES

    -------------

    if(model_proto.has_vmus()) {

            VLOG(1) << "HMM";

            // Vmus problem.

        const CpVmusProto& obj = model_proto.vmus();

        VLOG(2) << obj.literals_size() << " literals in the proto vmus.";

         std::vector<Literal> boolean_vars;

        ExtractVmus(model_proto, &boolean_vars);

        status = FindVmusDeletion(boolean_vars, solution_observer, model);

    }

    else {

    // HANDLE ORIGINAL CODE-PATHS

    if (!model_proto.has_objective()) {

        while (true) {

        status = ResetAndSolveIntegerProblem(/*assumptions=*/{}, model);

        if (status != SatSolver::Status::FEASIBLE) break;

        solution_observer();

        if (!parameters.enumerate_all_solutions()) break;

        model->Add(ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack());

        }

        if (status == SatSolver::INFEASIBLE) {

        shared_response_manager->NotifyThatImprovingProblemIsInfeasible(

            solution_info);

        }

    } else {

        // Optimization problem.

        const CpObjectiveProto& obj = model_proto.objective();

        VLOG(2) << obj.vars_size() << " terms in the proto objective.";

        VLOG(2) << "Initial num_bool: " << model->Get<SatSolver>()->NumVariables();

        if (parameters.optimize_with_core()) {

        std::vector<IntegerVariable> linear_vars;

        std::vector<IntegerValue> linear_coeffs;

        ExtractLinearObjective(model_proto, *model->GetOrCreate<CpModelMapping>(),

                                &linear_vars, &linear_coeffs);

        if (parameters.optimize_with_max_hs()) {

            status = MinimizeWithHittingSetAndLazyEncoding(

                objective_var, linear_vars, linear_coeffs, solution_observer,

                model);

        } else {

            CoreBasedOptimizer core(objective_var, linear_vars, linear_coeffs,

                                    solution_observer, model);

            status = core.Optimize();

        }

        } else {

        if (parameters.binary_search_num_conflicts() >= 0) {

            RestrictObjectiveDomainWithBinarySearch(objective_var,

                                                    solution_observer, model);

        }

        status = MinimizeIntegerVariableWithLinearScanAndLazyEncoding(

            objective_var, solution_observer, model);

        }

        }

    }
    ...

I'm not sure how to proceed from here. Any ideas about the general feasibility of the idea? And if so: any tips about the general implementation steps?

Maybe i'm on the wrong path working in *optimization.cc* (with my general global-constraint based model) as the deader says:

    // Optimization algorithms to solve a LinearBooleanProblem by using the SAT
    // solver as a black-box.

Maybe *Bop* is the source-code part i must look at, but things are intertwined a lot (including inline comments about potential refactorization in the future).

General development

Can i also ask about how or-tools is developed (which stack)?

I'm having *some* trouble using Eclipse-CDT on Linux, but maybe Visual Studio is more suited? Maybe i'm blind, but i don't see any IDE configuration files in the repository (maybe i'm wrong).

I'm currently only using it's C++ indexing capabilities (outsourcing building) and some classes are lost, like for example LinearBooleanProblem which is indexed correctly for some files, but missing in others. Not sure what the problem is and debugging this is not that important right now.

Another more simple question: Can i modify my:

    make build SOURCE=/ortoolsExampleProblem/multi_knapsack_sat.cc

to be a DEBUG-build? (Linux environment)

[s schnug]

No ideas to help me out here?

I could imagine, that someone knowing the internals of the solver might think about some usage-errors / invariant-breaking things, resulting in such behaviour (as observed), maybe even having some feeling about potential misinterpretations for someone trying to modify the code.

It's hard to proceed without knowing if there are obvious mistakes in the workflow(-assumptions) or more complex difficulties are observed (maybe even things which should not happen).

[fulin xie]

I recently started using or-tool, and have got same question. Have you figured out how to build in debug mode, so I can trace the process in gdb? Many thanks,

[fulin xie]

I recently started using or-tool, and have got same question. Have you figured out how to build in debug mode, so I can trace the process in gdb? Many thanks,

On Saturday, 29 June 2019 15:07:36 UTC+1, s schnug wrote:

[Laurent Perron]

Hi

To compile in debug, 

make DEBUG="-g" ...

"-g" on linux or mac

"/Zi /Od" on windows.

About assumptions, we are working on adding assumptions at the cp_model.proto level. But it will not happen soon. 

As you said, the code is complex.

The main idea would be to have a set of booleans that controls part of the models. Solving with assumptions would first try to enforce all assumptions and solve normally.

If the model is infeasible, it would heuristically try to find a minimal set of assumptions to negate to make the model feasible.

Please note that this works for LCG model too. The only constraint is that assumptions have to be literals.

But this will not happen soon.

--
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/3fea9c45-1013-4418-8648-cbbd4b9adcf3%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

--Laurent