Class: TwoSAT

Inherits:
Object
  • Object
show all
Defined in:
lib/two_sat.rb

Overview

TwoSAT Reference: github.com/atcoder/ac-library/blob/master/atcoder/twosat.hpp

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(n) ⇒ TwoSAT

Returns a new instance of TwoSAT.



6
7
8
9
10
 
# File 'lib/two_sat.rb', line 6

def initialize(n)
  @n = n
  @answer = Array.new(n)
  @scc = SCC.new(2 * n)
end

Instance Attribute Details

#answer ⇒ Object (readonly)

Returns the value of attribute answer.



12
13
14
 
# File 'lib/two_sat.rb', line 12

def answer
  @answer
end

Instance Method Details

#add_clause(i, f, j, g) ⇒ Object 



14
15
16
17
18
19
20
21
22
 
# File 'lib/two_sat.rb', line 14

def add_clause(i, f, j, g)
  unless 0 <= i && i < @n && 0 <= j && j < @n
    raise ArgumentError.new("i:#{i} and j:#{j} must be in (0...#{@n})")
  end

  @scc.add_edge(2 * i + (f ? 0 : 1), 2 * j + (g ? 1 : 0))
  @scc.add_edge(2 * j + (g ? 0 : 1), 2 * i + (f ? 1 : 0))
  nil
end

#satisfiable? ⇒ Boolean Also known as: satisfiable

Returns:

  • (Boolean) 


24
25
26
27
28
29
30
31
32
 
# File 'lib/two_sat.rb', line 24

def satisfiable?
  id = @scc.send(:scc_ids)[1]
  @n.times do |i|
    return false if id[2 * i] == id[2 * i + 1]

    @answer[i] = id[2 * i] < id[2 * i + 1]
  end
  true
end