Packages
fixpoint
0.8.44
0.22.1
0.21.5
0.21.4
0.21.3
0.21.2
0.21.1
0.21.0
0.20.6
0.20.5
0.20.4
0.20.3
0.20.2
0.20.1
0.19.5
0.19.4
0.19.3
0.19.2
0.19.1
0.18.2
0.18.1
0.17.6
0.17.5
0.17.4
0.17.3
0.17.2
0.17.1
0.16.5
0.16.4
0.16.3
0.16.2
0.16.1
0.16.0
0.15.6
0.15.5
0.15.4
0.15.3
0.15.2
0.15.1
0.15.0
0.14.9
0.14.8
0.14.7
0.14.6
0.14.5
0.14.4
0.14.3
0.14.2
0.14.1
0.13.5
0.13.4
0.13.2
0.13.1
0.12.9
0.12.8
0.12.7
0.12.6
0.12.5
0.12.4
0.12.2
0.12.1
0.11.8
0.11.7
0.11.6
0.11.5
0.11.4
0.11.3
0.11.2
0.11.1
0.10.7
0.10.6
0.10.5
0.10.4
0.10.3
0.10.2
0.10.1
0.9.12
0.9.11
0.9.10
0.9.9
0.9.8
0.9.7
0.9.6
0.9.5
0.9.4
0.9.3
0.9.2
0.9.1
0.9.0
0.8.52
0.8.51
0.8.50
0.8.49
0.8.48
0.8.46
0.8.44
0.8.43
0.8.42
0.8.41
0.8.40
0.8.39
0.8.38
0.8.37
0.8.36
0.8.35
0.8.34
0.8.33
0.8.32
0.8.31
0.8.30
0.8.29
0.8.28
0.8.27
0.8.26
0.8.25
0.8.24
0.8.23
0.8.22
0.8.21
0.8.20
0.8.19
0.8.18
0.8.17
0.8.16
0.8.15
0.8.14
0.8.13
0.8.12
0.8.11
0.8.10
0.8.9
0.8.8
0.8.7
0.8.6
0.8.5
0.8.4
0.8.3
0.8.2
0.8.1
0.8.0
0.7.10
0.7.9
0.7.8
0.7.7
0.7.6
0.7.5
0.7.4
0.7.3
0.7.2
0.7.1
0.7.0
0.6.5
0.6.4
0.6.3
0.6.2
0.6.1
0.6.0
0.5.12
0.5.11
0.5.10
0.5.9
0.5.8
0.5.7
0.5.6
0.5.5
0.5.4
0.5.3
0.5.2
0.5.1
0.5.0
0.4.3
0.4.2
0.4.1
0.4.0
0.3.6
0.3.5
0.3.4
0.3.3
0.3.2
0.3.1
0.3.0
0.2.3
0.2.2
0.2.1
0.1.3
0.1.2
0.1.1
0.1.0
Constraint Programming Solver
Current section
Files
Jump to
Current section
Files
lib/examples/sat_solver.ex
defmodule CPSolver.Examples.SatSolver do
alias CPSolver.Constraint.Or
alias CPSolver.Model
alias CPSolver.BooleanVariable
alias CPSolver.Variable.Interface
import CPSolver.Variable.View.Factory
@moduledoc """
This module solves SAT problems represented in CNF form.
It's a list of lists of integers, where a positive integer `i` represents a boolean variable mapped to `i`,
and a negative integer `j` represents negation of a boolean variable mapped to `j`.
Examples of CNF representation:
```elixir
# x1 AND (NOT x1)
[[1], [-1]]
# x1 AND (x1 OR x2 OR x3)
[[1], [1, 2, 3]]
# x1 AND x2 AND x3
[[1], [2], [3]]
```
"""
def solve(clauses) do
model = model(clauses)
{:ok, res} =
CPSolver.solve_sync(model,
search: {:first_fail, :indomain_max},
stop_on: {:max_solutions, 1}
)
res.status != :unsatisfiable && hd(res.solutions) |> sort_by_variables(res.variables)
end
def model(clauses) do
{vars, constraints} =
Enum.reduce(clauses, {Map.new(), []}, fn clause, {vars_acc, constraints_acc} ->
{clause_vars, new_vars_acc} = build_clause(clause, vars_acc)
{new_vars_acc, [Or.new(clause_vars) | constraints_acc]}
end)
final_vars =
Enum.flat_map(vars, fn {literal_id, var} -> (literal_id > 0 && [var]) || [] end)
|> Enum.sort_by(fn var -> Interface.variable(var).name end)
Model.new(final_vars, constraints)
end
def check_solution(solution, clauses) do
## Transform the solution into the form compatible with clause representation.
cnf_solution = to_cnf(solution)
Enum.all?(clauses, fn clause ->
Enum.any?(clause, fn literal -> literal in cnf_solution end)
end)
end
def to_cnf(solution) do
Enum.reduce(Enum.with_index(solution, 1), MapSet.new(),
fn {bool, idx}, acc ->
set_val = (bool == 0 && -idx || idx)
MapSet.put(acc, set_val)
end)
end
defp build_clause(clause, literal_map) do
Enum.reduce(clause, {[], literal_map}, fn literal, {clause_acc, literal_map_acc} ->
## Get or create literal variable
## Has literal variable been already registered?
{literal_var, updated_literal_map} =
case Map.get(literal_map_acc, literal) do
nil ->
## New literal variable, create it and update the literal map
new_literal_variable = create_variable(literal, Map.get(literal_map_acc, -literal))
{new_literal_variable, Map.put(literal_map_acc, literal, new_literal_variable)}
existing_literal_variable ->
{existing_literal_variable, literal_map_acc}
end
{[literal_var | clause_acc], updated_literal_map}
end)
end
## Creates a literal variable
defp create_variable(var_id, nil) when is_integer(var_id) do
## No literal variable of opposite sign
var = BooleanVariable.new(name: "#{abs(var_id)}")
(var_id > 0 && var) || negation(var)
end
defp create_variable(var_id, negation) when var_id > 0 do
Interface.variable(negation)
end
defp create_variable(var_id, positive_literal_variable) when var_id < 0 do
negation(positive_literal_variable)
end
defp sort_by_variables(solution, variables) do
Enum.zip(solution, variables)
|> Enum.sort_by(fn {_val, var_name} -> var_name end)
|> Enum.map(fn {val, _var_name} -> val end)
end
end