Packages
fixpoint
0.9.6
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
alias CPSolver.Search.Strategy
import CPSolver.Variable.View.Factory
require Logger
@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, opts \\ []) do
Keyword.get(opts, :print) && Logger.configure(level: :notice)
model = model(clauses)
default_opts =
[
search: {
#:most_completed,
#Strategy.most_completed(&Enum.random/1),
Strategy.mixed(
[
Strategy.most_completed(
Strategy.first_fail(&Enum.random/1))
#Strategy.afc({:afc_min, 0.9}, Strategy.first_fail(&Enum.random/1)))
]),
:indomain_max
},
stop_on: {:max_solutions, 1}
]
{:ok, res} =
CPSolver.solve(
model,
Keyword.merge(default_opts, opts)
)
cond do
res.status == :unsatisfiable ->
:unsatisfiable
Enum.empty?(res.solutions) ->
:unknown
true ->
List.first(res.solutions) |> sort_by_variables(res.variables)
end
|> tap(fn _ -> Logger.notice(inspect(res, pretty: true)) end)
end
def model(dimacs_instance) when is_atom(dimacs_instance) do
dimacs_instance
|> clauses()
|> model()
end
def model(clauses) when is_list(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
## We assume it's a 3-SAT instance
def clauses(dimacs_instance) do
dimacs_instances()
|> Map.get(dimacs_instance)
|> File.read!()
|> String.split("\n")
|> Enum.flat_map(fn line ->
case String.split(line, " ", trim: true) do
[x1, x2, x3, _0] = _clause when x1 not in ["p", "c"] ->
[Enum.map([x1, x2, x3], fn x -> String.to_integer(x) end)]
_other ->
[]
end
end)
end
def check_solution(solution, dimacs_instance) when is_atom(dimacs_instance) do
dimacs_instance
|> clauses()
|> then(fn clauses -> check_solution(solution, clauses) end)
end
def check_solution(solution, clauses) when is_list(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
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} -> String.to_integer(var_name) end)
|> Enum.map(fn {val, _var_name} -> val end)
end
def dimacs_instances() do
%{
sat50_218: "data/sat/uf50-01.cnf",
unsat50_218: "data/sat/uuf50-01.cnf",
sat100_430: "data/sat/uf100-01.cnf",
unsat100_430: "data/sat/uuf100-01.cnf",
sat150_645: "data/sat/uf150-01.cnf",
unsat150_645: "data/sat/uuf150-01.cnf"
}
end
end