diff --git a/manual/src/lib/basic.md b/manual/src/lib/basic.md
index 457f6996..a8ad743e 100644
--- a/manual/src/lib/basic.md
+++ b/manual/src/lib/basic.md
@@ -11,29 +11,30 @@ let mut solver = Solver::new();
 
 ## Loading a Formula
 
-We can load a formula by adding individual clauses:
+The solver also implements the `ExtendFormula` trait, so we already know how to
+add clauses from the previous chapter.
 
 ```rust
 # extern crate varisat;
 # use varisat::Solver;
 # let mut solver = Solver::new();
-use varisat::Lit;
+use varisat::ExtendFormula;
 
-let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
+let (x, y, z) = solver.new_lits();
 
 solver.add_clause(&[x, y, z]);
 solver.add_clause(&[!x, !y]);
 solver.add_clause(&[!y, !z]);
 ```
 
-By adding a formula:
+We can also load a `CnfFormula` with a single call of the `add_formula` method.
 
 ```rust
 # extern crate varisat;
-# use varisat::{Lit, Solver};
+# use varisat::Solver;
 # let mut solver = Solver::new();
-# let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
-use varisat::CnfFormula;
+# let (x, y, z) = solver.new_lits();
+use varisat::{CnfFormula, ExtendFormula};
 let mut formula = CnfFormula::new();
 formula.add_clause(&[x, y, z]);
 formula.add_clause(&[!x, !y]);
@@ -42,9 +43,10 @@ formula.add_clause(&[!y, !z]);
 solver.add_formula(&formula);
 ```
 
-Or by directly loading a [DIMACS CNF][dimacs] from anything that implements
-`std::io::Read`. This uses incremental parsing, making it more efficient than
-reading the whole formula into a `CnfFormula`.
+If our formula is stored as [DIMACS CNF][dimacs] in a file, or in another way
+that supports `std::io::Read`, we can load it into the solver with
+`add_dimacs_cnf`. This uses incremental parsing, making it more efficient than
+reading the whole formula into a `CnfFormula` first.
 
 ```rust
 # extern crate varisat;
@@ -79,10 +81,9 @@ query the solver for a set of assignments that make all clauses true.
 
 ```rust
 # extern crate varisat;
-# use varisat::Solver;
-# use varisat::Lit;
+# use varisat::{Solver, ExtendFormula};
 # let mut solver = Solver::new();
-# let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
+# let (x, y, z) = solver.new_lits();
 # let dimacs_cnf = b"1 2 3 0\n-1 -2 0\n-2 -3 0\n";
 # solver.add_dimacs_cnf(&dimacs_cnf[..]).expect("parse error");
 # let solution = solver.solve().unwrap();
diff --git a/manual/src/lib/formulas.md b/manual/src/lib/formulas.md
index f0b9d2e5..9dc365bd 100644
--- a/manual/src/lib/formulas.md
+++ b/manual/src/lib/formulas.md
@@ -41,10 +41,13 @@ assert_eq!(x.to_dimacs(), 1);
 assert!(Lit::from_dimacs(2).is_positive());
 assert!(Lit::from_dimacs(-3).is_negative());
 
-assert_eq!(Lit::positive(x), Lit::from_var(x, true));
-assert_eq!(Lit::negative(x), Lit::from_var(x, false));
+assert_eq!(Lit::positive(x), x.lit(true));
+assert_eq!(Lit::negative(x), x.lit(false));
 
-assert_eq!(Lit::negative(x), !Lit::positive(x));
+assert_eq!(x.positive(), Lit::from_var(x, true));
+assert_eq!(x.negative(), Lit::from_var(x, false));
+
+assert_eq!(x.positive(), !x.negative());
 
 assert_eq!(Lit::from_index(6, true).code(), 12);
 assert_eq!(Lit::from_index(6, false).code(), 13);
@@ -81,10 +84,13 @@ Instead Varisat provides the `CnfFormula` type, which stores all literals in a
 single `Vec`. When iterating over a `CnfFormula` the clauses can be accessed as
 slices.
 
+The `add_clause` method of the `ExtendFormula` trait allows adding new clauses
+to a `CnfFormula`.
+
 ```rust
 # extern crate varisat;
 # use varisat::{Var, Lit};
-use varisat::CnfFormula;
+use varisat::{CnfFormula, ExtendFormula};
 
 let mut formula = CnfFormula::new();
 
@@ -98,6 +104,29 @@ formula.add_clause(&[!a, !c]);
 assert_eq!(formula.iter().last().unwrap(), &[!a, !c]);
 ```
 
+## New Variables and Literals
+
+Often we don't care about the specific indices of variables. In that case,
+instead of manually computing indices, we can dynamically ask for new unused
+variables. This functionality is also also provided by the `ExtendFormula`
+trait.
+
+```rust
+# extern crate varisat;
+# use varisat::{CnfFormula, ExtendFormula, Lit, Var};
+let mut formula = CnfFormula::new();
+
+let a = formula.new_var().negative();
+let b = formula.new_lit();
+let (c, d, e) = formula.new_lits();
+let f: Vec<Lit> = formula.new_lit_iter(10).collect();
+
+formula.add_clause(&[a, b, c, d, e]);
+formula.add_clause(&f);
+
+assert_eq!(formula.var_count(), 15);
+```
+
 ## Parsing and Writing Formulas
 
 Varisat provides routines for parsing and writing Formulas in the [DIMACS
@@ -106,6 +135,7 @@ CNF][dimacs] format.
 ```rust
 # extern crate varisat;
 # use varisat::{Var, Lit};
+# use varisat::ExtendFormula;
 use varisat::dimacs::{DimacsParser, write_dimacs};
 
 let input = b"p cnf 3 2\n1 2 3 0\n-1 -3 0\n";
diff --git a/manual/src/lib/incremental.md b/manual/src/lib/incremental.md
index c615f442..7df14396 100644
--- a/manual/src/lib/incremental.md
+++ b/manual/src/lib/incremental.md
@@ -16,11 +16,12 @@ clauses that were already present prior to the last `solve` call.
 
 ```rust
 # extern crate varisat;
-use varisat::{Lit, Solver};
-
-let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
+use varisat::{ExtendFormula, Solver};
 
 let mut solver = Solver::new();
+
+let (x, y, z) = solver.new_lits();
+
 solver.add_clause(&[!x, y]);
 solver.add_clause(&[!y, z]);
 assert_eq!(solver.solve().unwrap(), true);
@@ -49,12 +50,13 @@ clauses:
 
 ```rust
 # extern crate varisat;
-use varisat::{Lit, Solver};
-
-let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
-let ignore_clauses = Lit::from_dimacs(4);
+use varisat::{ExtendFormula, Solver};
 
 let mut solver = Solver::new();
+
+let (x, y, z) = solver.new_lits();
+let ignore_clauses = solver.new_lit();
+
 solver.add_clause(&[!x, y]);
 solver.add_clause(&[!y, z]);
 assert_eq!(solver.solve().unwrap(), true);
diff --git a/varisat-dimacs/src/lib.rs b/varisat-dimacs/src/lib.rs
index 053fd121..7ac70937 100644
--- a/varisat-dimacs/src/lib.rs
+++ b/varisat-dimacs/src/lib.rs
@@ -4,7 +4,7 @@ use std::borrow::Borrow;
 use std::io;
 use std::mem::replace;
 
-use varisat_formula::{CnfFormula, Lit, Var};
+use varisat_formula::{CnfFormula, ExtendFormula, Lit, Var};
 
 use failure::{Error, Fail};
 
@@ -309,10 +309,8 @@ impl DimacsParser {
                 self.partial_clause.clear();
                 self.clause_count += 1;
             } else {
-                self.partial_clause.push(Lit::from_var(
-                    Var::from_dimacs(self.partial_lit as isize),
-                    !self.negate_next_lit,
-                ));
+                self.partial_clause
+                    .push(Var::from_dimacs(self.partial_lit as isize).lit(!self.negate_next_lit));
             }
         }
     }
diff --git a/varisat-formula/src/cnf.rs b/varisat-formula/src/cnf.rs
index c9e76a37..1f485ee4 100644
--- a/varisat-formula/src/cnf.rs
+++ b/varisat-formula/src/cnf.rs
@@ -1,10 +1,9 @@
 //! CNF formulas.
 use std::cmp::max;
 use std::fmt;
-use std::iter::Extend;
 use std::ops::Range;
 
-use crate::lit::Lit;
+use crate::lit::{Lit, Var};
 
 /// A formula in conjunctive normal form (CNF).
 ///
@@ -42,24 +41,6 @@ impl CnfFormula {
         self.clause_ranges.len()
     }
 
-    /// Appends a clause to the formula.
-    ///
-    /// `literals` can be an `IntoIterator<Item = Lit>` or `IntoIterator<Item = &Lit>`.
-    pub fn add_clause<L>(&mut self, literals: impl IntoIterator<Item = L>)
-    where
-        Vec<Lit>: Extend<L>,
-    {
-        let begin = self.literals.len();
-        self.literals.extend(literals);
-        let end = self.literals.len();
-
-        for &lit in self.literals[begin..end].iter() {
-            self.var_count = max(lit.index() + 1, self.var_count);
-        }
-
-        self.clause_ranges.push(begin..end);
-    }
-
     /// Iterator over all clauses.
     pub fn iter(&self) -> impl Iterator<Item = &[Lit]> {
         let literals = &self.literals;
@@ -69,17 +50,16 @@ impl CnfFormula {
     }
 }
 
-/// Convert any iterable of [`Lit`] iterables into a CnfFormula
-impl<F, I, L> From<F> for CnfFormula
+/// Convert an iterable of [`Lit`] slices into a CnfFormula
+impl<Clauses, Item> From<Clauses> for CnfFormula
 where
-    F: IntoIterator<Item = I>,
-    I: IntoIterator<Item = L>,
-    Vec<Lit>: Extend<L>,
+    Clauses: IntoIterator<Item = Item>,
+    Item: std::borrow::Borrow<[Lit]>,
 {
-    fn from(formula: F) -> CnfFormula {
+    fn from(clauses: Clauses) -> CnfFormula {
         let mut cnf_formula = CnfFormula::new();
-        for clause in formula {
-            cnf_formula.add_clause(clause);
+        for clause in clauses {
+            cnf_formula.add_clause(clause.borrow());
         }
         cnf_formula
     }
@@ -106,6 +86,142 @@ impl PartialEq for CnfFormula {
     }
 }
 
+/// Extend a formula with new variables and clauses.
+pub trait ExtendFormula: Sized {
+    /// Appends a clause to the formula.
+    ///
+    /// `literals` can be an `IntoIterator<Item = Lit>` or `IntoIterator<Item = &Lit>`.
+    fn add_clause(&mut self, literals: &[Lit]);
+
+    /// Add a new variable to the formula and return it.
+    fn new_var(&mut self) -> Var;
+
+    /// Add a new variable to the formula and return it as positive literal.
+    fn new_lit(&mut self) -> Lit {
+        self.new_var().positive()
+    }
+
+    /// Iterator over multiple new variables.
+    fn new_var_iter(&mut self, count: usize) -> NewVarIter<Self> {
+        NewVarIter {
+            formula: self,
+            vars_left: count,
+            phantom: std::marker::PhantomData,
+        }
+    }
+
+    /// Iterator over multiple new literals.
+    fn new_lit_iter(&mut self, count: usize) -> NewVarIter<Self, Lit> {
+        NewVarIter {
+            formula: self,
+            vars_left: count,
+            phantom: std::marker::PhantomData,
+        }
+    }
+
+    /// Add multiple new variables and return them.
+    ///
+    /// Returns a uniform tuple of variables. The number of variables is inferred, so it can be used
+    /// like `let (x, y, z) = formula.new_vars()`.
+    fn new_vars<Vars: UniformTuple<Var>>(&mut self) -> Vars {
+        Vars::tuple_from_iter(self.new_var_iter(Vars::tuple_len()))
+    }
+
+    /// Add multiple new variables and return them as positive literals.
+    ///
+    /// Returns a uniform tuple of variables. The number of variables is inferred, so it can be used
+    /// like `let (x, y, z) = formula.new_lits()`.
+    fn new_lits<Lits: UniformTuple<Lit>>(&mut self) -> Lits {
+        Lits::tuple_from_iter(self.new_lit_iter(Lits::tuple_len()))
+    }
+}
+
+/// Iterator over new variables or literals.
+///
+/// Created by the [`new_var_iter`][ExtendFormula::new_var_iter] and
+/// [`new_lit_iter`][ExtendFormula::new_lit_iter] methods of [`ExtendFormula`].
+pub struct NewVarIter<'a, F, V = Var> {
+    formula: &'a mut F,
+    vars_left: usize,
+    phantom: std::marker::PhantomData<V>,
+}
+
+impl<'a, F, V> Iterator for NewVarIter<'a, F, V>
+where
+    F: ExtendFormula,
+    V: From<Var>,
+{
+    type Item = V;
+
+    fn next(&mut self) -> Option<V> {
+        if self.vars_left == 0 {
+            None
+        } else {
+            let var = self.formula.new_var();
+            self.vars_left -= 1;
+            Some(V::from(var))
+        }
+    }
+}
+
+impl ExtendFormula for CnfFormula {
+    fn add_clause(&mut self, clause: &[Lit]) {
+        let begin = self.literals.len();
+        self.literals.extend_from_slice(clause);
+        let end = self.literals.len();
+
+        for &lit in self.literals[begin..end].iter() {
+            self.var_count = max(lit.index() + 1, self.var_count);
+        }
+
+        self.clause_ranges.push(begin..end);
+    }
+
+    fn new_var(&mut self) -> Var {
+        let var = Var::from_index(self.var_count);
+        self.var_count += 1;
+        var
+    }
+}
+
+/// Helper trait to initialize multiple variables of the same type.
+pub trait UniformTuple<Item> {
+    fn tuple_len() -> usize;
+    fn tuple_from_iter(items: impl Iterator<Item = Item>) -> Self;
+}
+
+macro_rules! ignore_first {
+    ($a:tt, $b:tt) => {
+        $b
+    };
+}
+
+macro_rules! array_like_impl {
+    ($count:expr, $($call:tt)*) => {
+        impl<Item> UniformTuple<Item> for ($(ignore_first!($call, Item)),*) {
+            fn tuple_len() -> usize { $count }
+            fn tuple_from_iter(mut items: impl Iterator<Item = Item>) -> Self {
+                ($(items.next().unwrap().into $call),*)
+            }
+        }
+    }
+}
+
+macro_rules! array_like_impl_4 {
+    ($count:expr, $($call:tt)*) => {
+        array_like_impl!($count * 4 + 2, $(()()()$call)* ()());
+        array_like_impl!($count * 4 + 3, $(()()()$call)* ()()());
+        array_like_impl!($count * 4 + 4, $(()()()$call)* ()()()());
+        array_like_impl!($count * 4 + 5, $(()()()$call)* ()()()()());
+    }
+}
+
+array_like_impl_4!(0,);
+array_like_impl_4!(1, ());
+array_like_impl_4!(2, ()());
+array_like_impl_4!(3, ()()());
+array_like_impl_4!(4, ()()()());
+
 #[cfg(any(test, feature = "proptest-strategies"))]
 #[doc(hidden)]
 pub mod strategy {
@@ -170,6 +286,17 @@ mod tests {
 
     use proptest::*;
 
+    #[test]
+    fn new_vars() {
+        let mut formula = CnfFormula::new();
+        let (x, y, z) = formula.new_vars();
+
+        assert_ne!(x, y);
+        assert_ne!(y, z);
+        assert_ne!(x, y);
+        assert_eq!(formula.var_count(), 3);
+    }
+
     #[test]
     fn simple_roundtrip() {
         let input = cnf![
@@ -192,7 +319,7 @@ mod tests {
     proptest! {
         #[test]
         fn roundtrip_from_vec(input in vec_formula(1..200usize, 0..1000, 0..10)) {
-            let formula = CnfFormula::from(input.iter().map(|clause| clause.iter().cloned()));
+            let formula = CnfFormula::from(input.clone());
 
             for (clause, ref_clause) in formula.iter().zip(input.iter()) {
                 prop_assert_eq!(clause, &ref_clause[..]);
diff --git a/varisat-formula/src/lib.rs b/varisat-formula/src/lib.rs
index b0f94139..5e51502a 100644
--- a/varisat-formula/src/lib.rs
+++ b/varisat-formula/src/lib.rs
@@ -60,5 +60,5 @@ pub mod lit;
 #[cfg(any(test, feature = "internal-testing"))]
 pub mod test;
 
-pub use cnf::CnfFormula;
+pub use cnf::{CnfFormula, ExtendFormula};
 pub use lit::{Lit, Var};
diff --git a/varisat-formula/src/lit.rs b/varisat-formula/src/lit.rs
index 9ca6fe26..2d011cbc 100644
--- a/varisat-formula/src/lit.rs
+++ b/varisat-formula/src/lit.rs
@@ -64,6 +64,27 @@ impl Var {
     pub const fn max_count() -> usize {
         Self::max_var().index() + 1
     }
+
+    /// Creates a literal from this var and a `bool` that is `true` when the literal is positive.
+    ///
+    /// Shortcut for `Lit::from_var(var, polarity)`.
+    pub fn lit(self, polarity: bool) -> Lit {
+        Lit::from_var(self, polarity)
+    }
+
+    /// Creates a positive literal from this var.
+    ///
+    /// Shortcut for `Lit::positive(var)`.
+    pub fn positive(self) -> Lit {
+        Lit::positive(self)
+    }
+
+    /// Creates a negative literal from this var.
+    ///
+    /// Shortcut for `Lit::negative(var)`.
+    pub fn negative(self) -> Lit {
+        Lit::negative(self)
+    }
 }
 
 /// Uses the 1-based DIMACS CNF encoding.
@@ -201,6 +222,12 @@ impl ops::BitXor<bool> for Lit {
     }
 }
 
+impl From<Var> for Lit {
+    fn from(var: Var) -> Lit {
+        Lit::positive(var)
+    }
+}
+
 /// Uses the 1-based DIMACS CNF encoding.
 impl fmt::Debug for Lit {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
@@ -226,6 +253,6 @@ pub mod strategy {
     }
 
     pub fn lit(index: impl Strategy<Value = usize>) -> impl Strategy<Value = Lit> {
-        (var(index), bool::ANY).prop_map(|(var, polarity)| Lit::from_var(var, polarity))
+        (var(index), bool::ANY).prop_map(|(var, polarity)| var.lit(polarity))
     }
 }
diff --git a/varisat/src/clause/alloc.rs b/varisat/src/clause/alloc.rs
index 0a02b39b..c7e0f494 100644
--- a/varisat/src/clause/alloc.rs
+++ b/varisat/src/clause/alloc.rs
@@ -195,7 +195,7 @@ impl ClauseRef {
 mod tests {
     use super::*;
 
-    use varisat_formula::{cnf::strategy::*, CnfFormula};
+    use varisat_formula::{cnf::strategy::*, CnfFormula, ExtendFormula};
 
     use proptest::*;
 
diff --git a/varisat/src/decision.rs b/varisat/src/decision.rs
index 896b6d15..4ab4ed0c 100644
--- a/varisat/src/decision.rs
+++ b/varisat/src/decision.rs
@@ -2,7 +2,7 @@
 
 use partial_ref::{partial, PartialRef};
 
-use varisat_formula::{Lit, Var};
+use varisat_formula::Var;
 
 use crate::context::{parts::*, Context};
 use crate::prop::{enqueue_assignment, Reason};
@@ -27,10 +27,7 @@ pub fn make_decision(
         .filter(|&var| ctx.part(AssignmentP).var_value(var).is_none())
         .next()
     {
-        let decision = Lit::from_var(
-            decision_var,
-            ctx.part(AssignmentP).last_var_value(decision_var),
-        );
+        let decision = decision_var.lit(ctx.part(AssignmentP).last_var_value(decision_var));
 
         ctx.part_mut(TrailP).new_decision_level();
 
diff --git a/varisat/src/lib.rs b/varisat/src/lib.rs
index 7bef6e61..8e394bae 100644
--- a/varisat/src/lib.rs
+++ b/varisat/src/lib.rs
@@ -28,7 +28,7 @@ mod state;
 mod tmp;
 
 pub use solver::{ProofFormat, Solver};
-pub use varisat_formula::{cnf, lit, CnfFormula, Lit, Var};
+pub use varisat_formula::{cnf, lit, CnfFormula, ExtendFormula, Lit, Var};
 
 pub mod dimacs {
     //! DIMCAS CNF parser and writer.
diff --git a/varisat/src/solver.rs b/varisat/src/solver.rs
index 6a8cb84e..0dd889db 100644
--- a/varisat/src/solver.rs
+++ b/varisat/src/solver.rs
@@ -6,7 +6,7 @@ use partial_ref::{IntoPartialRef, IntoPartialRefMut, PartialRef};
 use failure::{Error, Fail};
 
 use varisat_checker::ProofProcessor;
-use varisat_formula::{CnfFormula, Lit};
+use varisat_formula::{CnfFormula, ExtendFormula, Lit, Var};
 
 use crate::config::SolverConfigUpdate;
 use crate::context::{config_changed, ensure_var_count, parts::*, Context};
@@ -78,13 +78,6 @@ impl<'a> Solver<'a> {
         }
     }
 
-    /// Add a clause to the solver.
-    pub fn add_clause(&mut self, clause: &[Lit]) {
-        self.ensure_var_count_from_slice(clause);
-        let mut ctx = self.ctx.into_partial_ref_mut();
-        load_clause(ctx.borrow(), clause);
-    }
-
     /// Increases the variable count to handle all literals in the given slice.
     fn ensure_var_count_from_slice(&mut self, lits: &[Lit]) {
         if let Some(index) = lits.iter().map(|&lit| lit.index()).max() {
@@ -241,6 +234,23 @@ impl<'a> Drop for Solver<'a> {
     }
 }
 
+impl<'a> ExtendFormula for Solver<'a> {
+    /// Add a clause to the solver.
+    fn add_clause(&mut self, clause: &[Lit]) {
+        self.ensure_var_count_from_slice(clause);
+        let mut ctx = self.ctx.into_partial_ref_mut();
+        load_clause(ctx.borrow(), clause);
+    }
+
+    /// Add a new variable to the solver.
+    fn new_var(&mut self) -> Var {
+        let var_count = self.ctx.assignment.assignment().len();
+        let mut ctx = self.ctx.into_partial_ref_mut();
+        ensure_var_count(ctx.borrow(), var_count + 1);
+        Var::from_index(var_count)
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -489,7 +499,7 @@ mod tests {
                         let skipped = *candidates.last().unwrap();
                         core.push(skipped);
 
-                        let single_clause = CnfFormula::from(Some(&[skipped]));
+                        let single_clause = CnfFormula::from(Some([skipped]));
                         solver.add_formula(&single_clause);
                     },
                     Ok(false) => {
diff --git a/varisat/tests/checker.rs b/varisat/tests/checker.rs
index 5bf9ab55..0a4d43a9 100644
--- a/varisat/tests/checker.rs
+++ b/varisat/tests/checker.rs
@@ -6,7 +6,7 @@ use failure::{Error, Fail};
 use proptest::prelude::*;
 
 use varisat::checker::{CheckedProofStep, Checker, ProofProcessor};
-use varisat::{dimacs::write_dimacs, CnfFormula, Lit, ProofFormat, Solver, Var};
+use varisat::{dimacs::write_dimacs, CnfFormula, ExtendFormula, Lit, ProofFormat, Solver, Var};
 use varisat_formula::test::{conditional_pigeon_hole, sgen_unsat_formula};
 
 proptest! {
@@ -137,7 +137,7 @@ proptest! {
                     let skipped = *candidates.last().unwrap();
                     core.push(skipped);
 
-                    let single_clause = CnfFormula::from(Some(&[skipped]));
+                    let single_clause = CnfFormula::from(Some([skipped]));
                     solver.add_formula(&single_clause);
                 },
                 Ok(false) => {