[clang][dataflow] #llvm #flow-analysis Simplify formula at CNF construction time, and short-cut solving of known contradictory formulas.

[burakemir]

Summary

In dataflow analysis, SAT solver: simplify formula during CNF construction and short-cut
solving when the formula has been recognized as contradictory.

[sammccall]

This simplification makes sense, but if we're adding the layer, we're missing an opportunity to apply it completely.
(Intuitively, I don't see any reason that two passes is "enough")
To do this, we'd want to simplify existing formulas when we learn something new.

Curious whether you think this is worth doing and why - I don't think I'm opposed to the current version if it solves the practical problem, but I am concerned we might be adding simplification layers that solve some test cases but are defeated by relatively simple changes like reordering inputs.

---

For a complete version, I think the algorithm we'd want is something like:

clauses_so_far = {}
clauses_to_add = [...]

for clause in clauses_to_add:
  clause = simplify(clause)
  if clause is trivially true or clause in clauses_so_far:
    continue # adds nothing
  if clause is {lit}:
    # reprocess clauses containing the variable we just resolved
    affected_clauses = [c in clauses_so_far if lit in c or negate(lit) in c]
    clauses_so_far -= affected_clauses
    clauses_to_add += affected_clauses
  clauses_so_far.add(clause)
  if clause is trivially false:
    break

def simplify(clause):
  if clause.any(lit => {lit} in clauses_so_far):
    return trivially true 
  return clause.filter(lit => not {negate(lit)} in clauses_so_far)

So the builder data structure (clauses_so_far) needs to support:

• test for clause presence
• remove and return clauses containing a literal

I can't come up with anything particularly clever, but throwing some hashtables at it always works...

(A more powerful version would recognize that AvB can simplify AvBvC and so do removal by subset rather than a single literal, but that seems even further beyond scope)

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

179

It would be useful to briefly describe what kind of simplifications. (this drives e.g. the fact we use it twice).

AIUI:

It tracks variables that must be true/false, based on trivial clauses seen so far.
Such variables can be dropped from subsequently-added clauses, which
may render such clauses trivial and give us more known variables.

195

you're already testing this in the higher-level loop, so checking on every call to addClause doesn't seem to actually save anything significant.

IMO it makes responsibilities less clear, so I'd prefer to drop it here and addClauseLiterals

203

nit: capitalize variable names here & elsewhere

429

the issue is that info only propagates forward (earlier to later clauses, right?)

so by running this again, and sorting units first, we allow simplifications that propagate info backwards *once*, but we still don't have all simplifications.

D
Av!B
Bv!C
Cv!D

// first simplification pass

Av!B
Bv!C
C // hoist new unit

// second simplification pass

Av!B
B // hoist new unit

// third simplification pass
A

I think this is worth being explicit about: we're going to find some more simplifications, but we won't find them all, because running this to fixed point is too inefficient.

Is 2 experimentally determined to be the right number of passes? a guess? or am I misunderstanding :-)

[burakemir]

Addressing reviewer comments.

[burakemir]

Thanks for the review. PTAL.

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

429

You are right that one could do more work but it is better to leave this to the solver algorithm.

We know empirically that there will be a few unit clauses, so might as well spend *linear time* (in number of unit clauses) to save some work.

This won't be enough to determine whether all formulas are satisfiable, but it catches a few obvious contradictions.

Doing this twice (as opposed to once) catches more formulas that are obvious contradictions in our unit tests and some real sources. I picked two simply because when we obtain unit clauses "later", we had no opportunity to apply them to earlier clauses.

Doing full-blow mutations seems more complicated, esp. given that the Clauses data structure has been written for the actual solver algorithm. I think your concern on optimizing for a certain pattern of input formulas, which may well change in the future, is valid; therefore one should leave the "real" solving work to the solver algorithm, which systematically explores all cases.

[sammccall]

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

153

lits => Lits

184

I'm confused about this comment: the preprocessing looks like O(N): we process every clause once, and addClauseLiterals() runs in constant time. What am I missing?

202

if you're going to form an ArrayRef in any case, might as well skip this indirection and have the callsites pass addClause({L1, L2}) or so?

221

literal => L or so

259

IsKnownContradictory => isKnownContradictory

[burakemir]

Applied reviewer comments.

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

184

I am sorry for the misleading text: I only talked about addClause complexity.

And I estimated the lookup at a conservative O(log(K)) worst case complexity. And this is just completely wrong, since we can expect lookup to be on a hash-table. It would be O(1) average and worst case O(K).
I guess my mind was wandering off thinking about improving worst case lookup complexity.

Changed to O(N).

202

Thanks, this looks much nicer.

I chose to preserve the assert condition to check that there are <= 3 literals.

I believe the solver way work with clauses that have more literals but I don't know whether any trade-offs were made to focus on 3SAT in the solver.

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

 //===- WatchedLiteralsSolver.cpp --------------------------------*- C++ -*-===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines a SAT solver implementation that can be used by dataflow
 //  analyses.
 //
 //===----------------------------------------------------------------------===//
 
 #include <cassert>
+#include <cstddef>
 #include <cstdint>
-#include <iterator>
 #include <queue>
 #include <vector>
 
 #include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"

 
 /// A null literal is used as a placeholder in various data structures and
 /// algorithms.
 static constexpr Literal NullLit = 0;
 
 /// Returns the positive literal `V`.
 static constexpr Literal posLit(Variable V) { return 2 * V; }
 
+static constexpr bool isPosLit(Literal L) { return 0 == (L & 1); }
+
+static constexpr bool isNegLit(Literal L) { return 1 == (L & 1); }
+
 /// Returns the negative literal `!V`.
 static constexpr Literal negLit(Variable V) { return 2 * V + 1; }
 
 /// Returns the negated literal `!L`.
 static constexpr Literal notLit(Literal L) { return L ^ 1; }
 
 /// Returns the variable of `L`.
 static constexpr Variable var(Literal L) { return L >> 1; }
struct CNFFormula {
   /// follows the null clause. It is set to 0 and isn't used. Identifiers of
   /// clauses in the formula start from the element at index 1.
   std::vector<ClauseID> NextWatched;
 
   /// Stores the variable identifier and Atom for atomic booleans in the
   /// formula.
   llvm::DenseMap<Variable, Atom> Atomics;
 
+  /// Indicates that we already know the formula is unsatisfiable.
+  /// During construction, we catch simple cases of conflicting unit-clauses.
+  bool KnownContradictory;
+
   explicit CNFFormula(Variable LargestVar,
                       llvm::DenseMap<Variable, Atom> Atomics)
-      : LargestVar(LargestVar), Atomics(std::move(Atomics)) {
+      : LargestVar(LargestVar), Atomics(std::move(Atomics)),
+        KnownContradictory(false) {
     Clauses.push_back(0);
     ClauseStarts.push_back(0);
     NextWatched.push_back(0);
     const size_t NumLiterals = 2 * LargestVar + 1;
     WatchedHead.resize(NumLiterals + 1, 0);
   }
 
-  /// Adds the `L1 v L2 v L3` clause to the formula. If `L2` or `L3` are
-  /// `NullLit` they are respectively omitted from the clause.
-  ///
+  /// Adds the `L1 v ... v Ln` clause to the formula.
   /// Requirements:
   ///
-  ///  `L1` must not be `NullLit`.
+  ///  `Li` must not be `NullLit`.
   ///
   ///  All literals in the input that are not `NullLit` must be distinct.
-  void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) {
-    // The literals are guaranteed to be distinct from properties of Formula
-    // and the construction in `buildCNF`.
-    assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
-           (L2 != L3 || L2 == NullLit));
+  void addClause(ArrayRef<Literal> lits) {
+    assert(!lits.empty());
+    assert(llvm::all_of(lits, [](Literal L) { return L != NullLit; }));
 
     const ClauseID C = ClauseStarts.size();
     const size_t S = Clauses.size();
     ClauseStarts.push_back(S);
-
-    Clauses.push_back(L1);
-    if (L2 != NullLit)
-      Clauses.push_back(L2);
-    if (L3 != NullLit)
-      Clauses.push_back(L3);
+    Clauses.insert(Clauses.end(), lits.begin(), lits.end());
 
     // Designate the first literal as the "watched" literal of the clause.
-    NextWatched.push_back(WatchedHead[L1]);
-    WatchedHead[L1] = C;
+    NextWatched.push_back(WatchedHead[lits.front()]);
+    WatchedHead[lits.front()] = C;
   }
 
   /// Returns the number of literals in clause `C`.
   size_t clauseSize(ClauseID C) const {
     return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]
                                         : ClauseStarts[C + 1] - ClauseStarts[C];
   }
 
   /// Returns the literals of clause `C`.
   llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const {
     return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C));
   }
 };
 
+/// Applies simplifications while building up a BooleanFormula.
+/// We keep track of unit clauses, which tell us variables that must be
+/// true/false in any model that satisfies the overall formula.
+/// Such variables can be dropped from subsequently-added clauses, which
+/// may in turn yield more unit clauses or even a contradiction.
+/// The complexity of this preprocessing is O(log(K)) where K is the number
+/// of unit clauses. Assuming K << N, it is negligible. This method
+/// won't catch all contradictory formulas and need to leave general
+/// SAT solving to the solver algorithm.
+struct CNFFormulaBuilder {
+  // Formula should outlive CNFFormulaBuilder.
+  explicit CNFFormulaBuilder(CNFFormula &CNF)
+      : Formula(CNF) {}
+
+  /// Adds the `L1 v L2 v L3` clause to the formula. If `L2` or `L3` are
+  /// `NullLit` they are respectively omitted from the clause. Applies
+  /// simplifications, based on single-literal clauses.
+  ///
+  /// Requirements:
+  ///
+  ///  `L1` must not be `NullLit`.
+  ///
+  ///  All literals in the input that are not `NullLit` must be distinct.
+  void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) {
+    // The literals are guaranteed to be distinct from properties of BoolValue
+    // and the construction in `buildBooleanFormula`.
+    assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
+           (L2 != L3 || L2 == NullLit));
+
+    llvm::SmallVector<Literal, 3> Literals;
+    Literals.push_back(L1);
+    if (L2 != NullLit)
+      Literals.push_back(L2);
+    if (L3 != NullLit)
+      Literals.push_back(L3);
+
+    addClauseLiterals(Literals);
+  }
+
+  void addClauseLiterals(ArrayRef<Literal> Literals) {
+    // Contains literals of the simplified clause.
+    llvm::SmallVector<Literal> Simplified;
+    for (auto literal : Literals) {
+      auto v = var(literal);
+      if (trueVars.contains(v)) { // X must be true
+        if (isPosLit(literal))
+          return; // Omit clause `(... v X v ...)`, it is `true`.
+        else
+          continue; // Omit `!X` from `(... v !X v ...)`.
+      }
+      if (falseVars.contains(v)) { // X must be false
+        if (isNegLit(literal))
+          return; // Omit clause `(... v !X v ...)`, it is `true`.
+        else
+          continue; // Omit `X` from `(... v X v ...)`.
+      }
+      Simplified.push_back(literal);
+    }
+    if (Simplified.empty()) {
+      // Simplification made the clause empty, which is equivalent to `false`.
+      // We already know that this formula is unsatisfiable.
+      Formula.KnownContradictory = true;
+      // We can add any of the input literals to get an unsatisfiable formula.
+      Formula.addClause(Literals[0]);
+      return;
+    }
+    if (Simplified.size() == 1) {
+      // We have new unit clause.
+      const Literal lit = Simplified.front();
+      const Variable v = var(lit);
+      if (isPosLit(lit))
+        trueVars.insert(v);
+      else
+        falseVars.insert(v);
+    }
+    Formula.addClause(Simplified);
+  }
+
+  /// Returns true if we observed a contradiction while adding clauses.
+  /// In this case then the formula is already known to be unsatisfiable.
+  bool IsKnownContradictory() { return Formula.KnownContradictory; }
+
+private:
+  CNFFormula &Formula;
+  llvm::DenseSet<Variable> trueVars;
+  llvm::DenseSet<Variable> falseVars;
+};
+
 /// Converts the conjunction of `Vals` into a formula in conjunctive normal
 /// form where each clause has at least one and at most three literals.
 CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
   // The general strategy of the algorithm implemented below is to map each
   // of the sub-values in `Vals` to a unique variable and use these variables in
   // the resulting CNF expression to avoid exponential blow up. The number of
   // literals in the resulting formula is guaranteed to be linear in the number
   // of sub-formulas in `Vals`.
CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
   auto GetVar = [&SubValsToVar](const Formula *Val) {
     auto ValIt = SubValsToVar.find(Val);
     assert(ValIt != SubValsToVar.end());
     return ValIt->second;
   };
 
   CNFFormula CNF(NextVar - 1, std::move(Atomics));
   std::vector<bool> ProcessedSubVals(NextVar, false);
+  CNFFormulaBuilder builder(CNF);
 
-  // Add a conjunct for each variable that represents a top-level formula in
-  // `Vals`.
+  // Add a conjunct for each variable that represents a top-level conjunction
+  // value in `Vals`.
   for (const Formula *Val : Vals)
-    CNF.addClause(posLit(GetVar(Val)));
+    builder.addClause(posLit(GetVar(Val)));
 
   // Add conjuncts that represent the mapping between newly-created variables
   // and their corresponding sub-formulas.
   std::queue<const Formula *> UnprocessedSubVals;
   for (const Formula *Val : Vals)
     UnprocessedSubVals.push(Val);
   while (!UnprocessedSubVals.empty()) {
     const Formula *Val = UnprocessedSubVals.front();
while (!UnprocessedSubVals.empty()) {
     case Formula::And: {
       const Variable LHS = GetVar(Val->operands()[0]);
       const Variable RHS = GetVar(Val->operands()[1]);
 
       if (LHS == RHS) {
         // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
         // already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
+        builder.addClause(negLit(Var), posLit(LHS));
+        builder.addClause(posLit(Var), negLit(LHS));
       } else {
-        // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
-        // which is already in conjunctive normal form. Below we add each of the
-        // conjuncts of the latter expression to the result.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(negLit(Var), posLit(RHS));
-        CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+        // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v
+        // !B)` which is already in conjunctive normal form. Below we add each
+        // of the conjuncts of the latter expression to the result.
+        builder.addClause(negLit(Var), posLit(LHS));
+        builder.addClause(negLit(Var), posLit(RHS));
+        builder.addClause(posLit(Var), negLit(LHS), negLit(RHS));
       }
       break;
     }
     case Formula::Or: {
       const Variable LHS = GetVar(Val->operands()[0]);
       const Variable RHS = GetVar(Val->operands()[1]);
 
       if (LHS == RHS) {
         // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
         // already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
+        builder.addClause(negLit(Var), posLit(LHS));
+        builder.addClause(posLit(Var), negLit(LHS));
       } else {
         // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v
         // !B)` which is already in conjunctive normal form. Below we add each
         // of the conjuncts of the latter expression to the result.
-        CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
-        CNF.addClause(posLit(Var), negLit(RHS));
+        builder.addClause(negLit(Var), posLit(LHS), posLit(RHS));
+        builder.addClause(posLit(Var), negLit(LHS));
+        builder.addClause(posLit(Var), negLit(RHS));
       }
       break;
     }
     case Formula::Not: {
       const Variable Operand = GetVar(Val->operands()[0]);
 
       // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is
       // already in conjunctive normal form. Below we add each of the
       // conjuncts of the latter expression to the result.
-      CNF.addClause(negLit(Var), negLit(Operand));
-      CNF.addClause(posLit(Var), posLit(Operand));
+      builder.addClause(negLit(Var), negLit(Operand));
+      builder.addClause(posLit(Var), posLit(Operand));
       break;
     }
     case Formula::Implies: {
       const Variable LHS = GetVar(Val->operands()[0]);
       const Variable RHS = GetVar(Val->operands()[1]);
 
       // `X <=> (A => B)` is equivalent to
       // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
       // conjunctive normal form. Below we add each of the conjuncts of
       // the latter expression to the result.
-      CNF.addClause(posLit(Var), posLit(LHS));
-      CNF.addClause(posLit(Var), negLit(RHS));
-      CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+      builder.addClause(posLit(Var), posLit(LHS));
+      builder.addClause(posLit(Var), negLit(RHS));
+      builder.addClause(negLit(Var), negLit(LHS), posLit(RHS));
       break;
     }
     case Formula::Equal: {
       const Variable LHS = GetVar(Val->operands()[0]);
       const Variable RHS = GetVar(Val->operands()[1]);
 
       if (LHS == RHS) {
         // `X <=> (A <=> A)` is equvalent to `X` which is already in
         // conjunctive normal form. Below we add each of the conjuncts of the
         // latter expression to the result.
-        CNF.addClause(posLit(Var));
+        builder.addClause(posLit(Var));
 
         // No need to visit the sub-values of `Val`.
         continue;
       }
       // `X <=> (A <=> B)` is equivalent to
       // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which
       // is already in conjunctive normal form. Below we add each of the
       // conjuncts of the latter expression to the result.
-      CNF.addClause(posLit(Var), posLit(LHS), posLit(RHS));
-      CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
-      CNF.addClause(negLit(Var), posLit(LHS), negLit(RHS));
-      CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+      builder.addClause(posLit(Var), posLit(LHS), posLit(RHS));
+      builder.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+      builder.addClause(negLit(Var), posLit(LHS), negLit(RHS));
+      builder.addClause(negLit(Var), negLit(LHS), posLit(RHS));
       break;
     }
     }
+    if (builder.IsKnownContradictory()) {
+      return CNF;
+    }
     for (const Formula *Child : Val->operands())
       UnprocessedSubVals.push(Child);
   }
 
-  return CNF;
+  // Unit clauses that were added later were not
+  // considered for the simplification of earlier clauses. Do a final
+  // pass to find more opportunities for simplification.
+  CNFFormula FinalCNF(NextVar - 1, std::move(CNF.Atomics));
+  CNFFormulaBuilder FinalBuilder(FinalCNF);
+
+  // Collect unit clauses.
+  for (ClauseID C = 1; C < CNF.ClauseStarts.size(); ++C) {
+    if (CNF.clauseSize(C) == 1) {
+      FinalBuilder.addClause(CNF.clauseLiterals(C)[0]);
+    }
+  }
+
+  // Add all clauses that were added previously, preserving the order.
+  for (ClauseID C = 1; C < CNF.ClauseStarts.size(); ++C) {
+    FinalBuilder.addClauseLiterals(CNF.clauseLiterals(C));
+    if (FinalBuilder.IsKnownContradictory()) {
+      break;
+    }
+  }
+
+  return FinalCNF;
 }
 
 class WatchedLiteralsSolverImpl {
   /// A boolean formula in conjunctive normal form that the solver will attempt
   /// to prove satisfiable. The formula will be modified in the process.
   CNFFormula CNF;
 
   /// The search for a satisfying assignment of the variables in `Formula` will
for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
         ActiveVars.push_back(Var);
     }
   }
 
   // Returns the `Result` and the number of iterations "remaining" from
   // `MaxIterations` (that is, `MaxIterations` - iterations in this call).
   std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && {
+    if (CNF.KnownContradictory) {
+      // Short-cut the solving process. We already found out at CNF
+      // construction time that the formula is unsatisfiable.
+      return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations);
+    }
     size_t I = 0;
     while (I < ActiveVars.size()) {
       if (MaxIterations == 0)
         return std::make_pair(Solver::Result::TimedOut(), 0);
       --MaxIterations;
 
       // Assert that the following invariants hold:
       // 1. All active variables are unassigned.
while (I < ActiveVars.size()) {
 
         // This was the last active variable. Repeat the process from the
         // beginning.
         I = 0;
       } else {
         ++I;
       }
     }
-    return std::make_pair(Solver::Result::Satisfiable(buildSolution()), MaxIterations);
+    return std::make_pair(Solver::Result::Satisfiable(buildSolution()),
+                          MaxIterations);
   }
 
 private:
   /// Returns a satisfying truth assignment to the atoms in the boolean formula.
   llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
     llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
     for (auto &Atomic : CNF.Atomics) {
       // A variable may have a definite true/false assignment, or it may be
bool unassignedVarsFormingWatchedLiteralsAreActive() const {
     return true;
   }
 };
 
 Solver::Result
 WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
   if (Vals.empty())
     return Solver::Result::Satisfiable({{}});
-  auto [Res, Iterations] =
-      WatchedLiteralsSolverImpl(Vals).solve(MaxIterations);
+  auto [Res, Iterations] = WatchedLiteralsSolverImpl(Vals).solve(MaxIterations);
   MaxIterations = Iterations;
   return Res;
 }
 
 } // namespace dataflow
 } // namespace clang

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

TEST(SolverTest, ReachedLimitsReflectsTimeouts) {
   // !(Z ^ W) <=> !Z v !W
   auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
 
   // A ^ B
   ASSERT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut);
   EXPECT_TRUE(solver.reachedLimit());
 }
 
+TEST(SolverTest, SimpleButLargeContradiction) {
+  // This test ensures that the solver takes a short-cut on known
+  // contradictory inputs, without using max_iterations. At the time
+  // this test is added, formulas that are easily recognized to be
+  // contradictory at CNF construction time would lead to timeout.
+  WatchedLiteralsSolver solver(10);
+  ConstraintContext Ctx;
+  auto first = Ctx.atom();
+  auto last = first;
+  for (int i = 1; i < 10000; ++i) {
+    last = Ctx.conj(last, Ctx.atom());
+  }
+  last = Ctx.conj(Ctx.neg(first), last);
+  ASSERT_EQ(solver.solve({last}).getStatus(),
+            Solver::Result::Status::Unsatisfiable);
+  EXPECT_FALSE(solver.reachedLimit());
+
+  first = Ctx.atom();
+  last = Ctx.neg(first);
+  for (int i = 1; i < 10000; ++i) {
+    last = Ctx.conj(last, Ctx.neg(Ctx.atom()));
+  }
+  last = Ctx.conj(first, last);
+  ASSERT_EQ(solver.solve({last}).getStatus(),
+            Solver::Result::Status::Unsatisfiable);
+  EXPECT_FALSE(solver.reachedLimit());
+}
+
 } // namespace