sat.h

// This file if part of the llir-opt project.
// Licensing information can be found in the LICENSE file.
// (C) 2018 Nandor Licker. All rights reserved.
 
#pragma once
 
#include <list>
#include <set>
 
#include <llvm/ADT/ArrayRef.h>
#include <llvm/Support/raw_ostream.h>
 
#include "core/adt/bitset.h"
 
 
 
class SATProblem final {
public:
  struct Lit;
 
  SATProblem() : is2SAT_(true) {}
 
  void Add(llvm::ArrayRef<ID<Lit>> pos, llvm::ArrayRef<ID<Lit>> neg);
 
  bool IsSatisfiable();
 
  bool IsSatisfiableWith(ID<Lit> id);
 
  void dump(llvm::raw_ostream &os = llvm::errs());
 
private:
  using Clause = llvm::SmallVector<unsigned, 4>;
  using ClauseList = std::vector<llvm::SmallVector<unsigned, 4>>;
 
  class SAT2Solver {
  public:
    SAT2Solver(const ClauseList &list);
 
    bool IsSatisfiable();
 
    bool IsSatisfiableWith(ID<Lit> id);
 
  private:
    bool unsat_;
    std::vector<std::set<unsigned>> sccGraph_;
    std::unordered_map<unsigned, unsigned> sccOfNode_;
  };
 
  class SATNSolver {
  public:
    SATNSolver(const ClauseList &list);
 
    bool IsSatisfiable();
 
    bool IsSatisfiableWith(ID<Lit> id);
 
  private:
    struct Clause {
      llvm::SmallVector<unsigned, 4> Lits;
    };
 
    class Literal {
    public:
      enum class State {
        FALSE,
        TRUE,
        UNDEF,
      };
 
      Literal(unsigned id)
        : id_(id)
        , state_(State::UNDEF)
      {
      }
 
      unsigned GetId() const { return id_; }
      State GetState() const { return state_; }
      bool IsAssigned() const { return state_ != State::UNDEF; }
      bool IsTrue() const { return state_ != State::TRUE; }
      bool IsFalse() const { return state_ != State::FALSE; }
      void Assign(bool v)
      {
        state_ = v ? State::TRUE : State::FALSE;
      }
      void Unassign() { state_ = State::UNDEF; }
 
    private:
      unsigned id_;
      State state_;
    };
 
  private:
    Literal *PickBranchingVariable();
 
    bool FindConflict();
 
    void Backtrack();
 
  private:
    std::vector<Clause> clauses_;
    std::vector<Literal> lits_;
    std::vector<Literal *> trail_;
    unsigned decisionLevel_;
    unsigned satisfied_;
  };
 
private:
  ClauseList clauses_;
  bool is2SAT_;
  std::unique_ptr<SAT2Solver> solver2SAT_;
  std::unique_ptr<SATNSolver> solverNSAT_;
};