23#include "llvm/ADT/ArrayRef.h"
24#include "llvm/ADT/DenseMap.h"
25#include "llvm/ADT/DenseSet.h"
26#include "llvm/ADT/SmallVector.h"
27#include "llvm/ADT/STLExtras.h"
139 llvm::DenseMap<Variable, Atom>
Atomics)
145 const size_t NumLiterals = 2 *
LargestVar + 1;
156 assert(!lits.empty());
157 assert(llvm::all_of(lits, [](
Literal L) {
return L !=
NullLit; }));
160 const size_t S =
Clauses.size();
207 assert(!Literals.empty() && Literals.size() <= 3);
210 for (
auto L : Literals) {
212 llvm::all_of(Simplified,
213 [L](
Literal S) {
return S != L; }));
215 if (trueVars.contains(
X)) {
221 if (falseVars.contains(
X)) {
227 Simplified.push_back(L);
229 if (Simplified.empty()) {
232 Formula.KnownContradictory =
true;
234 Formula.addClause(Literals[0]);
237 if (Simplified.size() == 1) {
239 const Literal lit = Simplified.front();
269 llvm::DenseMap<const Formula *, Variable> SubValsToVar;
271 llvm::DenseMap<Variable, Atom> Atomics;
274 std::queue<const Formula *> UnprocessedSubVals;
275 for (
const Formula *Val : Vals)
276 UnprocessedSubVals.push(Val);
277 while (!UnprocessedSubVals.empty()) {
279 const Formula *Val = UnprocessedSubVals.front();
280 UnprocessedSubVals.pop();
282 if (!SubValsToVar.try_emplace(Val, Var).second)
287 UnprocessedSubVals.push(F);
293 auto GetVar = [&SubValsToVar](
const Formula *Val) {
294 auto ValIt = SubValsToVar.find(Val);
295 assert(ValIt != SubValsToVar.end());
296 return ValIt->second;
299 CNFFormula CNF(NextVar - 1, std::move(Atomics));
300 std::vector<bool> ProcessedSubVals(NextVar,
false);
305 for (
const Formula *Val : Vals)
310 std::queue<const Formula *> UnprocessedSubVals;
311 for (
const Formula *Val : Vals)
312 UnprocessedSubVals.push(Val);
313 while (!UnprocessedSubVals.empty()) {
314 const Formula *Val = UnprocessedSubVals.front();
315 UnprocessedSubVals.pop();
318 if (ProcessedSubVals[Var])
320 ProcessedSubVals[Var] =
true;
322 switch (Val->
kind()) {
419 UnprocessedSubVals.push(Child);
466 std::vector<Variable> LevelVars;
469 enum class State : uint8_t {
482 std::vector<State> LevelStates;
484 enum class Assignment : int8_t {
495 std::vector<Assignment> VarAssignments;
499 std::vector<Variable> ActiveVars;
504 : CNF(
buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
505 LevelStates(CNF.LargestVar + 1) {
506 assert(!Vals.empty());
511 LevelStates[0] = State::Decision;
514 VarAssignments.resize(CNF.
LargestVar + 1, Assignment::Unassigned);
519 ActiveVars.push_back(Var);
525 std::pair<Solver::Result, std::int64_t>
solve(std::int64_t MaxIterations) && {
532 while (I < ActiveVars.size()) {
533 if (MaxIterations == 0)
544 assert(activeVarsAreUnassigned());
545 assert(activeVarsFormWatchedLiterals());
546 assert(unassignedVarsFormingWatchedLiteralsAreActive());
548 const Variable ActiveVar = ActiveVars[I];
551 const bool unitPosLit = watchedByUnitClause(
posLit(ActiveVar));
552 const bool unitNegLit = watchedByUnitClause(
negLit(ActiveVar));
553 if (unitPosLit && unitNegLit) {
558 reverseForcedMoves();
567 LevelStates[Level] = State::Forced;
568 const Variable Var = LevelVars[Level];
569 VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
570 ? Assignment::AssignedFalse
571 : Assignment::AssignedTrue;
573 updateWatchedLiterals();
574 }
else if (unitPosLit || unitNegLit) {
579 LevelVars[Level] = ActiveVar;
580 LevelStates[Level] = State::Forced;
581 VarAssignments[ActiveVar] =
582 unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse;
586 if (I + 1 < ActiveVars.size()) {
589 ActiveVars[I] = ActiveVars.back();
595 ActiveVars.pop_back();
597 updateWatchedLiterals();
598 }
else if (I + 1 == ActiveVars.size()) {
603 LevelVars[Level] = ActiveVar;
604 LevelStates[Level] = State::Decision;
605 VarAssignments[ActiveVar] = decideAssignment(ActiveVar);
609 ActiveVars.pop_back();
611 updateWatchedLiterals();
626 llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
627 llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
633 VarAssignments[
Atomic.first] == Assignment::AssignedFalse
642 void reverseForcedMoves() {
643 for (; LevelStates[Level] == State::Forced; --Level) {
644 const Variable Var = LevelVars[Level];
646 VarAssignments[Var] = Assignment::Unassigned;
651 ActiveVars.push_back(Var);
656 void updateWatchedLiterals() {
661 const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
670 const size_t FalseLitWatcherStart = CNF.
ClauseStarts[FalseLitWatcher];
671 size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
672 while (isCurrentlyFalse(CNF.
Clauses[NewWatchedLitIdx]))
675 const Variable NewWatchedLitVar =
var(NewWatchedLit);
680 CNF.
Clauses[NewWatchedLitIdx] = FalseLit;
681 CNF.
Clauses[FalseLitWatcherStart] = NewWatchedLit;
685 if (!isWatched(NewWatchedLit) && !isWatched(
notLit(NewWatchedLit)) &&
686 VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
687 ActiveVars.push_back(NewWatchedLitVar);
693 FalseLitWatcher = NextFalseLitWatcher;
699 bool watchedByUnitClause(
Literal Lit)
const {
709 assert(Clause.front() == Lit);
719 return llvm::all_of(Clause.drop_front(),
720 [
this](
Literal L) { return isCurrentlyFalse(L); });
725 bool isCurrentlyFalse(
Literal Lit)
const {
726 return static_cast<int8_t
>(VarAssignments[
var(Lit)]) ==
727 static_cast<int8_t
>(Lit & 1);
731 bool isWatched(
Literal Lit)
const {
736 Assignment decideAssignment(
Variable Var)
const {
737 return !isWatched(
posLit(Var)) || isWatched(
negLit(Var))
738 ? Assignment::AssignedFalse
739 : Assignment::AssignedTrue;
748 WatchedLiterals.insert(Lit);
750 return WatchedLiterals;
754 bool activeVarsAreUnassigned()
const {
755 return llvm::all_of(ActiveVars, [
this](
Variable Var) {
756 return VarAssignments[Var] == Assignment::Unassigned;
761 bool activeVarsFormWatchedLiterals()
const {
763 return llvm::all_of(ActiveVars, [&WatchedLiterals](
Variable Var) {
764 return WatchedLiterals.contains(
posLit(Var)) ||
765 WatchedLiterals.contains(
negLit(Var));
771 bool unassignedVarsFormingWatchedLiteralsAreActive()
const {
774 for (
Literal Lit : watchedLiterals()) {
776 if (VarAssignments[Var] != Assignment::Unassigned)
778 if (ActiveVarsSet.contains(Var))
791 MaxIterations = Iterations;
std::pair< Solver::Result, std::int64_t > solve(std::int64_t MaxIterations) &&
WatchedLiteralsSolverImpl(const llvm::ArrayRef< const Formula * > &Vals)
Result solve(llvm::ArrayRef< const Formula * > Vals) override
Checks if the conjunction of Vals is satisfiable and returns the corresponding result.
uint32_t ClauseID
Clause identifiers are represented as positive integers.
static constexpr Variable NullVar
A null boolean variable is used as a placeholder in various data structures and algorithms.
static constexpr Literal negLit(Variable V)
Returns the negative literal !V.
static constexpr bool isNegLit(Literal L)
static constexpr Literal notLit(Literal L)
Returns the negated literal !L.
static constexpr Literal NullLit
A null literal is used as a placeholder in various data structures and algorithms.
static constexpr Literal posLit(Variable V)
Returns the positive literal V.
static constexpr ClauseID NullClause
A null clause identifier is used as a placeholder in various data structures and algorithms.
uint32_t Literal
Literals are represented as positive integers.
CNFFormula buildCNF(const llvm::ArrayRef< const Formula * > &Vals)
Converts the conjunction of Vals into a formula in conjunctive normal form where each clause has at l...
static constexpr Variable var(Literal L)
Returns the variable of L.
uint32_t Variable
Boolean variables are represented as positive integers.
static constexpr bool isPosLit(Literal L)
static Result TimedOut()
Constructs a result indicating that satisfiability checking on the queried boolean formula was not co...
static Result Unsatisfiable()
Constructs a result indicating that the queried boolean formula is unsatisfiable.
@ Satisfiable
Indicates that there exists a satisfying assignment for a boolean formula.