diff --git a/internal/solver/bench_test.go b/internal/solver/bench_test.go
index 289a016..59f46f3 100644
--- a/internal/solver/bench_test.go
+++ b/internal/solver/bench_test.go
@@ -7,7 +7,7 @@ import (
 	"testing"
 )
 
-var BenchmarkInput = func() []Variable {
+var BenchmarkConstraints = func() []Constraint {
 	const (
 		length      = 256
 		seed        = 9
@@ -22,10 +22,11 @@ var BenchmarkInput = func() []Variable {
 		return Identifier(strconv.Itoa(i))
 	}
 
-	variable := func(i int) TestVariable {
+	input := func(i int) []Constraint {
 		var c []Constraint
+		subject := id(i)
 		if rand.Float64() < pMandatory {
-			c = append(c, Mandatory())
+			c = append(c, Mandatory(subject))
 		}
 		if rand.Float64() < pDependency {
 			n := rand.Intn(nDependency-1) + 1
@@ -37,7 +38,7 @@ var BenchmarkInput = func() []Variable {
 				}
 				d = append(d, id(y))
 			}
-			c = append(c, Dependency(d...))
+			c = append(c, Dependency(subject, d...))
 		}
 		if rand.Float64() < pConflict {
 			n := rand.Intn(nConflict-1) + 1
@@ -46,39 +47,34 @@ var BenchmarkInput = func() []Variable {
 				for y == i {
 					y = rand.Intn(length)
 				}
-				c = append(c, Conflict(id(y)))
+				c = append(c, Conflict(subject, id(y)))
 			}
 		}
-		return TestVariable{
-			identifier:  id(i),
-			constraints: c,
-		}
+		return c
 	}
 
 	rand.Seed(seed)
-	result := make([]Variable, length)
-	for i := range result {
-		result[i] = variable(i)
+	constraints := make([]Constraint, 0)
+	for i := 0; i < length; i++ {
+		constrs := input(i)
+		constraints = append(constraints, constrs...)
 	}
-	return result
+	return constraints
 }()
 
 func BenchmarkSolve(b *testing.B) {
 	for i := 0; i < b.N; i++ {
-		s, err := New(WithInput(BenchmarkInput))
-		if err != nil {
-			b.Fatalf("failed to initialize solver: %s", err)
-		}
-		_, err = s.Solve(context.Background())
+		s, err := New(WithInput(BenchmarkConstraints))
 		if err != nil {
 			b.Fatalf("failed to initialize solver: %s", err)
 		}
+		s.Solve(context.Background())
 	}
 }
 
 func BenchmarkNewInput(b *testing.B) {
 	for i := 0; i < b.N; i++ {
-		_, err := New(WithInput(BenchmarkInput))
+		_, err := New(WithInput(BenchmarkConstraints))
 		if err != nil {
 			b.Fatalf("failed to initialize solver: %s", err)
 		}
diff --git a/internal/solver/constraints.go b/internal/solver/constraints.go
index b2b0b77..70e23ce 100644
--- a/internal/solver/constraints.go
+++ b/internal/solver/constraints.go
@@ -8,176 +8,173 @@ import (
 	"github.com/go-air/gini/z"
 )
 
-// Constraint implementations limit the circumstances under which a
-// particular Variable can appear in a solution.
 type Constraint interface {
-	String(subject Identifier) string
-	apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit
 	order() []Identifier
 	anchor() bool
+	apply(c *logic.C, lm *litMapping) z.Lit
+	String() string
+	Subject() Identifier
 }
 
-// zeroConstraint is returned by ConstraintOf in error cases.
-type zeroConstraint struct{}
-
-var _ Constraint = zeroConstraint{}
-
-func (zeroConstraint) String(subject Identifier) string {
-	return ""
+type mandatory struct {
+	subject Identifier
 }
 
-func (zeroConstraint) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
-	return z.LitNull
+func (constraint *mandatory) String() string {
+	return fmt.Sprintf("%s is mandatory", constraint.subject)
 }
 
-func (zeroConstraint) order() []Identifier {
-	return nil
+func (constraint *mandatory) apply(_ *logic.C, lm *litMapping) z.Lit {
+	return lm.LitOf(constraint.subject)
 }
 
-func (zeroConstraint) anchor() bool {
-	return false
+func (constraint *mandatory) order() []Identifier {
+	return nil
 }
 
-// AppliedConstraint values compose a single Constraint with the
-// Variable it applies to.
-type AppliedConstraint struct {
-	Variable   Variable
-	Constraint Constraint
+func (constraint *mandatory) anchor() bool {
+	return true
 }
 
-// String implements fmt.Stringer and returns a human-readable message
-// representing the receiver.
-func (a AppliedConstraint) String() string {
-	return a.Constraint.String(a.Variable.Identifier())
+func (constraint *mandatory) Subject() Identifier {
+	return constraint.subject
 }
 
-type mandatory struct{}
-
-func (constraint mandatory) String(subject Identifier) string {
-	return fmt.Sprintf("%s is mandatory", subject)
+func Mandatory(subject Identifier) Constraint {
+	return &mandatory{
+		subject: subject,
+	}
 }
 
-func (constraint mandatory) apply(_ *logic.C, lm *litMapping, subject Identifier) z.Lit {
-	return lm.LitOf(subject)
+type prohibited struct {
+	subject Identifier
 }
 
-func (constraint mandatory) order() []Identifier {
+func (constraint *prohibited) order() []Identifier {
 	return nil
 }
 
-func (constraint mandatory) anchor() bool {
-	return true
-}
-
-// Mandatory returns a Constraint that will permit only solutions that
-// contain a particular Variable.
-func Mandatory() Constraint {
-	return mandatory{}
+func (constraint *prohibited) anchor() bool {
+	return false
 }
 
-type prohibited struct{}
-
-func (constraint prohibited) String(subject Identifier) string {
-	return fmt.Sprintf("%s is prohibited", subject)
+func (constraint *prohibited) apply(c *logic.C, lm *litMapping) z.Lit {
+	return lm.LitOf(constraint.subject).Not()
 }
 
-func (constraint prohibited) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
-	return lm.LitOf(subject).Not()
+func (constraint *prohibited) String() string {
+	return fmt.Sprintf("%s is prohibited", constraint.subject)
 }
 
-func (constraint prohibited) order() []Identifier {
-	return nil
+func (constraint *prohibited) Subject() Identifier {
+	return constraint.subject
 }
 
-func (constraint prohibited) anchor() bool {
-	return false
+func Prohibited(subject Identifier) Constraint {
+	return &prohibited{
+		subject: subject,
+	}
 }
 
-// Prohibited returns a Constraint that will reject any solution that
-// contains a particular Variable. Callers may also decide to omit
-// an Variable from input to Solve rather than apply such a
-// Constraint.
-func Prohibited() Constraint {
-	return prohibited{}
+type dependency struct {
+	subject      Identifier
+	dependencies []Identifier
 }
 
-type dependency []Identifier
-
-func (constraint dependency) String(subject Identifier) string {
-	if len(constraint) == 0 {
-		return fmt.Sprintf("%s has a dependency without any candidates to satisfy it", subject)
+func (constraint *dependency) String() string {
+	if len(constraint.dependencies) == 0 {
+		return fmt.Sprintf("%s has a dependency without any candidates to satisfy it", constraint.subject)
 	}
-	s := make([]string, len(constraint))
-	for i, each := range constraint {
+	s := make([]string, len(constraint.dependencies))
+	for i, each := range constraint.dependencies {
 		s[i] = string(each)
 	}
-	return fmt.Sprintf("%s requires at least one of %s", subject, strings.Join(s, ", "))
+	return fmt.Sprintf("%s requires at least one of %s", constraint.subject, strings.Join(s, ", "))
 }
 
-func (constraint dependency) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
-	m := lm.LitOf(subject).Not()
-	for _, each := range constraint {
-		m = c.Or(m, lm.LitOf(each))
+func (constraint *dependency) apply(c *logic.C, lm *litMapping) z.Lit {
+	m := lm.LitOf(constraint.subject).Not()
+	ms := make([]z.Lit, len(constraint.dependencies))
+	for i, each := range constraint.dependencies {
+		ms[i] = lm.LitOf(each)
 	}
-	return m
+	return c.Ors(append(ms, m)...)
 }
 
-func (constraint dependency) order() []Identifier {
-	return constraint
+func (constraint *dependency) order() []Identifier {
+	return constraint.dependencies
 }
 
-func (constraint dependency) anchor() bool {
+func (constraint *dependency) anchor() bool {
 	return false
 }
 
+func (constraint *dependency) Subject() Identifier {
+	return constraint.subject
+}
+
 // Dependency returns a Constraint that will only permit solutions
-// containing a given Variable on the condition that at least one
-// of the Variables identified by the given Identifiers also
+// containing a given *DeppyEntity on the condition that at least one
+// of the Entities identified by the given Identifiers also
 // appears in the solution. Identifiers appearing earlier in the
 // argument list have higher preference than those appearing later.
-func Dependency(ids ...Identifier) Constraint {
-	return dependency(ids)
+func Dependency(subject Identifier, dependencies ...Identifier) Constraint {
+	return &dependency{
+		subject:      subject,
+		dependencies: dependencies,
+	}
 }
 
-type conflict Identifier
+type conflict struct {
+	subject  Identifier
+	conflict Identifier
+}
 
-func (constraint conflict) String(subject Identifier) string {
-	return fmt.Sprintf("%s conflicts with %s", subject, constraint)
+func (constraint *conflict) String() string {
+	return fmt.Sprintf("%s conflicts with %s", constraint.subject, constraint.conflict)
 }
 
-func (constraint conflict) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
-	return c.Or(lm.LitOf(subject).Not(), lm.LitOf(Identifier(constraint)).Not())
+func (constraint *conflict) apply(c *logic.C, lm *litMapping) z.Lit {
+	return c.Or(lm.LitOf(constraint.subject).Not(), lm.LitOf(constraint.conflict).Not())
 }
 
-func (constraint conflict) order() []Identifier {
+func (constraint *conflict) order() []Identifier {
 	return nil
 }
 
-func (constraint conflict) anchor() bool {
+func (constraint *conflict) anchor() bool {
 	return false
 }
 
+func (constraint *conflict) Subject() Identifier {
+	return constraint.subject
+}
+
 // Conflict returns a Constraint that will permit solutions containing
-// either the constrained Variable, the Variable identified by
+// either the constrained *DeppyEntity, the *DeppyEntity identified by
 // the given Identifier, or neither, but not both.
-func Conflict(id Identifier) Constraint {
-	return conflict(id)
+func Conflict(subject Identifier, conlict Identifier) Constraint {
+	return &conflict{
+		subject:  subject,
+		conflict: conlict,
+	}
 }
 
-type leq struct {
-	ids []Identifier
-	n   int
+type atMost struct {
+	subject Identifier
+	ids     []Identifier
+	n       int
 }
 
-func (constraint leq) String(subject Identifier) string {
+func (constraint *atMost) String() string {
 	s := make([]string, len(constraint.ids))
 	for i, each := range constraint.ids {
 		s[i] = string(each)
 	}
-	return fmt.Sprintf("%s permits at most %d of %s", subject, constraint.n, strings.Join(s, ", "))
+	return fmt.Sprintf("at most %d of %s are permitted", constraint.n, strings.Join(s, ", "))
 }
 
-func (constraint leq) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
+func (constraint *atMost) apply(c *logic.C, lm *litMapping) z.Lit {
 	ms := make([]z.Lit, len(constraint.ids))
 	for i, each := range constraint.ids {
 		ms[i] = lm.LitOf(each)
@@ -185,20 +182,171 @@ func (constraint leq) apply(c *logic.C, lm *litMapping, subject Identifier) z.Li
 	return c.CardSort(ms).Leq(constraint.n)
 }
 
-func (constraint leq) order() []Identifier {
+func (constraint *atMost) order() []Identifier {
 	return nil
 }
 
-func (constraint leq) anchor() bool {
+func (constraint *atMost) anchor() bool {
 	return false
 }
 
+func (constraint *atMost) Subject() Identifier {
+	return ""
+}
+
 // AtMost returns a Constraint that forbids solutions that contain
-// more than n of the Variables identified by the given
+// more than n of the Entities identified by the given
 // Identifiers.
-func AtMost(n int, ids ...Identifier) Constraint {
-	return leq{
-		ids: ids,
-		n:   n,
+func AtMost(subject Identifier, n int, ids ...Identifier) Constraint {
+	return &atMost{
+		subject: subject,
+		ids:     ids,
+		n:       n,
+	}
+}
+
+type and struct {
+	clauses []Constraint
+}
+
+func And(clauses ...Constraint) Constraint {
+	return &and{
+		clauses: clauses,
+	}
+}
+
+func (constraint *and) String() string {
+	collectIds := func() []string {
+		ids := make([]string, len(constraint.clauses))
+		for i, clause := range constraint.clauses {
+			ids[i] = clause.String()
+		}
+		return ids
+	}
+	return fmt.Sprintf("%s are required", strings.Join(collectIds(), " and "))
+}
+
+func (constraint *and) apply(c *logic.C, lm *litMapping) z.Lit {
+	collectTerms := func() []z.Lit {
+		terms := make([]z.Lit, len(constraint.clauses))
+		for i, clause := range constraint.clauses {
+			terms[i] = clause.apply(c, lm)
+		}
+		return terms
 	}
+	return c.Ands(collectTerms()...)
+}
+
+func (constraint *and) order() []Identifier {
+	return nil
+}
+
+func (constraint *and) anchor() bool {
+	return false
+}
+
+func (constraint *and) Subject() Identifier {
+	return ""
+}
+
+type or struct {
+	clauses []Constraint
+}
+
+func Or(clauses ...Constraint) Constraint {
+	return &or{
+		clauses: clauses,
+	}
+}
+
+func (constraint *or) String() string {
+	collectIds := func() []string {
+		ids := make([]string, len(constraint.clauses))
+		for i, clause := range constraint.clauses {
+			ids[i] = clause.String()
+		}
+		return ids
+	}
+	return fmt.Sprintf("%s are required", strings.Join(collectIds(), " or "))
+}
+
+func (constraint *or) apply(c *logic.C, lm *litMapping) z.Lit {
+	collectTerms := func() []z.Lit {
+		terms := make([]z.Lit, len(constraint.clauses))
+		for i, clause := range constraint.clauses {
+			terms[i] = clause.apply(c, lm)
+		}
+		return terms
+	}
+	return c.Ors(collectTerms()...)
+}
+
+func (constraint *or) order() []Identifier {
+	return nil
+}
+
+func (constraint *or) anchor() bool {
+	return false
+}
+
+func (constraint *or) Subject() Identifier {
+	return ""
+}
+
+type not struct {
+	clause Constraint
+}
+
+func Not(clause Constraint) Constraint {
+	return &not{
+		clause: clause,
+	}
+}
+
+func (constraint *not) String() string {
+	return fmt.Sprintf("not %s", constraint.clause.String())
+}
+
+func (constraint *not) apply(c *logic.C, lm *litMapping) z.Lit {
+	return constraint.clause.apply(c, lm).Not()
+}
+
+func (constraint *not) order() []Identifier {
+	return nil
+}
+
+func (constraint *not) anchor() bool {
+	return false
+}
+
+func (constraint *not) Subject() Identifier {
+	return ""
+}
+
+// zeroConstraint is returned by ConstraintOf in error cases.
+type zeroConstraint struct {
+}
+
+var _ Constraint = &zeroConstraint{}
+
+var ZeroConstraint = &zeroConstraint{}
+
+func (*zeroConstraint) String() string {
+	return ""
+}
+
+func (*zeroConstraint) apply(_ *logic.C, _ *litMapping) z.Lit {
+	return z.LitNull
+}
+
+func (*zeroConstraint) order() []Identifier {
+	return nil
+}
+
+func (*zeroConstraint) anchor() bool {
+	return false
+}
+
+func (*zeroConstraint) Subject() Identifier {
+	return ""
 }
diff --git a/internal/solver/constraints_test.go b/internal/solver/constraints_test.go
index 4bd0a2e..0a6b182 100644
--- a/internal/solver/constraints_test.go
+++ b/internal/solver/constraints_test.go
@@ -16,20 +16,20 @@ func TestOrder(t *testing.T) {
 	for _, tt := range []tc{
 		{
 			Name:       "mandatory",
-			Constraint: Mandatory(),
+			Constraint: Mandatory("a"),
 		},
 		{
 			Name:       "prohibited",
-			Constraint: Prohibited(),
+			Constraint: Prohibited("b"),
 		},
 		{
 			Name:       "dependency",
 			Constraint: Dependency("a", "b", "c"),
-			Expected:   []Identifier{"a", "b", "c"},
+			Expected:   []Identifier{"b", "c"},
 		},
 		{
 			Name:       "conflict",
-			Constraint: Conflict("a"),
+			Constraint: Conflict("a", "b"),
 		},
 	} {
 		t.Run(tt.Name, func(t *testing.T) {
diff --git a/internal/solver/lit_mapping.go b/internal/solver/lit_mapping.go
index eb7a739..fdefb30 100644
--- a/internal/solver/lit_mapping.go
+++ b/internal/solver/lit_mapping.go
@@ -22,94 +22,76 @@ func (inconsistentLitMapping) Error() string {
 }
 
 // litMapping performs translation between the input and output types of
-// Solve (Constraints, Variables, etc.) and the variables that
+// Solve (Constraints, Constraints, etc.) and the variables that
 // appear in the SAT formula.
 type litMapping struct {
-	inorder     []Variable
-	variables   map[z.Lit]Variable
-	lits        map[Identifier]z.Lit
-	constraints map[z.Lit]AppliedConstraint
-	c           *logic.C
-	errs        inconsistentLitMapping
+	inorder              []Constraint
+	constraintsByLiteral map[z.Lit][]Constraint
+	lits                 map[Identifier]z.Lit
+	constraints          map[z.Lit]Constraint
+	c                    *logic.C
+	errs                 inconsistentLitMapping
 }
 
 // newLitMapping returns a new litMapping with its state initialized based on
-// the provided slice of Variables. This includes construction of
-// the translation tables between Variables/Constraints and the
+// the provided slice of Entities. This includes construction of
+// the translation tables between Entities/Constraints and the
 // inputs to the underlying solver.
-func newLitMapping(variables []Variable) (*litMapping, error) {
+func newLitMapping(constraints []Constraint) (*litMapping, error) {
 	d := litMapping{
-		inorder:     variables,
-		variables:   make(map[z.Lit]Variable, len(variables)),
-		lits:        make(map[Identifier]z.Lit, len(variables)),
-		constraints: make(map[z.Lit]AppliedConstraint),
-		c:           logic.NewCCap(len(variables)),
-	}
-
-	// First pass to assign lits:
-	for _, variable := range variables {
-		im := d.c.Lit()
-		if _, ok := d.lits[variable.Identifier()]; ok {
-			return nil, DuplicateIdentifier(variable.Identifier())
-		}
-		d.lits[variable.Identifier()] = im
-		d.variables[im] = variable
-	}
-
-	for _, variable := range variables {
-		for _, constraint := range variable.Constraints() {
-			m := constraint.apply(d.c, &d, variable.Identifier())
-			if m == z.LitNull {
-				// This constraint doesn't have a
-				// useful representation in the SAT
-				// inputs.
-				continue
-			}
-
-			d.constraints[m] = AppliedConstraint{
-				Variable:   variable,
-				Constraint: constraint,
-			}
+		inorder:              make([]Constraint, len(constraints)),
+		constraintsByLiteral: make(map[z.Lit][]Constraint, 0),
+		lits:                 make(map[Identifier]z.Lit, 0),
+		constraints:          make(map[z.Lit]Constraint),
+		c:                    logic.NewC(),
+	}
+
+	for i, constraint := range constraints {
+		d.inorder[i] = constraints[i]
+
+		m := constraint.apply(d.c, &d)
+		if m == z.LitNull {
+			// This constraint doesn't have a
+			// useful representation in the SAT
+			// inputs.
+			continue
 		}
+
+		d.constraints[m] = constraint
+		litForVar := d.lits[constraint.Subject()]
+		d.constraintsByLiteral[litForVar] = append(d.constraintsByLiteral[litForVar], constraint)
 	}
 
 	return &d, nil
 }
 
-// LitOf returns the positive literal corresponding to the Variable
+// LitOf returns the positive literal corresponding to the *DeppyEntity
 // with the given Identifier.
 func (d *litMapping) LitOf(id Identifier) z.Lit {
-	m, ok := d.lits[id]
-	if ok {
-		return m
+	_, ok := d.lits[id]
+	if !ok {
+		d.lits[id] = d.c.Lit()
 	}
-	d.errs = append(d.errs, fmt.Errorf("variable %q referenced but not provided", id))
-	return z.LitNull
+	return d.lits[id]
 }
 
-// VariableOf returns the Variable corresponding to the provided
-// literal, or a zeroVariable if no such Variable exists.
-func (d *litMapping) VariableOf(m z.Lit) Variable {
-	i, ok := d.variables[m]
+func (d *litMapping) ConstraintsFor(m z.Lit) []Constraint {
+	constrs, ok := d.constraintsByLiteral[m]
 	if ok {
-		return i
+		return constrs
 	}
-	d.errs = append(d.errs, fmt.Errorf("no variable corresponding to %s", m))
-	return zeroVariable{}
+	return nil
 }
 
 // ConstraintOf returns the constraint application corresponding to
 // the provided literal, or a zeroConstraint if no such constraint
 // exists.
-func (d *litMapping) ConstraintOf(m z.Lit) AppliedConstraint {
+func (d *litMapping) ConstraintOf(m z.Lit) Constraint {
 	if a, ok := d.constraints[m]; ok {
 		return a
 	}
 	d.errs = append(d.errs, fmt.Errorf("no constraint corresponding to %s", m))
-	return AppliedConstraint{
-		Variable:   zeroVariable{},
-		Constraint: zeroConstraint{},
-	}
+	return ZeroConstraint
 }
 
 // Error returns a single error value that is an aggregation of all
@@ -134,8 +116,10 @@ func (d *litMapping) AddConstraints(g inter.S) {
 }
 
 func (d *litMapping) AssumeConstraints(s inter.S) {
-	for m := range d.constraints {
-		s.Assume(m)
+	for m, c := range d.constraints {
+		if !c.anchor() {
+			s.Assume(m)
+		}
 	}
 }
 
@@ -158,46 +142,33 @@ func (d *litMapping) CardinalityConstrainer(g inter.Adder, ms []z.Lit) *logic.Ca
 }
 
 // AnchorIdentifiers returns a slice containing the Identifiers of
-// every Variable with at least one "anchor" constraint, in the
+// every variable with at least one "anchor" constraint, in the
 // order they appear in the input.
 func (d *litMapping) AnchorIdentifiers() []Identifier {
 	var ids []Identifier
-	for _, variable := range d.inorder {
-		for _, constraint := range variable.Constraints() {
-			if constraint.anchor() {
-				ids = append(ids, variable.Identifier())
-				break
-			}
+	for _, c := range d.inorder {
+		if c.anchor() {
+			ids = append(ids, c.Subject())
 		}
 	}
-	return ids
-}
 
-func (d *litMapping) Variables(g inter.S) []Variable {
-	var result []Variable
-	for _, i := range d.inorder {
-		if g.Value(d.LitOf(i.Identifier())) {
-			result = append(result, i)
-		}
-	}
-	return result
+	return ids
 }
 
 func (d *litMapping) Lits(dst []z.Lit) []z.Lit {
-	if cap(dst) < len(d.inorder) {
-		dst = make([]z.Lit, 0, len(d.inorder))
+	if cap(dst) < len(d.lits) {
+		dst = make([]z.Lit, 0, len(d.lits))
 	}
 	dst = dst[:0]
-	for _, i := range d.inorder {
-		m := d.LitOf(i.Identifier())
-		dst = append(dst, m)
+	for _, lit := range d.lits {
+		dst = append(dst, lit)
 	}
 	return dst
 }
 
-func (d *litMapping) Conflicts(g inter.Assumable) []AppliedConstraint {
+func (d *litMapping) Conflicts(g inter.Assumable) []Constraint {
 	whys := g.Why(nil)
-	as := make([]AppliedConstraint, 0, len(whys))
+	as := make([]Constraint, 0, len(whys))
 	for _, why := range whys {
 		if a, ok := d.constraints[why]; ok {
 			as = append(as, a)
@@ -205,3 +176,22 @@ func (d *litMapping) Conflicts(g inter.Assumable) []AppliedConstraint {
 	}
 	return as
 }
+
+func (d *litMapping) Selection(g inter.S) []Identifier {
+	selection := make([]Identifier, 0)
+	for id, lit := range d.lits {
+		if g.Value(lit) {
+			selection = append(selection, id)
+		}
+	}
+	return selection
+}
+
+func (d *litMapping) IdentifierOf(lit z.Lit) Identifier {
+	for id, literal := range d.lits {
+		if literal == lit {
+			return id
+		}
+	}
+	return Identifier("nil")
+}
diff --git a/internal/solver/search.go b/internal/solver/search.go
index 523b311..88609c2 100644
--- a/internal/solver/search.go
+++ b/internal/solver/search.go
@@ -56,10 +56,10 @@ func (h *search) PushGuess() {
 		return
 	}
 
-	variable := h.lits.VariableOf(g.m)
-	for _, constraint := range variable.Constraints() {
+	constrs := h.lits.ConstraintsFor(g.m)
+	for _, constr := range constrs {
 		var ms []z.Lit
-		for _, dependency := range constraint.order() {
+		for _, dependency := range constr.order() {
 			ms = append(ms, h.lits.LitOf(dependency))
 		}
 		if len(ms) > 0 {
@@ -202,16 +202,16 @@ func (h *search) Do(ctx context.Context, anchors []z.Lit) (int, []z.Lit, map[z.L
 	return result, lits, set
 }
 
-func (h *search) Variables() []Variable {
-	result := make([]Variable, 0, len(h.guesses))
+func (h *search) Identifiers() []Identifier {
+	result := make([]Identifier, 0, len(h.guesses))
 	for _, g := range h.guesses {
 		if g.m != z.LitNull {
-			result = append(result, h.lits.VariableOf(g.candidates[g.index]))
+			result = append(result, h.lits.IdentifierOf(g.candidates[g.index]))
 		}
 	}
 	return result
 }
 
-func (h *search) Conflicts() []AppliedConstraint {
+func (h *search) Conflicts() []Constraint {
 	return h.lits.Conflicts(h.s)
 }
diff --git a/internal/solver/search_test.go b/internal/solver/search_test.go
index fd9221a..32d1461 100644
--- a/internal/solver/search_test.go
+++ b/internal/solver/search_test.go
@@ -31,7 +31,7 @@ func (c *TestScopeCounter) Untest() (result int) {
 func TestSearch(t *testing.T) {
 	type tc struct {
 		Name          string
-		Variables     []Variable
+		Constraints   []Constraint
 		TestReturns   []int
 		UntestReturns []int
 		Result        int
@@ -41,10 +41,10 @@ func TestSearch(t *testing.T) {
 	for _, tt := range []tc{
 		{
 			Name: "children popped from back of deque when guess popped",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("c")),
-				variable("b", Mandatory()),
-				variable("c"),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "c"),
+				Mandatory("b"),
 			},
 			TestReturns:   []int{0, -1},
 			UntestReturns: []int{-1, -1},
@@ -53,11 +53,11 @@ func TestSearch(t *testing.T) {
 		},
 		{
 			Name: "candidates exhausted",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("x")),
-				variable("b", Mandatory(), Dependency("y")),
-				variable("x"),
-				variable("y"),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "x"),
+				Mandatory("b"),
+				Dependency("b", "y"),
 			},
 			TestReturns:   []int{0, 0, -1, 1},
 			UntestReturns: []int{0},
@@ -79,7 +79,7 @@ func TestSearch(t *testing.T) {
 			var depth int
 			counter := &TestScopeCounter{depth: &depth, S: &s}
 
-			lits, err := newLitMapping(tt.Variables)
+			lits, err := newLitMapping(tt.Constraints)
 			assert.NoError(err)
 			h := search{
 				s:      counter,
@@ -97,7 +97,7 @@ func TestSearch(t *testing.T) {
 			assert.Equal(tt.Result, result)
 			var ids []Identifier
 			for _, m := range ms {
-				ids = append(ids, lits.VariableOf(m).Identifier())
+				ids = append(ids, lits.IdentifierOf(m))
 			}
 			assert.Equal(tt.Assumptions, ids)
 			assert.Equal(0, depth)
diff --git a/internal/solver/solve.go b/internal/solver/solve.go
index 766fa60..acf79b1 100644
--- a/internal/solver/solve.go
+++ b/internal/solver/solve.go
@@ -4,6 +4,7 @@ import (
 	"context"
 	"errors"
 	"fmt"
+	"sort"
 	"strings"
 
 	"github.com/go-air/gini"
@@ -15,7 +16,7 @@ var ErrIncomplete = errors.New("cancelled before a solution could be found")
 
 // NotSatisfiable is an error composed of a minimal set of applied
 // constraints that is sufficient to make a solution impossible.
-type NotSatisfiable []AppliedConstraint
+type NotSatisfiable []Constraint
 
 func (e NotSatisfiable) Error() string {
 	const msg = "constraints not satisfiable"
@@ -26,11 +27,12 @@ func (e NotSatisfiable) Error() string {
 	for i, a := range e {
 		s[i] = a.String()
 	}
+	sort.Strings(s)
 	return fmt.Sprintf("%s: %s", msg, strings.Join(s, ", "))
 }
 
 type Solver interface {
-	Solve(context.Context) ([]Variable, error)
+	Solve(context.Context) ([]Identifier, error)
 }
 
 type solver struct {
@@ -46,11 +48,11 @@ const (
 	unknown       = 0
 )
 
-// Solve takes a slice containing all Variables and returns a slice
-// containing only those Variables that were selected for
+// Solve takes a slice containing all Entities and returns a slice
+// containing only those Entities that were selected for
 // installation. If no solution is possible, or if the provided
 // Context times out or is cancelled, an error is returned.
-func (s *solver) Solve(ctx context.Context) (result []Variable, err error) {
+func (s *solver) Solve(ctx context.Context) (result []Identifier, err error) {
 	defer func() {
 		// This likely indicates a bug, so discard whatever
 		// return values were produced.
@@ -64,7 +66,7 @@ func (s *solver) Solve(ctx context.Context) (result []Variable, err error) {
 	s.litMap.AddConstraints(s.g)
 
 	// collect literals of all mandatory variables to assume as a baseline
-	assumptions := []z.Lit{}
+	var assumptions []z.Lit
 	for _, anchor := range s.litMap.AnchorIdentifiers() {
 		assumptions = append(assumptions, s.litMap.LitOf(anchor))
 	}
@@ -104,7 +106,7 @@ func (s *solver) Solve(ctx context.Context) (result []Variable, err error) {
 		for w := 0; w <= cs.N(); w++ {
 			s.g.Assume(cs.Leq(w))
 			if s.g.Solve() == satisfiable {
-				return s.litMap.Variables(s.g), nil
+				return s.litMap.Selection(s.g), nil
 			}
 		}
 		// Something is wrong if we can't find a model anymore
@@ -129,10 +131,10 @@ func New(options ...Option) (Solver, error) {
 
 type Option func(s *solver) error
 
-func WithInput(input []Variable) Option {
+func WithInput(constraints []Constraint) Option {
 	return func(s *solver) error {
 		var err error
-		s.litMap, err = newLitMapping(input)
+		s.litMap, err = newLitMapping(constraints)
 		return err
 	}
 }
diff --git a/internal/solver/solve_test.go b/internal/solver/solve_test.go
index d9ec36a..afb9d82 100644
--- a/internal/solver/solve_test.go
+++ b/internal/solver/solve_test.go
@@ -3,9 +3,7 @@ package solver
 import (
 	"bytes"
 	"context"
-	"errors"
 	"fmt"
-	"reflect"
 	"sort"
 	"testing"
 
@@ -56,28 +54,19 @@ func TestNotSatisfiableError(t *testing.T) {
 		{
 			Name: "single failure",
 			Error: NotSatisfiable{
-				AppliedConstraint{
-					Variable:   variable("a", Mandatory()),
-					Constraint: Mandatory(),
-				},
+				Mandatory("a"),
 			},
 			String: fmt.Sprintf("constraints not satisfiable: %s",
-				Mandatory().String("a")),
+				Mandatory("a").String()),
 		},
 		{
 			Name: "multiple failures",
 			Error: NotSatisfiable{
-				AppliedConstraint{
-					Variable:   variable("a", Mandatory()),
-					Constraint: Mandatory(),
-				},
-				AppliedConstraint{
-					Variable:   variable("b", Prohibited()),
-					Constraint: Prohibited(),
-				},
+				Mandatory("a"),
+				Prohibited("b"),
 			},
 			String: fmt.Sprintf("constraints not satisfiable: %s, %s",
-				Mandatory().String("a"), Prohibited().String("b")),
+				Mandatory("a").String(), Prohibited("b").String()),
 		},
 	} {
 		t.Run(tt.Name, func(t *testing.T) {
@@ -88,210 +77,184 @@ func TestNotSatisfiableError(t *testing.T) {
 
 func TestSolve(t *testing.T) {
 	type tc struct {
-		Name      string
-		Variables []Variable
-		Installed []Identifier
-		Error     error
+		Name        string
+		Constraints []Constraint
+		Installed   []Identifier
+		Error       error
 	}
 
 	for _, tt := range []tc{
 		{
-			Name: "no variables",
+			Name:      "no variables",
+			Installed: []Identifier{},
 		},
 		{
-			Name:      "unnecessary variable is not installed",
-			Variables: []Variable{variable("a")},
+			Name:        "single mandatory variable is installed",
+			Constraints: []Constraint{Mandatory("a")},
+			Installed:   []Identifier{"a"},
 		},
 		{
-			Name:      "single mandatory variable is installed",
-			Variables: []Variable{variable("a", Mandatory())},
-			Installed: []Identifier{"a"},
-		},
-		{
-			Name:      "both mandatory and prohibited produce error",
-			Variables: []Variable{variable("a", Mandatory(), Prohibited())},
+			Name:        "both mandatory and prohibited produce error",
+			Constraints: []Constraint{Mandatory("a"), Prohibited("a")},
 			Error: NotSatisfiable{
-				{
-					Variable:   variable("a", Mandatory(), Prohibited()),
-					Constraint: Mandatory(),
-				},
-				{
-					Variable:   variable("a", Mandatory(), Prohibited()),
-					Constraint: Prohibited(),
-				},
+				Mandatory("a"),
+				Prohibited("a"),
 			},
 		},
 		{
 			Name: "dependency is installed",
-			Variables: []Variable{
-				variable("a"),
-				variable("b", Mandatory(), Dependency("a")),
+			Constraints: []Constraint{
+				Mandatory("b"),
+				Dependency("b", "a"),
 			},
 			Installed: []Identifier{"a", "b"},
 		},
 		{
 			Name: "transitive dependency is installed",
-			Variables: []Variable{
-				variable("a"),
-				variable("b", Dependency("a")),
-				variable("c", Mandatory(), Dependency("b")),
+			Constraints: []Constraint{
+				Dependency("b", "a"),
+				Mandatory("c"),
+				Dependency("c", "b"),
 			},
 			Installed: []Identifier{"a", "b", "c"},
 		},
 		{
 			Name: "both dependencies are installed",
-			Variables: []Variable{
-				variable("a"),
-				variable("b"),
-				variable("c", Mandatory(), Dependency("a"), Dependency("b")),
+			Constraints: []Constraint{
+				Mandatory("c"),
+				Dependency("c", "a"),
+				Dependency("c", "b"),
 			},
 			Installed: []Identifier{"a", "b", "c"},
 		},
 		{
 			Name: "solution with first dependency is selected",
-			Variables: []Variable{
-				variable("a"),
-				variable("b", Conflict("a")),
-				variable("c", Mandatory(), Dependency("a", "b")),
+			Constraints: []Constraint{
+				Conflict("b", "a"),
+				Mandatory("c"),
+				Dependency("c", "a", "b"),
 			},
 			Installed: []Identifier{"a", "c"},
 		},
 		{
 			Name: "solution with only first dependency is selected",
-			Variables: []Variable{
-				variable("a"),
-				variable("b"),
-				variable("c", Mandatory(), Dependency("a", "b")),
+			Constraints: []Constraint{
+				Mandatory("c"),
+				Dependency("c", "a", "b"),
 			},
 			Installed: []Identifier{"a", "c"},
 		},
 		{
 			Name: "solution with first dependency is selected (reverse)",
-			Variables: []Variable{
-				variable("a"),
-				variable("b", Conflict("a")),
-				variable("c", Mandatory(), Dependency("b", "a")),
+			Constraints: []Constraint{
+				Conflict("b", "a"),
+				Mandatory("c"),
+				Dependency("c", "b", "a"),
 			},
 			Installed: []Identifier{"b", "c"},
 		},
 		{
 			Name: "two mandatory but conflicting packages",
-			Variables: []Variable{
-				variable("a", Mandatory()),
-				variable("b", Mandatory(), Conflict("a")),
+			Constraints: []Constraint{
+				Mandatory("b"),
+				Mandatory("a"),
+				Conflict("b", "a"),
 			},
 			Error: NotSatisfiable{
-				{
-					Variable:   variable("a", Mandatory()),
-					Constraint: Mandatory(),
-				},
-				{
-					Variable:   variable("b", Mandatory(), Conflict("a")),
-					Constraint: Mandatory(),
-				},
-				{
-					Variable:   variable("b", Mandatory(), Conflict("a")),
-					Constraint: Conflict("a"),
-				},
+				Mandatory("a"),
+				Mandatory("b"),
+				Conflict("b", "a"),
 			},
 		},
 		{
 			Name: "irrelevant dependencies don't influence search order",
-			Variables: []Variable{
-				variable("a", Dependency("x", "y")),
-				variable("b", Mandatory(), Dependency("y", "x")),
-				variable("x"),
-				variable("y"),
+			Constraints: []Constraint{
+				Dependency("a", "x", "y"),
+				Mandatory("b"),
+				Dependency("b", "y", "x"),
 			},
 			Installed: []Identifier{"b", "y"},
 		},
 		{
 			Name: "cardinality constraint prevents resolution",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")),
-				variable("x", Mandatory()),
-				variable("y", Mandatory()),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "x", "y"),
+				Mandatory("x"),
+				Mandatory("y"),
+				AtMost("a", 1, "x", "y"),
 			},
 			Error: NotSatisfiable{
-				{
-					Variable:   variable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")),
-					Constraint: AtMost(1, "x", "y"),
-				},
-				{
-					Variable:   variable("x", Mandatory()),
-					Constraint: Mandatory(),
-				},
-				{
-					Variable:   variable("y", Mandatory()),
-					Constraint: Mandatory(),
-				},
+				Mandatory("y"),
+				Mandatory("x"),
+				AtMost("a", 1, "x", "y"),
 			},
 		},
 		{
 			Name: "cardinality constraint forces alternative",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")),
-				variable("b", Mandatory(), Dependency("y")),
-				variable("x"),
-				variable("y"),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "x", "y"),
+				AtMost("a", 1, "x", "y"),
+				Mandatory("b"),
+				Dependency("b", "y"),
 			},
 			Installed: []Identifier{"a", "b", "y"},
 		},
 		{
 			Name: "two dependencies satisfied by one variable",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("y")),
-				variable("b", Mandatory(), Dependency("x", "y")),
-				variable("x"),
-				variable("y"),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "y"),
+				Mandatory("b"),
+				Dependency("b", "x", "y"),
 			},
 			Installed: []Identifier{"a", "b", "y"},
 		},
 		{
 			Name: "foo two dependencies satisfied by one variable",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("y", "z", "m")),
-				variable("b", Mandatory(), Dependency("x", "y")),
-				variable("x"),
-				variable("y"),
-				variable("z"),
-				variable("m"),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "y", "z", "m"),
+				Mandatory("b"),
+				Dependency("b", "x", "y"),
 			},
 			Installed: []Identifier{"a", "b", "y"},
 		},
 		{
 			Name: "result size larger than minimum due to preference",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("x", "y")),
-				variable("b", Mandatory(), Dependency("y")),
-				variable("x"),
-				variable("y"),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "x", "y"),
+				Mandatory("b"),
+				Dependency("b", "y"),
 			},
 			Installed: []Identifier{"a", "b", "x", "y"},
 		},
 		{
 			Name: "only the least preferable choice is acceptable",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("a1", "a2")),
-				variable("a1", Conflict("c1"), Conflict("c2")),
-				variable("a2", Conflict("c1")),
-				variable("b", Mandatory(), Dependency("b1", "b2")),
-				variable("b1", Conflict("c1"), Conflict("c2")),
-				variable("b2", Conflict("c1")),
-				variable("c", Mandatory(), Dependency("c1", "c2")),
-				variable("c1"),
-				variable("c2"),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "a1", "a2"),
+				Conflict("a1", "c1"),
+				Conflict("a1", "c2"),
+				Conflict("a2", "c1"),
+				Mandatory("b"),
+				Dependency("b", "b1", "b2"),
+				Conflict("b1", "c1"),
+				Conflict("b1", "c2"),
+				Conflict("b2", "c1"),
+				Mandatory("c"),
+				Dependency("c", "c1", "c2"),
 			},
 			Installed: []Identifier{"a", "a2", "b", "b2", "c", "c2"},
 		},
 		{
 			Name: "preferences respected with multiple dependencies per variable",
-			Variables: []Variable{
-				variable("a", Mandatory(), Dependency("x1", "x2"), Dependency("y1", "y2")),
-				variable("x1"),
-				variable("x2"),
-				variable("y1"),
-				variable("y2"),
+			Constraints: []Constraint{
+				Mandatory("a"),
+				Dependency("a", "x1", "x2"),
+				Dependency("a", "y1", "y2"),
 			},
 			Installed: []Identifier{"a", "x1", "y1"},
 		},
@@ -300,7 +263,7 @@ func TestSolve(t *testing.T) {
 			assert := assert.New(t)
 
 			var traces bytes.Buffer
-			s, err := New(WithInput(tt.Variables), WithTracer(LoggingTracer{Writer: &traces}))
+			s, err := New(WithInput(tt.Constraints), WithTracer(LoggingTracer{Writer: &traces}))
 			if err != nil {
 				t.Fatalf("failed to initialize solver: %s", err)
 			}
@@ -309,44 +272,11 @@ func TestSolve(t *testing.T) {
 
 			if installed != nil {
 				sort.SliceStable(installed, func(i, j int) bool {
-					return installed[i].Identifier() < installed[j].Identifier()
-				})
-			}
-
-			// Failed constraints are sorted in lexically
-			// increasing order of the identifier of the
-			// constraint's variable, with ties broken
-			// in favor of the constraint that appears
-			// earliest in the variable's list of
-			// constraints.
-			var ns NotSatisfiable
-			if errors.As(err, &ns) {
-				sort.SliceStable(ns, func(i, j int) bool {
-					if ns[i].Variable.Identifier() != ns[j].Variable.Identifier() {
-						return ns[i].Variable.Identifier() < ns[j].Variable.Identifier()
-					}
-					var x, y int
-					for ii, c := range ns[i].Variable.Constraints() {
-						if reflect.DeepEqual(c, ns[i].Constraint) {
-							x = ii
-							break
-						}
-					}
-					for ij, c := range ns[j].Variable.Constraints() {
-						if reflect.DeepEqual(c, ns[j].Constraint) {
-							y = ij
-							break
-						}
-					}
-					return x < y
+					return installed[i] < installed[j]
 				})
 			}
 
-			var ids []Identifier
-			for _, variable := range installed {
-				ids = append(ids, variable.Identifier())
-			}
-			assert.Equal(tt.Installed, ids)
+			assert.Equal(tt.Installed, installed)
 			assert.Equal(tt.Error, err)
 
 			if t.Failed() {
@@ -355,11 +285,3 @@ func TestSolve(t *testing.T) {
 		})
 	}
 }
-
-func TestDuplicateIdentifier(t *testing.T) {
-	_, err := New(WithInput([]Variable{
-		variable("a"),
-		variable("a"),
-	}))
-	assert.Equal(t, DuplicateIdentifier("a"), err)
-}
diff --git a/internal/solver/tracer.go b/internal/solver/tracer.go
index b103536..c876df2 100644
--- a/internal/solver/tracer.go
+++ b/internal/solver/tracer.go
@@ -6,8 +6,8 @@ import (
 )
 
 type SearchPosition interface {
-	Variables() []Variable
-	Conflicts() []AppliedConstraint
+	Identifiers() []Identifier
+	Conflicts() []Constraint
 }
 
 type Tracer interface {
@@ -25,10 +25,10 @@ type LoggingTracer struct {
 
 func (t LoggingTracer) Trace(p SearchPosition) {
 	fmt.Fprintf(t.Writer, "---\nAssumptions:\n")
-	for _, i := range p.Variables() {
-		fmt.Fprintf(t.Writer, "- %s\n", i.Identifier())
+	for _, i := range p.Identifiers() {
+		fmt.Fprintf(t.Writer, "- %s\n", i)
 	}
-	fmt.Fprintf(t.Writer, "Conflicts:\n")
+	fmt.Fprintf(t.Writer, "Conflict:\n")
 	for _, a := range p.Conflicts() {
 		fmt.Fprintf(t.Writer, "- %s\n", a)
 	}
diff --git a/internal/solver/variable.go b/internal/solver/variable.go
index 32afab7..c98f0e1 100644
--- a/internal/solver/variable.go
+++ b/internal/solver/variable.go
@@ -1,6 +1,6 @@
 package solver
 
-// Identifier values uniquely identify particular Variables within
+// Identifier values uniquely identify particular Identifiers within
 // the input to a single call to Solve.
 type Identifier string
 
@@ -18,7 +18,7 @@ func IdentifierFromString(s string) Identifier {
 // understood by this package.
 type Variable interface {
 	// Identifier returns the Identifier that uniquely identifies
-	// this Variable among all other Variables in a given
+	// this Variable among all other Identifiers in a given
 	// problem.
 	Identifier() Identifier
 	// Constraints returns the set of constraints that apply to