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
test/examples/sat_test.exs
defmodule CPSolverTest.Examples.SatSolver do
@moduledoc """
Most test cases are borrowed from:
https://github.com/ash-project/simple_sat/blob/main/test/simple_sat_test.exs
"""
use ExUnit.Case
alias CPSolver.Examples.SatSolver
alias CPSolver.Search.Strategy
test "simple unsatisfiable" do
assert_unsatisfiable([[1], [-1]])
end
test "slightly more complex unsatisfiable" do
assert_unsatisfiable([[1, 2], [-1, -2], [1], [2]])
end
test "single variable" do
assert [1] = SatSolver.solve([[1]])
end
test "three variables" do
assert_satisfiable([[1, 3], [2], [1, -2, 3]])
end
test "many single-variable clauses" do
assert_satisfiable([[7], [-8], [6], [-5], [-4], [-3], [2], [-1]])
end
test "bigger instance" do
clauses = [
[1],
[-3],
[-7],
[6],
[-5],
[-4],
[3, 2],
[1, 2],
[-7, -6, 5, 4, 3, -1, -2]
]
assert_satisfiable(clauses)
end
test "voting (https://github.com/bitwalker/picosat_elixir/blob/main/README.md#example)" do
assert MapSet.new([-2, 1, 3]) ==
SatSolver.solve([
[1, 2, -3],
[2, 3],
[-2],
[-1, 3]
])
|> SatSolver.to_cnf()
end
@tag :slow
test "Dimacs (sat/unsat, 50 vars, 218 clauses)" do
assert_satisfiable(:sat50_218)
assert_unsatisfiable(:unsat50_218)
end
@tag :slow
test "Dimacs (sat/unsat, 100 vars, 430 clauses)" do
assert_satisfiable(:sat100_430)
assert_unsatisfiable(:unsat100_430)
end
@tag :superslow
test "Dimacs (sat/unsat, 150 vars, 645 clauses)" do
assert_satisfiable(:sat150_645)
assert_unsatisfiable(:unsat150_645)
end
defp assert_satisfiable(clauses) do
solution = SatSolver.solve(clauses,
search: {
Strategy.chb(:chb_size_min, Strategy.most_completed(&Enum.random/1)), :indomain_max})
assert SatSolver.check_solution(solution, clauses)
end
defp assert_unsatisfiable(clauses) do
assert :unsatisfiable == SatSolver.solve(clauses,
timeout: :timer.minutes(1),
search: {
Strategy.mixed([
#&Enum.random/1,
#:dom_deg,
Strategy.chb(:chb_size_min, Strategy.most_completed(Strategy.most_constrained()))]),
:indomain_max}
)
end
end