Home
last modified time | relevance | path

Searched refs:sat_solver_ (Results 1 – 22 of 22) sorted by relevance

/dports/math/py-or-tools/or-tools-9.2/ortools/sat/
H A Dlb_tree_search.cc26 sat_solver_(model->GetOrCreate<SatSolver>()), in LbTreeSearch()
134 if (!sat_solver_->RestoreSolverToAssumptionLevel()) { in Search()
135 return sat_solver_->UnsatStatus(); in Search()
165 CHECK(sat_solver_->Assignment().LiteralIsAssigned( in Search()
243 if (!sat_solver_->RestoreSolverToAssumptionLevel()) { in Search()
244 return sat_solver_->UnsatStatus(); in Search()
265 sat_solver_->Backtrack( in Search()
267 if (!sat_solver_->FinishPropagation()) { in Search()
268 return sat_solver_->UnsatStatus(); in Search()
273 return sat_solver_->UnsatStatus(); in Search()
[all …]
H A Dprobing.cc39 sat_solver_(model->GetOrCreate<SatSolver>()), in Prober()
45 const int num_variables = sat_solver_->NumVariables(); in ProbeBooleanVariables()
63 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); in ProbeOneVariableInternal()
66 sat_solver_->AdvanceDeterministicTime(time_limit_); in ProbeOneVariableInternal()
68 if (sat_solver_->IsModelUnsat()) return false; in ProbeOneVariableInternal()
97 sat_solver_->AddUnitClause(l); in ProbeOneVariableInternal()
100 if (!sat_solver_->FinishPropagation()) return false; in ProbeOneVariableInternal()
106 if (!sat_solver_->FinishPropagation()) return false; in ProbeOneVariableInternal()
178 return sat_solver_->FinishPropagation(); in ProbeOneVariableInternal()
192 sat_solver_->SetAssumptionLevel(0); in ProbeOneVariable()
[all …]
H A Dinteger.cc52 CHECK_EQ(0, sat_solver_->CurrentDecisionLevel()); in FullyEncodeVariable()
122 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); in PartialDomainEncoding()
173 sat_solver_->AddClauseDuringSearch( in AddImplications()
181 sat_solver_->AddClauseDuringSearch( in AddImplications()
187 CHECK_EQ(0, sat_solver_->CurrentDecisionLevel()); in AddAllImplicationsBetweenAssociatedLiterals()
306 sat_solver_->AddUnitClause(literal); in AssociateToIntegerLiteral()
308 sat_solver_->AddUnitClause(literal.Negated()); in AssociateToIntegerLiteral()
358 DCHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); in AssociateToIntegerEqualValue()
367 sat_solver_->AddUnitClause(literal.Negated()); in AssociateToIntegerEqualValue()
384 sat_solver_->AddUnitClause(literal); in AssociateToIntegerEqualValue()
[all …]
H A Dinteger_search.cc767 sat_solver_(model->GetOrCreate<SatSolver>()), in IntegerSearchHelper()
784 sat_solver_->Backtrack(0); in BeforeTakingDecision()
785 if (!sat_solver_->RestoreSolverToAssumptionLevel()) { in BeforeTakingDecision()
790 if (sat_solver_->CurrentDecisionLevel() == 0) { in BeforeTakingDecision()
792 sat_solver_->NotifyThatModelIsUnsat(); in BeforeTakingDecision()
799 sat_solver_->NotifyThatModelIsUnsat(); in BeforeTakingDecision()
806 sat_solver_->NotifyThatModelIsUnsat(); in BeforeTakingDecision()
874 const int old_level = sat_solver_->CurrentDecisionLevel(); in TakeDecision()
887 if (sat_solver_->CurrentDecisionLevel() > old_level && in TakeDecision()
896 sat_solver_->AdvanceDeterministicTime(time_limit_); in TakeDecision()
[all …]
H A Dimplied_bounds.h83 sat_solver_(model->GetOrCreate<SatSolver>()), in ImpliedBounds()
154 SatSolver* sat_solver_; variable
H A Dfeasibility_pump.cc45 sat_solver_(model->GetOrCreate<SatSolver>()), in FeasibilityPump()
551 sat_solver_->ResetToLevelZero(); in PropagationRounding()
661 if (!sat_solver_->FinishPropagation()) { in PropagationRounding()
665 sat_solver_->EnqueueDecisionAndBacktrackOnConflict(to_enqueue); in PropagationRounding()
667 if (sat_solver_->IsModelUnsat()) { in PropagationRounding()
672 sat_solver_->ResetToLevelZero(); in PropagationRounding()
H A Dsat_inprocessing.cc65 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); in PresolveLoop()
131 << "/" << sat_solver_->NumVariables() in PresolveLoop()
184 sat_solver_->MinimizeSomeClauses(/*decisions_budget=*/1000); in InprocessingRound()
199 << "/" << sat_solver_->NumVariables() in InprocessingRound()
224 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); in LevelZeroPropagate()
226 return sat_solver_->Propagate(); in LevelZeroPropagate()
259 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); in RemoveFixedAndEquivalentVariables()
290 const int num_literals(sat_solver_->NumVariables() * 2); in RemoveFixedAndEquivalentVariables()
391 const LiteralIndex num_literals(sat_solver_->NumVariables() * 2); in SubsumeAndStrenghtenRound()
H A Dprobing.h83 SatSolver* sat_solver_; variable
H A Dsat_inprocessing.h98 sat_solver_(model->GetOrCreate<SatSolver>()), in Inprocessing()
143 SatSolver* sat_solver_; variable
H A Dimplied_bounds.cc200 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 1); in ProcessIntegerTrail()
230 CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0); in EnqueueNewDeductions()
240 return sat_solver_->FinishPropagation(); in EnqueueNewDeductions()
H A Dlb_tree_search.h102 SatSolver* sat_solver_; variable
H A Dfeasibility_pump.h202 SatSolver* sat_solver_; variable
H A Doptimization.h191 SatSolver* sat_solver_; variable
H A Dinteger_search.h255 SatSolver* sat_solver_; variable
H A Dinteger.h359 : sat_solver_(model->GetOrCreate<SatSolver>()), in IntegerEncoder()
518 DCHECK_EQ(0, sat_solver_->CurrentDecisionLevel()); in GetTrueLiteral()
521 Literal(sat_solver_->NewBooleanVariable(), true); in GetTrueLiteral()
523 sat_solver_->AddUnitClause(literal_true); in GetTrueLiteral()
557 SatSolver* sat_solver_; variable
H A Doptimization.cc1316 sat_solver_(model->GetOrCreate<SatSolver>()), in CoreBasedOptimizer()
1374 sat_solver_->Backtrack(0); in ProcessSolution()
1375 sat_solver_->SetAssumptionLevel(0); in ProcessSolution()
1385 if (!sat_solver_->ResetToLevelZero()) return false; in PropagateObjectiveBounds()
1518 if (!sat_solver_->ResetToLevelZero()) return false; in CoverOptimization()
1683 if (!sat_solver_->ResetToLevelZero()) return SatSolver::INFEASIBLE; in Optimize()
/dports/math/py-or-tools/or-tools-9.2/ortools/bop/
H A Dbop_fs.cc85 sat_solver_() {} in GuidedSatFirstSolutionGenerator()
97 if (!sat_solver_) { in SynchronizeIfNeeded()
98 sat_solver_ = absl::make_unique<sat::SatSolver>(); in SynchronizeIfNeeded()
111 sat_solver_->AddPropagator(propagator.get()); in SynchronizeIfNeeded()
112 sat_solver_->TakePropagatorOwnership(std::move(propagator)); in SynchronizeIfNeeded()
126 sat_solver_->SetAssignmentPreference( in SynchronizeIfNeeded()
133 sat_solver_.get()); in SynchronizeIfNeeded()
137 sat_solver_->SetAssignmentPreference( in SynchronizeIfNeeded()
182 sat_solver_->SetParameters(sat_params); in Optimize()
185 const sat::SatSolver::Status sat_status = sat_solver_->Solve(); in Optimize()
[all …]
H A Dbop_lns.cc73 sat_solver_ = absl::make_unique<sat::SatSolver>(); in SynchronizeIfNeeded()
75 LoadStateProblemToSatSolver(problem_state, sat_solver_.get()); in SynchronizeIfNeeded()
95 sat_solver_->AddLinearConstraint( in SynchronizeIfNeeded()
99 if (sat_solver_->IsModelUnsat()) return BopOptimizerBase::ABORT; in SynchronizeIfNeeded()
105 sat_solver_.get()); in SynchronizeIfNeeded()
128 CHECK(sat_solver_ != nullptr); in Optimize()
129 const double initial_dt = sat_solver_->deterministic_time(); in Optimize()
131 time_limit->AdvanceDeterministicTime(sat_solver_->deterministic_time() - in Optimize()
145 sat_solver_->SetParameters(sat_params); in Optimize()
146 const sat::SatSolver::Status sat_status = sat_solver_->Solve(); in Optimize()
[all …]
H A Dbop_ls.cc626 void SatWrapper::BacktrackAll() { sat_solver_->Backtrack(0); }
630 const sat::Trail& trail = sat_solver_->LiteralTrail();
639 CHECK(!sat_solver_->Assignment().VariableIsAssigned( in UL_HARQ_IR_CTC_Sub_Burst_IE()
644 const int old_decision_level = sat_solver_->CurrentDecisionLevel(); in UL_HARQ_IR_CTC_Sub_Burst_IE()
647 if (sat_solver_->IsModelUnsat()) { in UL_HARQ_IR_CTC_Sub_Burst_IE()
654 const sat::Trail& propagation_trail = sat_solver_->LiteralTrail(); in UL_HARQ_IR_CTC_Sub_Burst_IE()
660 return old_decision_level + 1 - sat_solver_->CurrentDecisionLevel(); in UL_HARQ_IR_CTC_Sub_Burst_IE()
664 const int old_decision_level = sat_solver_->CurrentDecisionLevel();
666 sat_solver_->Backtrack(old_decision_level - 1);
671 bop::ExtractLearnedInfoFromSatSolver(sat_solver_, info);
[all …]
H A Dbop_ls.h63 bool IsModelUnsat() const { return sat_solver_->IsModelUnsat(); }
67 return sat_solver_->Assignment();
98 sat::SatSolver* sat_solver_;
H A Dbop_fs.h69 std::unique_ptr<sat::SatSolver> sat_solver_; variable
H A Dbop_lns.h59 std::unique_ptr<sat::SatSolver> sat_solver_; variable