kirimochi.rb

# frozen_string_literal: true

require 'set'

# # KiriMochi: A SAT Solver Written in Ruby
#
# KiriMochi is a SAT solver written in Ruby. It is based on [MiniSAT](http://minisat.se),
# [Glucose](https://www.labri.fr/perso/lsimon/research/glucose/), and [Gophersat](https://github.com/crillab/gophersat),
# but the implementation is simpler than theirs and easy to understand.
# It implements modern techniques in SAT solving, including
#
# - conflict-driven clause learning (CDCL),
# - two-watched literals,
# - variable selection heuristics based on VSIDS, and
# - learned clause reduction based on LBD.
#
# Due to the Ruby performance and poor optimization, KiriMochi is roughly 5-20x slower than the based implementations.
#
# ## Version History
#
# ### v0.2.0 (2025-09-05)
# 
# This release contains a new feature `Solver#each`.
#
# - Add the `Solver#each` method to enumerate all solutions.
# - Implement a random decision (however, it is disabled by the default setting).
# - Replace `Array#each` with `while` for optimization.
# - Replace `Array#delete_if` with `Array#index` and `Array#delete_at`.
#
# ### v0.1.1 (2025-09-02)
#
# This release contains a small optimization.
#
# - Replace `Integer#times` with `while` for optimization.
# 
# ### v0.1.0 (2025-08-29)
#
# It is the initial release. The following features are implemented:
#
# - conflict-driven clause learning (CDCL),
# - two-watched literals,
# - variable selection heuristics based on VSIDS,
# - learned clause reduction based on LBD.
#
# ## License
#
# This project is licensed under the MIT license.
#
# Copyright 2025 Hiroya Fujinami (a.k.a. TSUYUSATO "MakeNowJust" Kitsune) <[email protected]>
# 
# Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
# associated documentation files (the “Software”), to deal in the Software without restriction, including
# without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to
# the following conditions:
# 
# The above copyright notice and this permission notice shall be included in all copies or substantial portions
# of the Software.
# 
# THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED
# TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL
# THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF
# CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
# DEALINGS IN THE SOFTWARE.

module KiriMochi
  VERSION = '0.2.0'

  # Parses a given string as the DIMACS CNF format and returns an array of clauses.
  #
  # This implementation is very naive. It does not handle all edge cases and
  # assumes the input is well-formed.
  def self.load_cnf(text)
    num_clauses = nil
    clauses = []

    text.lines.each do |line|
      line = line.strip
      next if line.empty? || line.start_with?('c') || line.start_with?('%') || line.start_with?('0')

      if line.start_with?('p cnf')
        unless clauses.empty? && num_clauses.nil?
          raise ArgumentError, 'An invalid problem line is found'
        end

        parts = line.split
        num_clauses = parts[3].to_i
        next
      end

      clause = line.split.map(&:to_i)
      clause.pop if clause.last == 0
      clauses << clause
    end

    if num_clauses
      raise ArgumentError, 'The number of clauses does not match' if clauses.size != num_clauses
    end

    clauses
  end

  # `LearnedClause` is a clause with additional information of a learned clause used in CDCL.
  #
  # This class is mutable. We can change `activity` and its status (via `lock` and `unlock`),
  # but `clause` and `lbd` are immutable.
  class LearnedClause
    def initialize(clause, lbd)
      @clause = clause
      @lbd = lbd
      @activity = 0.0

      # `@status` can be either `:locked` or `:unlocked`.
      # `:locked` means the clause is used in the current model, and `:unlocked` means otherwise.
      @status = :locked
    end

    attr_reader :clause, :lbd
    attr_accessor :activity

    def locked? = @status == :locked

    def lock
      @status = :locked
    end

    def unlock
      @status = :unlocked
    end
  end

  # `Heap` is a binary heap data structure for priority queue.
  # It is used for a variable queue based on VSIDS.
  #
  # A comparison function is provided to determine the priority of each value.
  # Note that we need to notify changes of priorities to the heap manually.
  class Heap
    def initialize(&lt)
      @content = []
      @indices = []
      @lt = lt
    end

    def empty? = @content.empty?

    def include?(x) =
      x < @indices.size && @indices[x] >= 0

    def notify(x)
      percolate_up(@indices[x])
    end

    def enqueue(x)
      @indices.push(-1) while @indices.size < x
      @indices[x] = @content.size
      @content << x
      percolate_up(@indices[x])
    end

    def dequeue
      x = @content[0]
      @content[0] = @content.last
      @indices[@content[0]] = 0
      @indices[x] = -1
      @content.pop
      percolate_down(0) unless @content.empty?
      x
    end

    def sample(random: Random) =
      @content.sample(random:)

    private

    def left(i) = i * 2 + 1
    def right(i) = (i + 1) * 2
    def parent(i) = (i - 1) >> 1

    def percolate_up(i)
      x = @content[i]
      p = parent(i)
      while i != 0 && @lt.call(x, @content[p])
        @content[i] = @content[p]
        @indices[@content[p]] = i
        i = p
        p = parent(p)
      end
      @content[i] = x
      @indices[x] = i
    end

    def percolate_down(i)
      x = @content[i]
      while left(i) < @content.size
        child =
          if right(i) < @content.size && @lt.call(@content[right(i)], @content[left(i)])
            right(i)
          else
            left(i)
          end
        break unless @lt.call(@content[child], x)
        @content[i] = @content[child]
        @indices[@content[i]] = i
        i = child
      end
      @content[i] = x
      @indices[x] = i
    end
  end

  # `RingBuffer` is a fixed-size circular buffer for numeric values.
  # It also computes the total/moving average of the values.
  # It is used for storing the LBD and trail sizes in `LbdStats`.
  class RingBuffer
    def initialize(capacity)
      @capacity = capacity
      @buffer = Array.new(capacity) { 0 }

      # `@total_sum` and `@total_nb` hold the total sum and number, respectively,
      # of the values pushed to it until now.
      @total_sum = 0
      @total_nb = 0

      # `@index` is a pointer to the circular buffer, and `@is_full` indicates
      # whether `@index` reached the capacity until now.
      @index = 0
      @is_full = false

      # It is the moving average of the values in the buffer.
      @recent_avg = 0.0
    end

    attr_reader :recent_avg

    def clear
      @index = 0
      @is_full = false
      @recent_avg = 0.0
    end

    def total_avg =
      @total_sum.to_f / @total_nb.to_f

    def full? = @is_full

    def push(value)
      @total_nb += 1
      @total_sum += value

      if @index < @capacity && !full?
        @buffer[@index] = value
        @index += 1
        @recent_avg = (@recent_avg * (@index - 1) + value) / @index

        if @index == @capacity
          @index = 0
          @is_full = true
        end
      else
        old_value = @buffer[@index]
        @buffer[@index] = value
        @index += 1
        @index = 0 if @index == @capacity
        @recent_avg += (value - old_value) / @capacity.to_f
      end
    end
  end

  # `LbdStats` holds statistics about the LBD and trail sizes.
  # It is used to determine when to restart the solver.
  #
  # This idea is inspired by [Glucose](https://www.labri.fr/perso/lsimon/research/glucose/).
  class LbdStats
    # Default value constants:
    NbMaxLbd = 50
    NbMaxTrail = 5000
    TriggerRestartK = 0.8
    PostponeRestartT = 1.4

    def initialize(
      nb_max_lbd: NbMaxLbd,
      nb_max_trail: NbMaxTrail,
      trigger_restart_k: TriggerRestartK,
      postpone_restart_t: PostponeRestartT
    )
      @lbd_buffer = RingBuffer.new(nb_max_lbd)
      @trail_buffer = RingBuffer.new(nb_max_trail)
      @trigger_restart_k = trigger_restart_k
      @postpone_restart_t = postpone_restart_t
    end

    def must_restart?
      return false unless @lbd_buffer.full?

      @lbd_buffer.recent_avg * @trigger_restart_k > @lbd_buffer.total_avg
    end

    def push(trail_size, lbd)
      @trail_buffer.push(trail_size)
      if @trail_buffer.full? && @lbd_buffer.full?
        @lbd_buffer.clear if trail_size > (@trail_buffer.recent_avg * @postpone_restart_t).to_i
      end

      @lbd_buffer.push(lbd)
    end

    def clear
      @lbd_buffer.clear
    end
  end

  # `Solver` is a SAT solver implementation.
  class Solver
    # Default value constants:
    VarInc = 1.0
    VarDecay = 0.8
    ClauseInc = 1.0
    ClauseDecay = 0.999
    NbMaxLearnedClauses = 2000
    NbMaxLearnedClausesPostponeInc = 1000
    NbMaxLearnedClausesInc = 300
    RandomFreq = 0

    # Constants:
    VarLimit = 1e100
    ClauseLimit = 1e30

    # TODO: implement `verbose` mode.

    def initialize(problem, config = {})
      # Initialize statistics counters.
      @stat_nb_restarts = 0
      @stat_nb_conflicts = 0
      @stat_nb_decisions = 0
      @stat_nb_random_decisions = 0
      @stat_nb_propagations = 0
      @stat_nb_learned = 0
      @stat_nb_deleted = 0

      # A set of variables appeared in the problem.
      @vars = Set.new

      # A hash table mapping watched literals to clauses (watcher list).
      #
      # Watched literals must be placed at the first or second position in the clause.
      # In short, for any `lit` and each `clause` in `watchers[lit]`, `clause[0] == -lit` or `clause[1] == -lit` hold.
      #
      # Note that a watcher list does not contain trivial unit clauses.
      @watchers = {}

      # A queue of found unit clauses.
      @units = []

      # Initialize `@vars`, `@watcher`, and `@units` from the given problem.
      problem.each do |clause|
        raise ArgumentError, 'An empty clause is invalid' if clause.empty?

        clause = clause.dup
        # The first call removes duplicate literals, and the second call (in the suffix `if`)
        # removes combinations of a literal and its negation.
        # `Array#uniq!` returns `self` if duplicates are found and deleted, and returns `nil` otherwise,
        # so the `if` condition checks `clause` does not contain both a literal and its negation (i.e., contradiction).
        clause.uniq!
        raise ArgumentError, 'Duplicate literals are not allowed' if clause.uniq!(&:abs)

        clause.each do |lit|
          @vars << lit.abs
          @watchers[lit] ||= []
          @watchers[-lit] ||= []
        end

        if clause.size == 1
          @units << clause
        else
          @watchers[-clause[0]] << clause
          @watchers[-clause[1]] << clause
        end
      end

      # Initialize instance variables about the current model.
      @model = {}
      @reasons = {}
      @dec_levels = {}
      @trail = []

      # Initialize instance variables about variable selection.
      max_var = @vars.max
      @var_polarity = [1] * (max_var + 1)
      @var_activity = [0] * (max_var + 1)
      @var_queue = Heap.new { |i, j| @var_activity[i] > @var_activity[j] }
      @vars.each { |v| @var_queue.enqueue(v) }
      @var_inc = config[:var_inc] || VarInc
      @var_decay = config[:var_decay] || VarDecay

      # Initialize instance variables about learned clauses.
      @learned_clauses = []
      @nb_max_learned_clauses = config[:nb_max_learned_clauses] || NbMaxLearnedClauses
      @nb_max_learned_clauses_inc = config[:nb_max_learned_clauses_inc] || NbMaxLearnedClausesInc
      @nb_max_learned_clauses_postpone_inc = config[:nb_max_learned_clauses_postpone_inc] || NbMaxLearnedClausesPostponeInc
      @idx_reduce = 1
      @clause_to_learned_clause = {}
      @clause_inc = config[:clause_inc] || ClauseInc
      @clause_decay = config[:clause_decay] || ClauseDecay

      # Initialize instance variables about restarts.
      nb_max_lbd = config[:nb_max_lbd] || LbdStats::NbMaxLbd
      nb_max_trail = config[:nb_max_trail] || LbdStats::NbMaxTrail
      trigger_restart_k = config[:trigger_restart_k] || LbdStats::TriggerRestartK
      postpone_restart_t = config[:postpone_restart_t] || LbdStats::PostponeRestartT
      @lbd_stats = LbdStats.new(nb_max_lbd:, nb_max_trail:, trigger_restart_k:, postpone_restart_t:)

      # Initialize instance variables to avoid allocation.
      @preallocated_set = Set.new

      @random_seed = config[:random_seed] || Random.new_seed
      @random = Random.new(@random_seed)
      @random_freq = config[:random_freq] || RandomFreq
    end

    # Returns statistics as a hash.
    def stats
      {
        random_seed: @random_seed,
        nb_restarts: @stat_nb_restarts,
        nb_conflicts: @stat_nb_conflicts,
        nb_decisions: @stat_nb_decisions,
        nb_random_decisions: @stat_nb_random_decisions,
        nb_propagations: @stat_nb_propagations,
        nb_learned: @stat_nb_learned,
        nb_deleted: @stat_nb_deleted
      }
    end

    # Runs the solver and returns the model hash if found, or `nil` if unsatisfiable.
    def solve
      ok = search_and_propagate
      while ok.nil?
        ok = search_and_propagate
      end
      ok ? @model.dup : nil
    end

    # Enumerates all solutions. A found solution is yielded to the given block.
    # If a block is not given, an enumerator is returned.
    def each
      return to_enum unless block_given?

      model = solve

      until model.nil?
        yield model

        dec_vars = model.keys.filter { |var| @reasons[var].nil? }
        new_clause = dec_vars.map { |var| model[var] ? -var : var }

        @lbd_stats.clear
        backtrack(0)

        # It is the only solution.
        break if new_clause.empty?

        if new_clause.size == 1
          @units << new_clause
        else
          @watchers[-new_clause[0]] << new_clause
          @watchers[-new_clause[1]] << new_clause
        end

        model = solve
      end

      nil
    end

    private

    # Runs the main loop of the SAT solver.
    # When it returns `true`, the problem is satisfiable; when it returns `false`, it is unsatisfiable;
    # and, when it returns `nil`, satisfiability is unknown, so the solver should restart.
    def search_and_propagate
      @stat_nb_restarts += 1

      dec_level = 0

      if @units.empty?
        dec_level += 1
        lit = make_decision
        reason = nil
      else
        unit = @units.shift
        lit = unit[0]
        reason = unit
      end

      until lit.nil?
        if reason
          @reasons[lit.abs] = reason
          @clause_to_learned_clause[reason.object_id]&.lock
        end
        conflict = assign(lit, dec_level)

        # When a conflict is detected on propagation, ...
        if conflict
          @stat_nb_conflicts += 1

          # Increase variable decay rate after 5000 conflicts.
          # TODO: make it configurable.
          if @stat_nb_conflicts % 5000 == 0 && @var_decay < 0.95
            @var_decay += 0.01
          end

          backtrack_level, new_clause = analyze(conflict, dec_level)
          return false unless backtrack_level

          backtrack(backtrack_level)

          dec_level = backtrack_level
          lit = new_clause[0]
          reason = new_clause
          next
        end

        # When no conflict is detected on propagation, ...

        # If unit propagation is possible, we perform it.
        unless @units.empty?
          unit = @units.shift
          lit = unit[0]
          reason = unit
          next
        end

        if @lbd_stats.must_restart?
          @lbd_stats.clear
          backtrack(0)
          return nil
        end

        if @stat_nb_conflicts >= @idx_reduce * @nb_max_learned_clauses
          @idx_reduce = @stat_nb_conflicts / @nb_max_learned_clauses + 1
          reduce_learned
          bump_nb_max_learned_clauses
        end

        dec_level += 1
        lit = make_decision
        reason = nil
      end

      return true
    end

    # Returns the next decision literal.
    #
    # If it returns `nil`, it means there are no more variables to decide.
    # Therefore, the search is finished as satisfiable.
    def make_decision
      @stat_nb_decisions += 1

      if @random_freq > 0.0 && @random.rand < @random_freq
        @stat_nb_random_decisions += 1
        var = @var_queue.sample(random: @random)
        return var * @var_polarity[var] unless @model.key?(var)
      end

      until @var_queue.empty?
        var = @var_queue.dequeue
        return var * @var_polarity[var] unless @model.key?(var)
      end

      nil
    end

    # Does backtracking to the given decision level.
    # After this invocation, `@dec_levels[@trail.last.abs] == backtrack_level` if `@trail.last` is not `nil`.
    #
    # It also clears `@units`.
    def backtrack(backtrack_level)
      @units.clear

      while [email protected]? && @dec_levels[@trail.last.abs] > backtrack_level
        lit = @trail.pop

        @model.delete(lit.abs)

        clause = @reasons.delete(lit.abs)
        if learned = @clause_to_learned_clause[clause.object_id]
          learned.unlock
        end

        @dec_levels.delete(lit.abs)

        @var_polarity[lit.abs] = lit > 0 ? 1 : -1

        @var_queue.enqueue(lit.abs) unless @var_queue.include?(lit.abs)
      end
    end

    # Updates the current model by `lit`, and propagates the assignment.
    # If a conflict is detected, it returns the conflicting clause, or it returns `nil` otherwise.
    def assign(lit, dec_level)
      @stat_nb_propagations += 1

      var = lit.abs
      case lit_status(lit)
      when true
        # If the literal is satisfiable, we do nothing.
        return nil
      when false
        # If the literal is unsatisfiable, we report a conflict.
        # This case is only reachable if the given problem is trivially unsatisfiable;
        # in short, `clauses` given to the constructor contains `[lit]` and `[-lit]` for some `lit`.
        # In other case, the conflict is detected by the watcher-list updation below.
        return [] # Therefore, this return value is dummy.
      when nil
        # If the literal is unassigned, we assign it.
        @model[var] = (lit > 0)
        @dec_levels[var] = dec_level
        @trail << lit
      end

      # As propagation, we update the watcher list of `lit` in in-place manner.
      ws = @watchers[lit]
      next_ws_size = 0

      i = 0
      ws_size = ws.size
      while i < ws_size
        w = ws[i]

        # We enforce `w[1] == -lit` and `lit_status(w[1]) == false`.
        # Note that `w.size > 2` since we don't watch `clause.size == 1` and `clause` must be non-empty.
        w[0], w[1] = w[1], w[0] if w[0] == -lit

        status = lit_status(w[0])
        if status == true
          # If `w` is already satisfied, we keep it in the watcher list.
          ws[next_ws_size] = w
          next_ws_size += 1
          i += 1
          next
        end

        # We find an unassigned literal, and set it as a new watched literal.
        found = false
        # To avoid allocation of a range, we use the below instead of `(2...w.size).each do |k|`.
        k = 2
        w_size = w.size
        while k < w_size
          unless lit_status(w[k]) == false
            w[1], w[k] = w[k], w[1]
            @watchers[-w[1]] << w
            found = true
            break
          end
          k += 1
        end
        if found
          i += 1
          next
        end

        if status == false
          # If both `w[0]` and `w[1]` are unsatisfiable and such a literal is not found,
          # then `w` is unsatisfiable and we report a conflict.

          (i...ws.size).each do |j|
            ws[next_ws_size] = ws[j]
            next_ws_size += 1
          end
          (ws.size - next_ws_size).times { ws.pop }

          return w
        end

        # If such a literal is not found, then `w` is a unit clause.
        @units << w
        ws[next_ws_size] = w
        next_ws_size += 1
        i += 1

        nil
      end
      (ws.size - next_ws_size).times { ws.pop }

      nil
    end

    # Analyzes the given conflict clause and returns a pair of a backtrack level and a learned clause.
    # If the conflict occured at the top level, it returns `nil` and means the problem is unsatisfiable.
    def analyze(conflict, dec_level)
      return if dec_level == 0

      trail_index = @trail.size - 1
      clause = conflict
      level_lit = nil
      num_level_lit = 0
      seen = @preallocated_set.clear
      new_clause = [0]

      while level_lit.nil? || num_level_lit > 0
        clause_bump_activity(clause)

        ((level_lit.nil? ? 0 : 1)...clause.size).each do |i|
          lit = clause[i]
          next if seen.include?(lit.abs)
          seen.add(lit.abs)
          var_bump_activity(lit.abs)
          if @dec_levels[lit.abs] == dec_level
            num_level_lit += 1
          else
            new_clause << lit
          end
        end

        while !seen.include?(@trail[trail_index].abs)
          trail_index -= 1
        end

        level_lit = @trail[trail_index]
        clause = @reasons[level_lit.abs]
        trail_index -= 1
        num_level_lit -= 1
        seen.delete(level_lit.abs)
      end

      clause_decay_activity()
      var_decay_activity()

      new_clause[0] = -level_lit
      minimize_learned(new_clause, seen)

      backtrack_level = 0
      lbd = 1
      if new_clause.size > 1
        max_i = 1
        backtrack_level = @dec_levels[new_clause[1].abs]
        seen_levels = @preallocated_set.clear
        seen_levels << backtrack_level
        (2...new_clause.size).each do |i|
          dec_level = @dec_levels[new_clause[i].abs]
          if dec_level > backtrack_level
            backtrack_level = dec_level
            max_i = i
          end
          seen_levels.add(dec_level)
        end

        new_clause[1], new_clause[max_i] = new_clause[max_i], new_clause[1]
        @watchers[-new_clause[0]] << new_clause
        @watchers[-new_clause[1]] << new_clause
        lbd += seen_levels.size

        learned = LearnedClause.new(new_clause, lbd)
        @stat_nb_learned += 1
        @learned_clauses << learned
        @clause_to_learned_clause[new_clause.object_id] = learned
      end

      @lbd_stats.push(@trail.size, lbd)

      return backtrack_level, new_clause
    end

    # Minimizes the learned clause by removing irrelevant literals.
    def minimize_learned(new_clause, seen)
      j = 1

      (1...new_clause.size).each do |i|
        lit = new_clause[i]
        reason = @reasons[lit.abs]
        if reason.nil?
          new_clause[j] = lit
          j += 1
          next
        end

        if (1...reason.size).any? { |k| !seen.include?(reason[k].abs) && @dec_levels[reason[k].abs] > 0 }
          new_clause[j] = lit
          j += 1
          next
        end
      end

      (new_clause.size - j).times { new_clause.pop }
      nil
    end

    # Reduces the learned clauses depending on their activity and LBD.
    def reduce_learned
      @learned_clauses.sort! do |a, b|
        cmp = a.lbd <=> b.lbd
        cmp.zero? ? a.activity <=> b.activity : -cmp
      end

      learned_clause_size = @learned_clauses.size
      length = learned_clause_size / 2
      postpone_nb_max_learned_clauses if @learned_clauses[length].lbd <= 3

      nb_deleted = 0
      length.times do |i|
        learned = @learned_clauses[i]
        next if learned.lbd <= 2 || learned.locked?

        nb_deleted += 1
        @stat_nb_deleted += 1
        @learned_clauses[i] = @learned_clauses.pop

        delete_learned_clause(learned)
      end

      nil
    end

    # Deletes the learned clause from watcher lists.
    def delete_learned_clause(learned)
      object_id = learned.clause.object_id
      @clause_to_learned_clause.delete(object_id)

      ws1 = @watchers[-learned.clause[0]]
      index1 = ws1.index { |x| x.object_id == object_id }
      ws1.delete_at(index1) if index1

      ws2 = @watchers[-learned.clause[1]]
      index2 = ws2.index { |x| x.object_id == object_id }
      ws2.delete_at(index2) if index2

      nil
    end

    # Returns the status of the given literal in the current model.
    # If it returns `true`, the literal is satisfied; if it returns `false`, the literal is falsified;
    # and, if it returns `nil`, the literal is unassigned.
    def lit_status(lit)
      var = lit.abs
      return nil unless @model.key?(var)
      @model[var] == (lit > 0)
    end

    # Increments the activity of the given variable.
    def var_bump_activity(var)
      @var_activity[var] += @var_inc
      if @var_activity[var] > VarLimit
        @var_activity.map! { |a| a / VarLimit }
        @var_inc /= VarLimit
      end
      @var_queue.notify(var) if @var_queue.include?(var)
    end

    # Decays the variable activity.
    def var_decay_activity
      @var_inc /= @var_decay
    end

    # Increments the activity of the given clause.
    def clause_bump_activity(clause)
      learned = @clause_to_learned_clause[clause.object_id]
      return if learned.nil?

      learned.activity += @clause_inc
      if learned.activity > ClauseLimit
        @learned_clauses.each do |lc|
          lc.activity /= ClauseLimit
        end
        @clause_inc /= ClauseLimit
      end
    end

    # Decays the clause activity.
    def clause_decay_activity
      @clause_inc /= @clause_decay
    end

    # Increments the maximum number of learned clauses.
    def bump_nb_max_learned_clauses
      @nb_max_learned_clauses += @nb_max_learned_clauses_inc
    end

    # Postpones the maximum number of learned clauses.
    def postpone_nb_max_learned_clauses
      @nb_max_learned_clauses += @nb_max_learned_clauses_postpone_inc
    end
  end

  # An entry point of the solver program.
  def self.main(argv)
    require 'optparse'

    models = 1
    config = {}
    opt = OptionParser.new

    opt.on('-n INT', '--models INT') { |v| models = v.to_i }
    opt.on('--var-inc FLOAT') { |v| config[:var_inc] = v.to_f }
    opt.on('--var-decay FLOAT') { |v| config[:var_decay] = v.to_f }
    opt.on('--clause-inc FLOAT') { |v| config[:clause_inc] = v.to_f }
    opt.on('--clause-decay FLOAT') { |v| config[:clause_decay] = v.to_f }
    opt.on('--nb-max-learned-clauses INT') { |v| config[:nb_max_learned_clauses] = v.to_i }
    opt.on('--nb-max-learned-clauses-postpone-inc INT') { |v| config[:nb_max_learned_clauses_postpone_inc] = v.to_i }
    opt.on('--nb-max-learned-clauses-inc INT') { |v| config[:nb_max_learned_clauses_inc] = v.to_i }
    opt.on('--nb-max-lbd INT') { |v| config[:nb_max_lbd] = v.to_i }
    opt.on('--nb-max-trail INT') { |v| config[:nb_max_trail] = v.to_i }
    opt.on('--trigger-restart-k FLOAT') { |v| config[:trigger_restart_k] = v.to_f }
    opt.on('--postpone-restart-t FLOAT') { |v| config[:postpone_restart_t] = v.to_f }
    opt.on('--random-seed INT') { |v| config[:random_seed] = v.to_i }
    opt.on('--random-freq FLOAT') { |v| config[:random_freq] = v.to_f }

    argv = opt.parse!(argv)

    problem = load_cnf(File.read(argv[0]))
    solver = Solver.new(problem, config)

    nb_answer = 0
    solver.each do |model|
      nb_answer += 1
      puts "c Answer #{nb_answer}"

      values = model.keys.map { |k| model[k] ? k : -k }.sort_by(&:abs)
      puts "v #{values.join(' ')} 0"

      break if models != 0 && models == nb_answer
    end

    puts "s #{nb_answer > 0 ? "SATISFIABLE" : "UNSATISFIABLE"}"

    stats = solver.stats
    puts "c      random seed: #{stats[:random_seed]}"
    puts "c         restarts: #{stats[:nb_restarts]}"
    puts "c        conflicts: #{stats[:nb_conflicts]}"
    puts "c        decisions: #{stats[:nb_decisions]}"
    puts "c random decisions: #{stats[:nb_random_decisions]}"
    puts "c     propagations: #{stats[:nb_propagations]}"
    puts "c  learned clauses: #{stats[:nb_learned]}"
    puts "c  deleted clauses: #{stats[:nb_deleted]}"
  end
end

KiriMochi.main(ARGV) if __FILE__ == $0