def deps do
  [
    {:crux, "~> 0.1.2"},
    # Choose one SAT solver backend:
    {:picosat_elixir, "~> 0.2"}, # Recommended: Fast NIF-based solver
    # OR
    {:simple_sat, "~> 0.1"}      # Pure Elixir alternative
  ]
end

import Crux.Expression

# Basic boolean operations
expr = b(:user_logged_in and (:is_admin or :is_moderator))

# Advanced boolean operators
expr = b(xor(:payment_cash, :payment_card))  # exactly one payment method
expr = b(implies(:is_student, :gets_discount)) # if student then discount

alias Crux.{Expression, Formula}

# Create and solve a formula
expression = Expression.b(:a and (:b or :c))
formula = Formula.from_expression(expression)

case Crux.solve(formula) do
  {:ok, solution} ->
    IO.inspect(solution) # %{a: true, b: true, c: false}
  {:error, :unsatisfiable} ->
    IO.puts("No solution exists")
end

import Crux.Expression

# Simplify expressions
complex_expr = b((:a and true) or (false and :b))
simple_expr = Expression.simplify(complex_expr)  # :a

# Evaluate with variable assignments
result = Expression.run(b(:a and :b), fn
  :a -> true
  :b -> false
end)  # false

# Convert to Conjunctive Normal Form
cnf_expr = Expression.to_cnf(b(:a or (:b and :c)))

formula = Formula.from_expression(Expression.b(:a and :b))
# %Formula{
#   cnf: [[1], [2]],
#   bindings: %{1 => :a, 2 => :b},
#   reverse_bindings: %{a: 1, b: 2}
# }

# Check satisfiability
Crux.satisfiable?(formula)  # true/false

# Find all satisfying scenarios
Crux.satisfying_scenarios(formula)  # [%{a: true, b: true}]

# Build decision trees
tree = Crux.decision_tree(formula)  # {:a, false, {:b, false, true}}

# Creation
Expression.b(:a and :b)

# Manipulation
Expression.simplify/1      # Simplify expressions
Expression.to_cnf/1        # Convert to CNF
Expression.balance/1       # Normalize operand order

# Evaluation
Expression.run/2           # Evaluate with variable bindings
Expression.expand/2        # Expand with custom callbacks

# Traversal
Expression.prewalk/2       # Pre-order traversal
Expression.postwalk/2      # Post-order traversal

# Constraint helpers
Expression.at_most_one/1   # At most one variable true
Expression.exactly_one/1   # Exactly one variable true
Expression.all_or_none/1   # All variables same value

{:picosat_elixir, "~> 0.2"}

{:simple_sat, "~> 0.1"}

formula = Formula.from_expression(Expression.b(:a and :b))
tree = Crux.decision_tree(formula, sorter: &<=/2)
# {:a, false, {:b, false, true}}

import Crux.Expression

# User can have at most one role
roles = [:admin, :moderator, :user]
at_most_one_role = at_most_one(roles)

# Payment methods - exactly one must be selected
payment_methods = [:cash, :card, :paypal]
payment_constraint = exactly_one(payment_methods)

# Feature flags - all related features synchronized
related_features = [:dark_mode_ui, :dark_mode_api]
sync_constraint = all_or_none(related_features)

opts = [
  conflicts?: fn
    :admin, :guest -> true    # admin and guest roles conflict
    _, _ -> false
  end,
  implies?: fn
    :admin, :can_delete -> true  # admin implies delete permission
    _, _ -> false
  end
]

scenarios = Crux.satisfying_scenarios(formula, opts)

import Crux.Expression

# User access policy
policy = b(
  (:is_owner or :is_admin) and
  not :is_suspended and
  (:has_subscription or :is_trial_user)
)

# Check if a specific user satisfies the policy
user_context = %{
  is_owner: false,
  is_admin: true,
  is_suspended: false,
  has_subscription: true,
  is_trial_user: false
}

result = Expression.run(policy, fn var -> Map.get(user_context, var, false) end)

case result do
  true -> :access_granted
  false -> :access_denied
end

# Meeting room scheduling
rooms = [:room_a, :room_b, :room_c]
time_slots = [:slot_1, :slot_2, :slot_3]

constraints = for room <- rooms do
  # Each room can be booked at most once per time slot
  at_most_one(for slot <- time_slots, do: :"#{room}_#{slot}")
end