Class: PropLogic::Minisat::IncrementalSolver

Inherits:
Object
  • Object
show all
Defined in:
lib/prop_logic/minisat/incremental_solver.rb

Overview

Note:

currently only Ruby part is incremental.

Incremental solver using minisat.

Instance Method Summary collapse

Constructor Details

#initialize(initial_term) ⇒ IncrementalSolver

constructor.

Parameters:

  • initial (Term) —

    term for starting SAT solver.



13
14
15
16
17
18
19
20
21
22
 
# File 'lib/prop_logic/minisat/incremental_solver.rb', line 13

def initialize(initial_term)
  @solver = ::MiniSat::Solver.new
  # automagically add variable in Hash
  @variables_map = Hash.new { |h, k| h[k] = @solver.new_var }
  @terms = []
  @variables = []
  # true if False was added
  @contradicted = false
  add initial_term
end

Instance Method Details

#add(*terms) ⇒ IncrementalSolver Also known as: <<

add terms to this solver.

Returns:



37
38
39
40
 
# File 'lib/prop_logic/minisat/incremental_solver.rb', line 37

def add(*terms)
  terms.each { |term| add_one_term term }
  self
end

#sat? ⇒ Term, false

check if terms are satisfiable.

Returns:

  • (Term) —

    term satisfying conditions.

  • (false) —

    if unsatisfied.



47
48
49
50
51
52
53
54
55
56
57
58
 
# File 'lib/prop_logic/minisat/incremental_solver.rb', line 47

def sat?
  return false if @contradicted
  return True if variables.empty?
  vars = []
  unless @terms.empty?
    return false unless @solver.solve
    ret_vars = variables & @variables_map.keys
    vars = ret_vars.map { |k| @solver[@variables_map[k]] ? k : ~k }
  end
  extra_vars = variables - @variables_map.keys
  PropLogic.all_and(*vars, *extra_vars)
end

#term ⇒ Object 



29
30
31
32
33
 
# File 'lib/prop_logic/minisat/incremental_solver.rb', line 29

def term
  return False if @contradicted
  return True if @terms.empty?
  PropLogic.all_and(*@terms)
end

#variables ⇒ Array

Returns containing variables.

Returns:

  • (Array) —

    containing variables



25
26
27
 
# File 'lib/prop_logic/minisat/incremental_solver.rb', line 25

def variables
  @variables.dup
end