23#include "llvm/ADT/DenseMap.h"
24#include "llvm/ADT/DenseSet.h"
25#include "llvm/ADT/STLExtras.h"
125 llvm::DenseMap<Variable, AtomicBoolValue *>
Atomics;
128 llvm::DenseMap<Variable, AtomicBoolValue *>
Atomics)
133 const size_t NumLiterals = 2 *
LargestVar + 1;
148 assert(L1 !=
NullLit && L1 != L2 && L1 != L3 &&
152 const size_t S =
Clauses.size();
188 llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
190 llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
193 std::queue<BoolValue *> UnprocessedSubVals;
195 UnprocessedSubVals.push(Val);
196 while (!UnprocessedSubVals.empty()) {
198 BoolValue *Val = UnprocessedSubVals.front();
199 UnprocessedSubVals.pop();
201 if (!SubValsToVar.try_emplace(Val, Var).second)
208 auto *
C = cast<ConjunctionValue>(Val);
209 UnprocessedSubVals.push(&
C->getLeftSubValue());
210 UnprocessedSubVals.push(&
C->getRightSubValue());
214 auto *D = cast<DisjunctionValue>(Val);
215 UnprocessedSubVals.push(&D->getLeftSubValue());
216 UnprocessedSubVals.push(&D->getRightSubValue());
220 auto *N = cast<NegationValue>(Val);
221 UnprocessedSubVals.push(&N->getSubVal());
225 auto *I = cast<ImplicationValue>(Val);
226 UnprocessedSubVals.push(&I->getLeftSubValue());
227 UnprocessedSubVals.push(&I->getRightSubValue());
231 auto *B = cast<BiconditionalValue>(Val);
232 UnprocessedSubVals.push(&B->getLeftSubValue());
233 UnprocessedSubVals.push(&B->getRightSubValue());
242 Atomics[Var] = cast<AtomicBoolValue>(Val);
246 llvm_unreachable(
"buildBooleanFormula: unhandled value kind");
251 auto GetVar = [&SubValsToVar](
const BoolValue *Val) {
252 auto ValIt = SubValsToVar.find(Val);
253 assert(ValIt != SubValsToVar.end());
254 return ValIt->second;
258 std::vector<bool> ProcessedSubVals(NextVar,
false);
267 std::queue<BoolValue *> UnprocessedSubVals;
269 UnprocessedSubVals.push(Val);
270 while (!UnprocessedSubVals.empty()) {
271 const BoolValue *Val = UnprocessedSubVals.front();
272 UnprocessedSubVals.pop();
275 if (ProcessedSubVals[Var])
277 ProcessedSubVals[Var] =
true;
279 if (
auto *
C = dyn_cast<ConjunctionValue>(Val)) {
280 const Variable LeftSubVar = GetVar(&
C->getLeftSubValue());
281 const Variable RightSubVar = GetVar(&
C->getRightSubValue());
283 if (LeftSubVar == RightSubVar) {
291 UnprocessedSubVals.push(&
C->getLeftSubValue());
301 UnprocessedSubVals.push(&
C->getLeftSubValue());
302 UnprocessedSubVals.push(&
C->getRightSubValue());
304 }
else if (
auto *D = dyn_cast<DisjunctionValue>(Val)) {
305 const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
306 const Variable RightSubVar = GetVar(&D->getRightSubValue());
308 if (LeftSubVar == RightSubVar) {
316 UnprocessedSubVals.push(&D->getLeftSubValue());
326 UnprocessedSubVals.push(&D->getLeftSubValue());
327 UnprocessedSubVals.push(&D->getRightSubValue());
329 }
else if (
auto *N = dyn_cast<NegationValue>(Val)) {
330 const Variable SubVar = GetVar(&N->getSubVal());
339 UnprocessedSubVals.push(&N->getSubVal());
340 }
else if (
auto *I = dyn_cast<ImplicationValue>(Val)) {
341 const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
342 const Variable RightSubVar = GetVar(&I->getRightSubValue());
353 UnprocessedSubVals.push(&I->getLeftSubValue());
354 UnprocessedSubVals.push(&I->getRightSubValue());
355 }
else if (
auto *B = dyn_cast<BiconditionalValue>(Val)) {
356 const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
357 const Variable RightSubVar = GetVar(&B->getRightSubValue());
359 if (LeftSubVar == RightSubVar) {
377 UnprocessedSubVals.push(&B->getLeftSubValue());
378 UnprocessedSubVals.push(&B->getRightSubValue());
405 std::vector<Variable> LevelVars;
408 enum class State : uint8_t {
421 std::vector<State> LevelStates;
423 enum class Assignment : int8_t {
434 std::vector<Assignment> VarAssignments;
438 std::vector<Variable> ActiveVars;
443 LevelStates(Formula.LargestVar + 1) {
444 assert(!Vals.empty());
449 LevelStates[0] = State::Decision;
452 VarAssignments.resize(Formula.
LargestVar + 1, Assignment::Unassigned);
457 ActiveVars.push_back(Var);
463 while (I < ActiveVars.size()) {
471 assert(activeVarsAreUnassigned());
472 assert(activeVarsFormWatchedLiterals());
473 assert(unassignedVarsFormingWatchedLiteralsAreActive());
475 const Variable ActiveVar = ActiveVars[I];
478 const bool unitPosLit = watchedByUnitClause(
posLit(ActiveVar));
479 const bool unitNegLit = watchedByUnitClause(
negLit(ActiveVar));
480 if (unitPosLit && unitNegLit) {
485 reverseForcedMoves();
494 LevelStates[Level] = State::Forced;
495 const Variable Var = LevelVars[Level];
496 VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
497 ? Assignment::AssignedFalse
498 : Assignment::AssignedTrue;
500 updateWatchedLiterals();
501 }
else if (unitPosLit || unitNegLit) {
506 LevelVars[Level] = ActiveVar;
507 LevelStates[Level] = State::Forced;
508 VarAssignments[ActiveVar] =
509 unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse;
513 if (I + 1 < ActiveVars.size()) {
516 ActiveVars[I] = ActiveVars.back();
522 ActiveVars.pop_back();
524 updateWatchedLiterals();
525 }
else if (I + 1 == ActiveVars.size()) {
530 LevelVars[Level] = ActiveVar;
531 LevelStates[Level] = State::Decision;
532 VarAssignments[ActiveVar] = decideAssignment(ActiveVar);
536 ActiveVars.pop_back();
538 updateWatchedLiterals();
553 llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
555 llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution;
556 for (
auto &Atomic : Formula.
Atomics) {
560 Solution[Atomic.second] =
561 VarAssignments[Atomic.first] == Assignment::AssignedFalse
570 void reverseForcedMoves() {
571 for (; LevelStates[Level] == State::Forced; --Level) {
572 const Variable Var = LevelVars[Level];
574 VarAssignments[Var] = Assignment::Unassigned;
579 ActiveVars.push_back(Var);
584 void updateWatchedLiterals() {
589 const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
598 const size_t FalseLitWatcherStart = Formula.
ClauseStarts[FalseLitWatcher];
599 size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
600 while (isCurrentlyFalse(Formula.
Clauses[NewWatchedLitIdx]))
603 const Variable NewWatchedLitVar =
var(NewWatchedLit);
608 Formula.
Clauses[NewWatchedLitIdx] = FalseLit;
609 Formula.
Clauses[FalseLitWatcherStart] = NewWatchedLit;
613 if (!isWatched(NewWatchedLit) && !isWatched(
notLit(NewWatchedLit)) &&
614 VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
615 ActiveVars.push_back(NewWatchedLitVar);
618 Formula.
WatchedHead[NewWatchedLit] = FalseLitWatcher;
621 FalseLitWatcher = NextFalseLitWatcher;
627 bool watchedByUnitClause(
Literal Lit)
const {
638 assert(Clause.front() == Lit);
648 return llvm::all_of(Clause.drop_front(),
649 [
this](
Literal L) { return isCurrentlyFalse(L); });
654 bool isCurrentlyFalse(
Literal Lit)
const {
655 return static_cast<int8_t
>(VarAssignments[
var(Lit)]) ==
656 static_cast<int8_t
>(Lit & 1);
660 bool isWatched(
Literal Lit)
const {
665 Assignment decideAssignment(
Variable Var)
const {
666 return !isWatched(
posLit(Var)) || isWatched(
negLit(Var))
667 ? Assignment::AssignedFalse
668 : Assignment::AssignedTrue;
677 WatchedLiterals.insert(Lit);
679 return WatchedLiterals;
683 bool activeVarsAreUnassigned()
const {
684 return llvm::all_of(ActiveVars, [
this](
Variable Var) {
685 return VarAssignments[Var] == Assignment::Unassigned;
690 bool activeVarsFormWatchedLiterals()
const {
692 return llvm::all_of(ActiveVars, [&WatchedLiterals](
Variable Var) {
693 return WatchedLiterals.contains(
posLit(Var)) ||
694 WatchedLiterals.contains(
negLit(Var));
700 bool unassignedVarsFormingWatchedLiteralsAreActive()
const {
703 for (
Literal Lit : watchedLiterals()) {
705 if (VarAssignments[Var] != Assignment::Unassigned)
707 if (ActiveVarsSet.contains(Var))
Solver::Result solve() &&
WatchedLiteralsSolverImpl(const llvm::DenseSet< BoolValue * > &Vals)
Result solve(llvm::DenseSet< BoolValue * > 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.
BooleanFormula buildBooleanFormula(const llvm::DenseSet< BoolValue * > &Vals)
Converts the conjunction of Vals into a formula in conjunctive normal form where each clause has at l...
static constexpr Literal negLit(Variable V)
Returns the negative literal !V.
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.
static constexpr Variable var(Literal L)
Returns the variable of L.
uint32_t Variable
Boolean variables are represented as positive integers.
@ C
Languages that the frontend can parse and compile.
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.