Packages
fixpoint
0.9.0
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
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 "2 instances (50 vars, 218 clauses) from Dimacs" do
assert_satisfiable(:sat50_218)
assert_unsatisfiable(:unsat50_218)
end
@tag :slow
test "2 bigger instances (100 vars, 403 clauses) from Dimacs" do
assert_satisfiable(:sat100_403)
assert_unsatisfiable(:unsat100_403)
end
defp assert_satisfiable(clauses) do
solution = SatSolver.solve(clauses)
assert SatSolver.check_solution(solution, clauses)
end
defp assert_unsatisfiable(clauses) do
assert :unsatisfiable == SatSolver.solve(clauses)
end
end