Repository: chrjabs/rustsat (language: python)

Issue:
General API ergonomics improvements
I have a situation where I need to keep recreating the solver. There is a significant amount of time spent cloning the cnf, because `add_cnf`, which calls `add_clause`, both take by value.

Looking at the implementations of `add_clause`, none of them seem to actually need the clause by value -- but changing `add_clause` to accept `&Clause` "breaks the world", as it would need changing every call to `add_clause`.

My best suggestion (assuming you are happy to improve it), would be to add `add_cnf_ref` and `add_clause_ref` to `Solver`. These will allow people (like me) to add cnf and clauses by reference, and will only require implementing `add_clause_ref` to each solver (which, from trying out with kissat, actually can be done by just renaming `add_clause` to `add_clause_ref`, and then making `add_clause` call `add_clause_ref`, because the `add_clause` implementations don't actually need the clause by value).


Discussion / hints:
This would be awesome, I was also wondering if it is really necessary to pass by value. It wasn't a performance issue for me, but just led to a somewhat ugly code with lots of cloning. Also e.g. `to_dimacs_path` takes `SatInstance` by value, which shouldn't be necessary?

A somewhat related issue is that I'd often want to quickly print out the number of variables and clauses, and `inst.n_clauses()` works fine with a reference, but `inst.var_manager().n_used()` requires a mutable reference, which is often inconvenient.
Very insightful feedback, thanks. Since so far I have mostly been the only user of this library, I mainly wrote the API in a way that worked for me, trying to somewhat think about potential other use cases, but it's always better to get proper feedback.
Here are some thoughts on the API ergonomics mentioned so far:

- `add_clause`: I think I made this take by value thinking that in theory a Rust SAT solver could truly take ownership of a clause. Given that all supported solvers are external, copy clauses literal by literal, and don't even have the same concept of ownership, in hindsight that does not make that much sense. I agree that introducing `add_clause_ref` seems like an easy and very doable fix for this issue.
- `var_manager()`: I think introducing a similar `var_manager_ref()` to be able to access the variable manager without mutability is a good idea. This of course implies that the original method should rather have been named `var_manager_mut()`, which one could introduce as well and deprecate the original `var_manager()`.
- `to_dimacs_path`: this one is slightly more tricky. `to_opb_path` can actually take by reference, but `to_dimacs_path` would at least need to take by mutable reference, which I think would be confusing. This is because `SatInstance` supports non-clausal constraints, while DIMACS CNF does not. So if the instance object contains PB constraints, `to_dimacs_path` will convert them to CNF, mutating the instance, before writing it to file. Rather than changing the signature of `SatInstance::to_dimacs_path`, one could introduce `Cnf::to_dimacs_path`, which would not need mutability.

How do these ideas sound to you for your usecases? Also, it would be great if you could drop any further inconveniences you run into in your applications here.
Maybe I can expand a bit on my typical use cases. For me it's often convenient to define something like
```
struct Foo {
    inst: SatInstance,
    // plus all kinds of parameters that specify what kind of an instance we are building
    // plus all kinds of things that help with mapping domain-specific objects to variables of "inst"
}
```
Then high-level code might look a bit like this:
```
let foo = Foo::new(...);
foo.build_instance(...);
foo.solve_instance(...);
```
And here it would be natural that `build_instance()` and all helper methods it calls take `&mut self` (as it will modify `foo.inst` and other structures), while `solve_instance()` and all helper methods it calls would only need to take `&self`, and solving could be even parallelized.

I understand the challenge that `SatInstance` ≠ `Cnf`. Maybe I should rethink the structure so that we have:
```
struct Foo {
    inst: SatInstance,
    cnf: Cnf,
    // ...
}
```
and the final step of `build_instace()` will also turn `inst` into `cnf`, and `solve_instance` would ignore `inst` and only use `cnf`. Is this closer to the way the library is intended to be used?

For this to work with external solvers one would indeed need to have `Cnf::to_dimacs_path`.
I see. Do you ever incrementally change the `SatInstance` after the initial `build_instance` call? If not, I would even suggest only keeping the `Cnf` around or (if you are not using any PB constraints when creating the instance) only ever working with a `Cnf`. I somewhat intentionally kept the `Cnf` struct simpler and more light weight, so that might mean a bit more manual work, but if you only have clausal constraints, it shouldn't be that much.
One small API inconvenience:

It's a common use case for me that I have e.g. `lits: Vec<Lit>` and I'd like to add it as a clause. Now it's something like `inst.add_clause(lits.as_slice().into())`, but maybe there could be a convenience method that would let me do e.g. `inst.add_xxx(&lits)` in this case? After all, we can conveniently use `&[Lit]` in e.g. `add_clause_impl_clause`, so this would be analogous. I do not know what would be a good naming convention here, though. Maybe `add_nary` so that it's following the pattern `add_binary` and `add_ternary`?
Just for your information, I'll give you an overview of what I'm doing :)

I'm actually generating my SAT instance using an external program ( https://github.com/conjure-cp/conjure ), which takes a high-level language and turns it into SAT. I then I have a little structure like:

```
pub struct SatCore {
    pub solver: Arc<Mutex<Solver>>,
    pub cnf: Arc<Cnf>,
}
```

Then I create a thread local copy of this using the `thread_local` package, so every thread gets it's own solver.

I then use rayon to solve problems in parallel which require lots of solving SAT instances.
For boring technical reasons (I can explain, or at some point I'll write a paper :) ), I sometimes need to assign a bunch of literals, and then later I need to 'unassign' them which you can't really do, so I just recreate the solver from the Cnf (I know I could do this with assumptions, but I get much better performance by assigning for my problem), so I recreate the solve by doing:

```
          let mut solver = Solver::default();
            solver
                .add_cnf(self.cnf.as_ref().clone())
                .expect("FATAL: Solver bug");
```

Then pop it into the mutex:

```
            let mut mutex_solver = self.solver.lock().unwrap();
            *mutex_solver = solver;
```

Good news, this works really well! My laptop has 32 cores, which I can saturate fairly easily just using rayon's par_iter.

Fix patch:
diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs
index 2dd045bb..2303370f 100644
--- a/cadical/src/lib.rs
+++ b/cadical/src/lib.rs
@@ -351,6 +351,15 @@ impl Extend<Clause> for CaDiCaL<'_, '_> {
     }
 }
 
+impl<'a> Extend<&'a Clause> for CaDiCaL<'_, '_> {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(cl)
+                .expect("Error adding clause in extend")
+        })
+    }
+}
+
 impl Solve for CaDiCaL<'_, '_> {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::ccadical_signature() };
@@ -427,7 +436,7 @@ impl Solve for CaDiCaL<'_, '_> {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -436,7 +445,7 @@ impl Solve for CaDiCaL<'_, '_> {
         self.state = InternalSolverState::Input;
         // Call CaDiCaL backend
         clause
-            .into_iter()
+            .iter()
             .for_each(|l| unsafe { ffi::ccadical_add(self.handle, l.to_ipasir()) });
         unsafe { ffi::ccadical_add(self.handle, 0) };
         Ok(())
diff --git a/data/tiny-single-opt.opb b/data/tiny-single-opt.opb
new file mode 100644
index 00000000..042f3b78
--- /dev/null
+++ b/data/tiny-single-opt.opb
@@ -0,0 +1,6 @@
+* #variable= 4 #constraint= 3
+* A handwritten OPB sat instance for basic testing
+min: 1 x1 2 x2;
+5 x1 -3 x2 >= 4;
+5 x3 -3 x4 >= 2;
+5 ~x4 >= 4;
diff --git a/docs/0-5-0-migration-guide.md b/docs/0-5-0-migration-guide.md
new file mode 100644
index 00000000..c7203dab
--- /dev/null
+++ b/docs/0-5-0-migration-guide.md
@@ -0,0 +1,47 @@
+# Migration Guide for Breaking Changes in v0.5.0
+
+This document gives an overview of the breaking API changes in v0.5.0 and how
+to update your code accordingly. Mostly, follow the error messages the compiler
+will give you after updating to the new RustSAT version.
+
+## Error Handling
+
+Error handling in the `Solve` trait, and file parsers now uses the
+[`anyhow`](https://docs.rs/anyhow/latest/anyhow/) crate. This allows for better
+error messages, and better tracing. In the process, some of the error types or
+variants that are not needed any more have been removed:
+
+- `rustsat::solvers::SolverError` has been removed and only
+  `rustsat::solvers::StateError` remains
+- `rustsat::instances::fio::opb::Error` has been removed
+- `rustsat::instances::fio::dimacs::Error` has been removed
+- `rustsat::instances::fio::ParsingError` has been removed
+- `rustsat::solvers::SolverState::Error` has also been removed as no error
+  state is needed with proper error returns
+
+If you need to handle a specific error, you can use `anyhow`'s
+[`downcast`](https://docs.rs/anyhow/latest/anyhow/struct.Error.html#method.downcast)
+(e.g., on `solvers::StateError`), but I imagine most often these errors are
+anyhow just propagated outwards and displayed.
+
+## Changes to Improve API Ergonomics
+
+There have been some API changes to improve usability, even though they are breaking.
+
+- File writing methods: all file writing methods (on `SatInstance`,
+  `OptInstance` and `MultiOptInstance`) are now called `write_` instead of `to_`.
+  Furthermore they take references instead of values and will return an error if
+  a specific format of the instance is expected but the instance does not satisfy
+  this requirement.
+- File reading methods: all file reading methods (DIMACS and OPB, on
+  `SatInsatnce`, etc) now require a `BufRead` type as input. Previously, the
+  reader was internally wrapped in a
+  [`BufReader`](https://doc.rust-lang.org/stable/std/io/struct.BufReader.html)
+  object. This now has to be done externally to avoid potentially double
+  buffering.
+- "Heavy" conversion function (e.g., `SatInstance::to_cnf`) are now called
+  `into_`. Additionally, inplace converter functions named `convert_to_` are also
+  provided.
+- Methods providing references to internal data are now named `_ref` and `_mut`
+  if mutability is allowed. If only a non-mutable accessor is present, the `_ref`
+  suffix is omitted (e.g., for `SatInstance::cnf`).
diff --git a/glucose/src/core.rs b/glucose/src/core.rs
index 1c4a5231..ab9b4769 100644
--- a/glucose/src/core.rs
+++ b/glucose/src/core.rs
@@ -82,6 +82,15 @@ impl Extend<Clause> for Glucose {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Glucose {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(cl)
+                .expect("Error adding clause in extend")
+        })
+    }
+}
+
 impl Solve for Glucose {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::cglucose4_signature() };
@@ -150,7 +159,7 @@ impl Solve for Glucose {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -158,7 +167,7 @@ impl Solve for Glucose {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call glucose backend
-        clause.into_iter().for_each(|l| unsafe {
+        clause.iter().for_each(|l| unsafe {
             ffi::cglucose4_add(self.handle, l.to_ipasir());
         });
         unsafe { ffi::cglucose4_add(self.handle, 0) };
diff --git a/glucose/src/simp.rs b/glucose/src/simp.rs
index 133dd083..84fcee65 100644
--- a/glucose/src/simp.rs
+++ b/glucose/src/simp.rs
@@ -90,6 +90,15 @@ impl Extend<Clause> for Glucose {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Glucose {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(cl)
+                .expect("Error adding clause in extend")
+        })
+    }
+}
+
 impl Solve for Glucose {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::cglucose4_signature() };
@@ -158,7 +167,7 @@ impl Solve for Glucose {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -166,7 +175,7 @@ impl Solve for Glucose {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call glucose backend
-        clause.into_iter().for_each(|l| unsafe {
+        clause.iter().for_each(|l| unsafe {
             ffi::cglucosesimp4_add(self.handle, l.to_ipasir());
         });
         unsafe { ffi::cglucosesimp4_add(self.handle, 0) };
diff --git a/ipasir/src/lib.rs b/ipasir/src/lib.rs
index e4806b45..a1938893 100644
--- a/ipasir/src/lib.rs
+++ b/ipasir/src/lib.rs
@@ -186,7 +186,7 @@ impl Solve for IpasirSolver<'_, '_> {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         clause.iter().for_each(|l| match self.stats.max_var {
@@ -202,7 +202,7 @@ impl Solve for IpasirSolver<'_, '_> {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call IPASIR backend
-        for lit in &clause {
+        for lit in clause {
             unsafe { ffi::ipasir_add(self.handle, lit.to_ipasir()) }
         }
         unsafe { ffi::ipasir_add(self.handle, 0) };
@@ -369,6 +369,15 @@ impl Extend<Clause> for IpasirSolver<'_, '_> {
     }
 }
 
+impl<'a> Extend<&'a Clause> for IpasirSolver<'_, '_> {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(cl)
+                .expect("Error adding clause in extend")
+        })
+    }
+}
+
 /// cbindgen:ignore
 mod ffi {
     use super::{LearnCallbackPtr, TermCallbackPtr};
diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs
index 900a4e1e..e0172c8a 100644
--- a/kissat/src/lib.rs
+++ b/kissat/src/lib.rs
@@ -188,6 +188,15 @@ impl Extend<Clause> for Kissat<'_> {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Kissat<'_> {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(cl)
+                .expect("Error adding clause in extend")
+        })
+    }
+}
+
 impl Solve for Kissat<'_> {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::kissat_signature() };
@@ -260,7 +269,7 @@ impl Solve for Kissat<'_> {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Kissat is non-incremental, so only add if in input or configuring state
         if !matches!(
             self.state,
@@ -288,7 +297,7 @@ impl Solve for Kissat<'_> {
         self.state = InternalSolverState::Input;
         // Call Kissat backend
         clause
-            .into_iter()
+            .iter()
             .for_each(|l| unsafe { ffi::kissat_add(self.handle, l.to_ipasir()) });
         unsafe { ffi::kissat_add(self.handle, 0) };
         Ok(())
diff --git a/minisat/src/core.rs b/minisat/src/core.rs
index 7fa688ea..5d1200b4 100644
--- a/minisat/src/core.rs
+++ b/minisat/src/core.rs
@@ -82,6 +82,15 @@ impl Extend<Clause> for Minisat {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Minisat {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(cl)
+                .expect("Error adding clause in extend")
+        })
+    }
+}
+
 impl Solve for Minisat {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::cminisat_signature() };
@@ -150,7 +159,7 @@ impl Solve for Minisat {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -158,7 +167,7 @@ impl Solve for Minisat {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call minisat backend
-        clause.into_iter().for_each(|l| unsafe {
+        clause.iter().for_each(|l| unsafe {
             ffi::cminisat_add(self.handle, l.to_ipasir());
         });
         unsafe { ffi::cminisat_add(self.handle, 0) };
diff --git a/minisat/src/simp.rs b/minisat/src/simp.rs
index e0991260..8c56b86b 100644
--- a/minisat/src/simp.rs
+++ b/minisat/src/simp.rs
@@ -90,6 +90,15 @@ impl Extend<Clause> for Minisat {
     }
 }
 
+impl<'a> Extend<&'a Clause> for Minisat {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(cl)
+                .expect("Error adding clause in extend")
+        })
+    }
+}
+
 impl Solve for Minisat {
     fn signature(&self) -> &'static str {
         let c_chars = unsafe { ffi::cminisat_signature() };
@@ -158,7 +167,7 @@ impl Solve for Minisat {
         }
     }
 
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
         // Update wrapper-internal state
         self.stats.n_clauses += 1;
         self.stats.avg_clause_len =
@@ -166,7 +175,7 @@ impl Solve for Minisat {
                 / self.stats.n_clauses as f32;
         self.state = InternalSolverState::Input;
         // Call minisat backend
-        clause.into_iter().for_each(|l| unsafe {
+        clause.iter().for_each(|l| unsafe {
             ffi::cminisatsimp_add(self.handle, l.to_ipasir());
         });
         unsafe { ffi::cminisatsimp_add(self.handle, 0) };
diff --git a/rustsat/.gitignore b/rustsat/.gitignore
new file mode 100644
index 00000000..79cbaa16
--- /dev/null
+++ b/rustsat/.gitignore
@@ -0,0 +1,4 @@
+rustsat-test.opb
+rustsat-test.cnf
+rustsat-test.wcnf
+rustsat-test.mcnf
diff --git a/rustsat/src/encodings/card.rs b/rustsat/src/encodings/card.rs
index 7bb3ab93..9ba9f4d9 100644
--- a/rustsat/src/encodings/card.rs
+++ b/rustsat/src/encodings/card.rs
@@ -356,7 +356,7 @@ pub fn encode_cardinality_constraint<CE: BoundBoth + FromIterator<Lit>, Col: Col
         return;
     }
     if constr.is_clause() {
-        collector.extend([constr.as_clause().unwrap()]);
+        collector.extend([constr.into_clause().unwrap()]);
         return;
     }
     CE::encode_constr(constr, collector, var_manager).unwrap()
diff --git a/rustsat/src/encodings/nodedb.rs b/rustsat/src/encodings/nodedb.rs
index fba5bf17..6bd575e3 100644
--- a/rustsat/src/encodings/nodedb.rs
+++ b/rustsat/src/encodings/nodedb.rs
@@ -291,6 +291,7 @@ impl NodeCon {
 }
 
 /// Trait for a database managing [`NodeLike`]s by their [`NodeId`]s
+#[allow(dead_code)]
 pub trait NodeById: IndexMut<NodeId, Output = Self::Node> {
     /// The type of node in the database
     type Node: NodeLike;
diff --git a/rustsat/src/encodings/pb.rs b/rustsat/src/encodings/pb.rs
index f52b17b4..ca7557e5 100644
--- a/rustsat/src/encodings/pb.rs
+++ b/rustsat/src/encodings/pb.rs
@@ -405,11 +405,11 @@ pub fn encode_pb_constraint<PBE: BoundBoth + FromIterator<(Lit, usize)>, Col: Co
         return;
     }
     if constr.is_clause() {
-        collector.extend([constr.as_clause().unwrap()]);
+        collector.extend([constr.into_clause().unwrap()]);
         return;
     }
     if constr.is_card() {
-        let card = constr.as_card_constr().unwrap();
+        let card = constr.into_card_constr().unwrap();
         return card::default_encode_cardinality_constraint(card, collector, var_manager);
     }
     PBE::encode_constr(constr, collector, var_manager).unwrap()
diff --git a/rustsat/src/instances/fio.rs b/rustsat/src/instances/fio.rs
index 3ee2cc9f..f258299f 100644
--- a/rustsat/src/instances/fio.rs
+++ b/rustsat/src/instances/fio.rs
@@ -17,29 +17,35 @@ pub struct ObjNoExist(usize);
 
 /// Opens a reader for the file at Path.
 /// With feature `compression` supports bzip2 and gzip compression.
-pub(crate) fn open_compressed_uncompressed_read<P: AsRef<Path>>(
+pub fn open_compressed_uncompressed_read<P: AsRef<Path>>(
     path: P,
-) -> Result<Box<dyn io::Read>, io::Error> {
+) -> Result<Box<dyn io::BufRead>, io::Error> {
     let path = path.as_ref();
     let raw_reader = File::open(path)?;
     #[cfg(feature = "compression")]
     if let Some(ext) = path.extension() {
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("bz2")) {
-            return Ok(Box::new(bzip2::read::BzDecoder::new(raw_reader)));
+            return Ok(Box::new(io::BufReader::new(bzip2::read::BzDecoder::new(
+                raw_reader,
+            ))));
         }
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("gz")) {
-            return Ok(Box::new(flate2::read::GzDecoder::new(raw_reader)));
+            return Ok(Box::new(io::BufReader::new(flate2::read::GzDecoder::new(
+                raw_reader,
+            ))));
         }
         if ext.eq_ignore_ascii_case(std::ffi::OsStr::new("xz")) {
-            return Ok(Box::new(xz2::read::XzDecoder::new(raw_reader)));
+            return Ok(Box::new(io::BufReader::new(xz2::read::XzDecoder::new(
+                raw_reader,
+            ))));
         }
     }
-    Ok(Box::new(raw_reader))
+    Ok(Box::new(io::BufReader::new(raw_reader)))
 }
 
 /// Opens a writer for the file at Path.
 /// With feature `compression` supports bzip2 and gzip compression.
-pub(crate) fn open_compressed_uncompressed_write<P: AsRef<Path>>(
+pub fn open_compressed_uncompressed_write<P: AsRef<Path>>(
     path: P,
 ) -> Result<Box<dyn io::Write>, io::Error> {
     let path = path.as_ref();
diff --git a/rustsat/src/instances/fio/dimacs.rs b/rustsat/src/instances/fio/dimacs.rs
index 76e9e92e..d121a7ed 100644
--- a/rustsat/src/instances/fio/dimacs.rs
+++ b/rustsat/src/instances/fio/dimacs.rs
@@ -12,7 +12,7 @@
 
 use crate::{
     instances::{Cnf, ManageVars, SatInstance},
-    types::{Clause, Lit, Var},
+    types::{Clause, Lit},
 };
 use anyhow::Context;
 use nom::{
@@ -27,7 +27,7 @@ use nom::{
 };
 use std::{
     convert::TryFrom,
-    io::{self, BufRead, BufReader, Read, Write},
+    io::{self, BufRead, Write},
 };
 use thiserror::Error;
 
@@ -53,10 +53,9 @@ pub struct InvalidPLine(String);
 /// Parses a CNF instance from a reader (typically a (compressed) file)
 pub fn parse_cnf<R, VM>(reader: R) -> anyhow::Result<SatInstance<VM>>
 where
-    R: Read,
+    R: BufRead,
     VM: ManageVars + Default,
 {
-    let reader = BufReader::new(reader);
     let content = parse_dimacs(reader)?;
     #[cfg(not(feature = "optimization"))]
     {
@@ -73,12 +72,11 @@ where
 /// (compressed) file). The objective with the index obj_idx is used.
 pub fn parse_wcnf_with_idx<R, VM>(reader: R, obj_idx: usize) -> anyhow::Result<OptInstance<VM>>
 where
-    R: Read,
+    R: BufRead,
     VM: ManageVars + Default,
 {
     use super::ObjNoExist;
 
-    let reader = BufReader::new(reader);
     let (constrs, mut objs) = parse_dimacs(reader)?;
     if objs.is_empty() {
         objs.push(Objective::default());
@@ -95,10 +93,9 @@ where
 /// Parses a MCNF instance (old or new format) from a reader (typically a (compressed) file)
 pub fn parse_mcnf<R, VM>(reader: R) -> anyhow::Result<MultiOptInstance<VM>>
 where
-    R: Read,
+    R: BufRead,
     VM: ManageVars + Default,
 {
-    let reader = BufReader::new(reader);
     let (constrs, objs) = parse_dimacs(reader)?;
     Ok(MultiOptInstance::compose(constrs, objs))
 }
@@ -472,22 +469,12 @@ fn parse_clause_ending(input: &str) -> IResult<&str, &str> {
 /// Writes a CNF to a DIMACS CNF file
 pub fn write_cnf_annotated<W: Write>(
     writer: &mut W,
-    cnf: Cnf,
-    max_var: Option<Var>,
+    cnf: &Cnf,
+    n_vars: u32,
 ) -> Result<(), io::Error> {
     writeln!(writer, "c CNF file written by RustSAT")?;
-    writeln!(
-        writer,
-        "p cnf {} {}",
-        if let Some(max_var) = max_var {
-            max_var.pos_lit().to_ipasir()
-        } else {
-            0
-        },
-        cnf.len()
-    )?;
-    cnf.into_iter()
-        .try_for_each(|cl| write_clause(writer, cl))?;
+    writeln!(writer, "p cnf {} {}", n_vars, cnf.len())?;
+    cnf.iter().try_for_each(|cl| write_clause(writer, cl))?;
     writer.flush()
 }
 
@@ -506,7 +493,7 @@ pub fn write_cnf<W: Write, Iter: Iterator<Item = CnfLine>>(
 ) -> Result<(), io::Error> {
     data.try_for_each(|dat| match dat {
         CnfLine::Comment(c) => write!(writer, "c {}", c),
-        CnfLine::Clause(cl) => write_clause(writer, cl),
+        CnfLine::Clause(cl) => write_clause(writer, &cl),
     })
 }
 
@@ -514,26 +501,26 @@ pub fn write_cnf<W: Write, Iter: Iterator<Item = CnfLine>>(
 /// Writes a CNF and soft clauses to a (post 22, no p line) DIMACS WCNF file
 pub fn write_wcnf_annotated<W: Write, CI: WClsIter>(
     writer: &mut W,
-    cnf: Cnf,
+    cnf: &Cnf,
     softs: (CI, isize),
-    max_var: Option<Var>,
+    n_vars: Option<u32>,
 ) -> Result<(), io::Error> {
     let (soft_cls, offset) = softs;
     let soft_cls: Vec<(Clause, usize)> = soft_cls.into_iter().collect();
     writeln!(writer, "c WCNF file written by RustSAT")?;
-    if let Some(mv) = max_var {
-        writeln!(writer, "c highest var: {}", mv.pos_lit().to_ipasir())?;
+    if let Some(n_vars) = n_vars {
+        writeln!(writer, "c {} variables", n_vars)?;
     }
     writeln!(writer, "c {} hard clauses", cnf.len())?;
     writeln!(writer, "c {} soft clauses", soft_cls.len())?;
     writeln!(writer, "c objective offset: {}", offset)?;
-    cnf.into_iter().try_for_each(|cl| {
+    cnf.iter().try_for_each(|cl| {
         write!(writer, "h ")?;
         write_clause(writer, cl)
     })?;
     soft_cls.into_iter().try_for_each(|(cl, w)| {
         write!(writer, "{} ", w)?;
-        write_clause(writer, cl)
+        write_clause(writer, &cl)
     })?;
     writer.flush()
 }
@@ -559,22 +546,22 @@ pub fn write_wcnf<W: Write, Iter: Iterator<Item = WcnfLine>>(
         WcnfLine::Comment(c) => write!(writer, "c {}", c),
         WcnfLine::Hard(cl) => {
             write!(writer, "h ")?;
-            write_clause(writer, cl)
+            write_clause(writer, &cl)
         }
         WcnfLine::Soft(cl, w) => {
             write!(writer, "{} ", w)?;
-            write_clause(writer, cl)
+            write_clause(writer, &cl)
         }
     })
 }
 
 #[cfg(feature = "multiopt")]
 /// Writes a CNF and multiple objectives as sets of soft clauses to a DIMACS MCNF file
-pub fn write_mcnf_annotated<W: Write, CI: WClsIter>(
+pub fn write_mcnf_annotated<W: Write, Iter: Iterator<Item = (CI, isize)>, CI: WClsIter>(
     writer: &mut W,
-    cnf: Cnf,
-    softs: Vec<(CI, isize)>,
-    max_var: Option<Var>,
+    cnf: &Cnf,
+    softs: Iter,
+    n_vars: Option<u32>,
 ) -> Result<(), io::Error> {
     let (soft_cls, offsets) = softs.into_iter().unzip::<_, _, Vec<_>, Vec<_>>();
     let soft_cls: Vec<Vec<(Clause, usize)>> = soft_cls
@@ -582,8 +569,8 @@ pub fn write_mcnf_annotated<W: Write, CI: WClsIter>(
         .map(|ci| ci.into_iter().collect())
         .collect();
     writeln!(writer, "c MCNF file written by RustSAT")?;
-    if let Some(mv) = max_var {
-        writeln!(writer, "c highest var: {}", mv.pos_lit().to_ipasir())?;
+    if let Some(n_vars) = n_vars {
+        writeln!(writer, "c {} variables", n_vars)?;
     }
     writeln!(writer, "c {} hard clauses", cnf.len())?;
     writeln!(writer, "c {} objectives", soft_cls.len())?;
@@ -597,7 +584,7 @@ pub fn write_mcnf_annotated<W: Write, CI: WClsIter>(
         .into_iter()
         .try_for_each(|o| write!(writer, "{} ", o))?;
     writeln!(writer, ")")?;
-    cnf.into_iter().try_for_each(|cl| {
+    cnf.iter().try_for_each(|cl| {
         write!(writer, "h ")?;
         write_clause(writer, cl)
     })?;
@@ -607,7 +594,7 @@ pub fn write_mcnf_annotated<W: Write, CI: WClsIter>(
         .try_for_each(|(idx, sft_cls)| {
             sft_cls.into_iter().try_for_each(|(cl, w)| {
                 write!(writer, "o{} {} ", idx + 1, w)?;
-                write_clause(writer, cl)
+                write_clause(writer, &cl)
             })
         })?;
     writer.flush()
@@ -634,16 +621,16 @@ pub fn write_mcnf<W: Write, Iter: Iterator<Item = McnfLine>>(
         McnfLine::Comment(c) => writeln!(writer, "c {}", c),
         McnfLine::Hard(cl) => {
             write!(writer, "h ")?;
-            write_clause(writer, cl)
+            write_clause(writer, &cl)
         }
         McnfLine::Soft(cl, w, oidx) => {
             write!(writer, "o{} {} ", oidx + 1, w)?;
-            write_clause(writer, cl)
+            write_clause(writer, &cl)
         }
     })
 }
 
-fn write_clause<W: Write>(writer: &mut W, clause: Clause) -> Result<(), io::Error> {
+fn write_clause<W: Write>(writer: &mut W, clause: &Clause) -> Result<(), io::Error> {
     clause
         .into_iter()
         .try_for_each(|l| write!(writer, "{} ", l.to_ipasir()))?;
@@ -659,7 +646,7 @@ mod tests {
     use crate::{
         clause,
         instances::{Cnf, SatInstance},
-        ipasir_lit, var,
+        ipasir_lit,
     };
     use nom::error::Error as NomError;
     use std::io::{Cursor, Seek};
@@ -1093,12 +1080,12 @@ mod tests {
 
         let mut cursor = Cursor::new(vec![]);
 
-        write_cnf_annotated(&mut cursor, true_cnf.clone(), Some(var![1])).unwrap();
+        write_cnf_annotated(&mut cursor, &true_cnf, 2).unwrap();
 
         cursor.rewind().unwrap();
 
         let parsed_inst: SatInstance = super::parse_cnf(cursor).unwrap();
-        let (parsed_cnf, _) = parsed_inst.as_cnf();
+        let (parsed_cnf, _) = parsed_inst.into_cnf();
 
         assert_eq!(parsed_cnf, true_cnf);
     }
@@ -1110,14 +1097,15 @@ mod tests {
         let mut true_obj = Objective::new();
         true_constrs.add_clause(clause![ipasir_lit![1], ipasir_lit![2]]);
         true_obj.add_soft_clause(10, clause![ipasir_lit![-3], ipasir_lit![4], ipasir_lit![5]]);
+        let offset = true_obj.offset();
 
         let mut cursor = Cursor::new(vec![]);
 
         write_wcnf_annotated(
             &mut cursor,
-            true_constrs.clone().as_cnf().0,
-            true_obj.clone().as_soft_cls(),
-            Some(var![1]),
+            &true_constrs.cnf(),
+            (true_obj.iter_soft_cls(), offset),
+            Some(5),
         )
         .unwrap();
 
@@ -1136,18 +1124,21 @@ mod tests {
         let mut true_obj1 = Objective::new();
         true_constrs.add_clause(clause![ipasir_lit![1], ipasir_lit![2]]);
         true_obj0.add_soft_clause(3, clause![ipasir_lit![-1]]);
+        let offset0 = true_obj0.offset();
         true_obj1.add_soft_clause(10, clause![ipasir_lit![-3], ipasir_lit![4], ipasir_lit![5]]);
+        let offset1 = true_obj1.offset();
 
         let mut cursor = Cursor::new(vec![]);
 
         write_mcnf_annotated(
             &mut cursor,
-            true_constrs.clone().as_cnf().0,
+            &true_constrs.cnf(),
             vec![
-                true_obj0.clone().as_soft_cls(),
-                true_obj1.clone().as_soft_cls(),
-            ],
-            Some(var![4]),
+                (true_obj0.iter_soft_cls(), offset0),
+                (true_obj1.iter_soft_cls(), offset1),
+            ]
+            .into_iter(),
+            Some(5),
         )
         .unwrap();
 
diff --git a/rustsat/src/instances/fio/opb.rs b/rustsat/src/instances/fio/opb.rs
index 8c1d941e..a2f78782 100644
--- a/rustsat/src/instances/fio/opb.rs
+++ b/rustsat/src/instances/fio/opb.rs
@@ -27,7 +27,7 @@ use nom::{
     IResult,
 };
 use std::{
-    io::{self, BufRead, BufReader, Read, Write},
+    io::{self, BufRead, Write},
     num::TryFromIntError,
 };
 
@@ -92,7 +92,7 @@ enum OpbData {
 /// Parses the constraints from an OPB file as a [`SatInstance`]
 pub fn parse_sat<R, VM>(reader: R, opts: Options) -> anyhow::Result<SatInstance<VM>>
 where
-    R: Read,
+    R: BufRead,
     VM: ManageVars + Default,
 {
     let data = parse_opb_data(reader, opts)?;
@@ -114,7 +114,7 @@ pub fn parse_opt_with_idx<R, VM>(
     opts: Options,
 ) -> anyhow::Result<OptInstance<VM>>
 where
-    R: Read,
+    R: BufRead,
     VM: ManageVars + Default,
 {
     use super::ObjNoExist;
@@ -149,7 +149,7 @@ where
 /// index (starting from 0).
 pub fn parse_multi_opt<R, VM>(reader: R, opts: Options) -> anyhow::Result<MultiOptInstance<VM>>
 where
-    R: Read,
+    R: BufRead,
     VM: ManageVars + Default,
 {
     let data = parse_opb_data(reader, opts)?;
@@ -164,8 +164,7 @@ where
 }
 
 /// Parses all OPB data of a reader
-fn parse_opb_data<R: Read>(reader: R, opts: Options) -> anyhow::Result<Vec<OpbData>> {
-    let mut reader = BufReader::new(reader);
+fn parse_opb_data<R: BufRead>(mut reader: R, opts: Options) -> anyhow::Result<Vec<OpbData>> {
     let mut buf = String::new();
     let mut data = vec![];
     // TODO: consider not necessarily reading a full line
@@ -350,7 +349,7 @@ fn opb_data(input: &str, opts: Options) -> IResult<&str, OpbData> {
 /// Writes a [`SatInstance`] to an OPB file
 pub fn write_sat<W, VM>(
     writer: &mut W,
-    inst: SatInstance<VM>,
+    inst: &SatInstance<VM>,
     opts: Options,
 ) -> Result<(), io::Error>
 where
@@ -371,125 +370,103 @@ where
     writeln!(writer, "* {} cardinality constraints", inst.cards.len())?;
     writeln!(writer, "* {} pseudo-boolean constraints", inst.pbs.len())?;
     inst.cnf
-        .into_iter()
+        .iter()
         .try_for_each(|cl| write_clause(writer, cl, opts))?;
     inst.cards
-        .into_iter()
+        .iter()
         .try_for_each(|card| write_card(writer, card, opts))?;
     inst.pbs
-        .into_iter()
+        .iter()
         .try_for_each(|pb| write_pb(writer, pb, opts))?;
     writer.flush()
 }
 
 #[cfg(feature = "optimization")]
-/// Writes an [`OptInstance`] to an OPB file
-pub fn write_opt<W, VM>(
+/// Writes an optimization instance to an OPB file
+pub fn write_opt<W, VM, LI>(
     writer: &mut W,
-    inst: OptInstance<VM>,
+    constrs: &SatInstance<VM>,
+    obj: (LI, isize),
     opts: Options,
 ) -> Result<(), io::Error>
 where
     W: Write,
+    LI: WLitIter,
     VM: ManageVars,
 {
-    let (constrs, obj) = inst.decompose();
-    let cnf = constrs.cnf;
-    let cards = constrs.cards;
-    let pbs = constrs.pbs;
-    let mut vm = constrs.var_manager;
-    let (hardened, softs) = obj.as_soft_lits(&mut vm);
+    let cnf = &constrs.cnf;
+    let cards = &constrs.cards;
+    let pbs = &constrs.pbs;
     writeln!(
         writer,
         "* #variable = {} #constraint= {}",
-        vm.n_used(),
+        constrs.n_vars(),
         cnf.len() + cards.len() + pbs.len()
     )?;
     writeln!(writer, "* OPB file written by RustSAT")?;
-    if let Some(max_var) = vm.max_var() {
+    if let Some(max_var) = constrs.max_var() {
         writeln!(writer, "* maximum variable: {}", max_var)?;
     }
     writeln!(writer, "* {} original hard clauses", cnf.len())?;
     writeln!(writer, "* {} cardinality constraints", cards.len())?;
     writeln!(writer, "* {} pseudo-boolean constraints", pbs.len())?;
-    writeln!(
-        writer,
-        "* {} relaxed and hardened soft clauses",
-        hardened.len()
-    )?;
-    write_objective(writer, softs, opts)?;
-    hardened
-        .into_iter()
-        .try_for_each(|cl| write_clause(writer, cl, opts))?;
-    cnf.into_iter()
+    write_objective(writer, obj, opts)?;
+    cnf.iter()
         .try_for_each(|cl| write_clause(writer, cl, opts))?;
     cards
-        .into_iter()
+        .iter()
         .try_for_each(|card| write_card(writer, card, opts))?;
-    pbs.into_iter()
-        .try_for_each(|pb| write_pb(writer, pb, opts))?;
+    pbs.iter().try_for_each(|pb| write_pb(writer, pb, opts))?;
     writer.flush()
 }
 
 #[cfg(feature = "multiopt")]
 /// Writes a [`MultiOptInstance`] to an OPB file
-pub fn write_multi_opt<W, VM>(
+pub fn write_multi_opt<W, VM, Iter, LI>(
     writer: &mut W,
-    inst: MultiOptInstance<VM>,
+    constrs: &SatInstance<VM>,
+    mut objs: Iter,
     opts: Options,
 ) -> Result<(), io::Error>
 where
     W: Write,
     VM: ManageVars,
+    Iter: Iterator<Item = (LI, isize)>,
+    LI: WLitIter,
 {
-    let (constrs, objs) = inst.decompose();
-    let cnf = constrs.cnf;
-    let cards = constrs.cards;
-    let pbs = constrs.pbs;
-    let mut vm = constrs.var_manager;
-    let (hardened, objs) = objs
-        .into_iter()
-        .map(|o| o.as_soft_lits(&mut vm))
-        .unzip::<_, _, Vec<_>, Vec<_>>();
+    let cnf = &constrs.cnf;
+    let cards = &constrs.cards;
+    let pbs = &constrs.pbs;
     writeln!(
         writer,
         "* #variable = {} #constraint= {}",
-        vm.n_used(),
+        constrs.n_vars(),
         cnf.len() + cards.len() + pbs.len()
     )?;
     writeln!(writer, "* OPB file written by RustSAT")?;
-    if let Some(max_var) = vm.max_var() {
+    if let Some(max_var) = constrs.max_var() {
         writeln!(writer, "* maximum variable: {}", max_var)?;
     }
     writeln!(writer, "* {} original hard clauses", cnf.len())?;
     writeln!(writer, "* {} cardinality constraints", cards.len())?;
     writeln!(writer, "* {} pseudo-boolean constraints", pbs.len())?;
     write!(writer, "* ( ")?;
-    hardened
-        .iter()
-        .try_for_each(|h| write!(writer, "{} ", h.len()))?;
     writeln!(writer, ") relaxed and hardened soft clauses",)?;
-    objs.into_iter()
-        .try_for_each(|softs| write_objective(writer, softs, opts))?;
-    hardened.into_iter().try_for_each(|h| {
-        h.into_iter()
-            .try_for_each(|cl| write_clause(writer, cl, opts))
-    })?;
-    cnf.into_iter()
+    objs.try_for_each(|softs| write_objective(writer, softs, opts))?;
+    cnf.iter()
         .try_for_each(|cl| write_clause(writer, cl, opts))?;
     cards
-        .into_iter()
+        .iter()
         .try_for_each(|card| write_card(writer, card, opts))?;
-    pbs.into_iter()
-        .try_for_each(|pb| write_pb(writer, pb, opts))?;
+    pbs.iter().try_for_each(|pb| write_pb(writer, pb, opts))?;
     writer.flush()
 }
 
 /// Writes a clause to an OPB file
-fn write_clause<W: Write>(writer: &mut W, clause: Clause, opts: Options) -> Result<(), io::Error> {
+fn write_clause<W: Write>(writer: &mut W, clause: &Clause, opts: Options) -> Result<(), io::Error> {
     if opts.no_negated_lits {
         let mut rhs: isize = 1;
-        clause.into_iter().try_for_each(|l| {
+        clause.iter().try_for_each(|l| {
             if l.is_pos() {
                 write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx)
             } else {
@@ -499,7 +476,7 @@ fn write_clause<W: Write>(writer: &mut W, clause: Clause, opts: Options) -> Resu
         })?;
         writeln!(writer, ">= {};", rhs)
     } else {
-        clause.into_iter().try_for_each(|l| {
+        clause.iter().try_for_each(|l| {
             if l.is_pos() {
                 write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx)
             } else {
@@ -513,123 +490,137 @@ fn write_clause<W: Write>(writer: &mut W, clause: Clause, opts: Options) -> Resu
 /// Writes a cardinality constraint to an OPB file
 fn write_card<W: Write>(
     writer: &mut W,
-    card: CardConstraint,
+    card: &CardConstraint,
     opts: Options,
 ) -> Result<(), io::Error> {
+    let mut iter_a;
+    let mut iter_b;
+    let neg_lit = |l: &Lit| !*l;
     if opts.no_negated_lits {
-        let (lits, bound, op) = match card {
+        let (lits, bound, op): (&mut dyn Iterator<Item = Lit>, _, _) = match card {
             CardConstraint::UB(constr) => {
-                let (lits, bound) = constr.decompose();
-                let bound = lits.len() as isize - bound as isize;
+                let (lits, bound) = constr.decompose_ref();
+                let bound = lits.len() as isize - *bound as isize;
                 // Flip operator by negating literals
-                let lits: Vec<Lit> = lits.into_iter().map(|l| !l).collect();
-                (lits, bound, ">=")
+                iter_a = lits.iter().map(neg_lit);
+                (&mut iter_a, bound, ">=")
             }
             CardConstraint::LB(constr) => {
-                let (lits, bound) = constr.decompose();
-                (lits, bound as isize, ">=")
+                let (lits, bound) = constr.decompose_ref();
+                iter_b = lits.iter().copied();
+                (&mut iter_b, *bound as isize, ">=")
             }
             CardConstraint::EQ(constr) => {
-                let (lits, bound) = constr.decompose();
-                (lits, bound as isize, "=")
+                let (lits, bound) = constr.decompose_ref();
+                iter_b = lits.iter().copied();
+                (&mut iter_b, *bound as isize, "=")
             }
         };
         let mut offset = 0;
-        lits.into_iter().try_for_each(|l| {
+        for l in lits {
             if l.is_pos() {
-                write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx)
+                write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx)?;
             } else {
                 offset += 1;
-                write!(writer, "-1 x{} ", l.vidx32() + opts.first_var_idx)
+                write!(writer, "-1 x{} ", l.vidx32() + opts.first_var_idx)?;
             }
-        })?;
+        }
         writeln!(writer, "{} {};", op, bound - offset)
     } else {
-        let (lits, bound, op) = match card {
+        let (lits, bound, op): (&mut dyn Iterator<Item = Lit>, _, _) = match card {
             CardConstraint::UB(constr) => {
-                let (lits, bound) = constr.decompose();
-                let bound = lits.len() as isize - bound as isize;
+                let (lits, bound) = constr.decompose_ref();
+                let bound = lits.len() as isize - *bound as isize;
                 // Flip operator by negating literals
-                let lits: Vec<Lit> = lits.into_iter().map(|l| !l).collect();
-                (lits, bound, ">=")
+                iter_a = lits.iter().map(neg_lit);
+                (&mut iter_a, bound, ">=")
             }
             CardConstraint::LB(constr) => {
-                let (lits, bound) = constr.decompose();
-                (lits, bound as isize, ">=")
+                let (lits, bound) = constr.decompose_ref();
+                iter_b = lits.iter().copied();
+                (&mut iter_b, *bound as isize, ">=")
             }
             CardConstraint::EQ(constr) => {
-                let (lits, bound) = constr.decompose();
-                (lits, bound as isize, "=")
+                let (lits, bound) = constr.decompose_ref();
+                iter_b = lits.iter().copied();
+                (&mut iter_b, *bound as isize, "=")
             }
         };
-        lits.into_iter().try_for_each(|l| {
+        for l in lits {
             if l.is_pos() {
-                write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx)
+                write!(writer, "1 x{} ", l.vidx32() + opts.first_var_idx)?;
             } else {
-                write!(writer, "1 ~x{} ", l.vidx32() + opts.first_var_idx)
+                write!(writer, "1 ~x{} ", l.vidx32() + opts.first_var_idx)?;
             }
-        })?;
+        }
         writeln!(writer, "{} {};", op, bound)
     }
 }
 
 /// Writes a pseudo-boolean constraint to an OPB file
-fn write_pb<W: Write>(writer: &mut W, pb: PBConstraint, opts: Options) -> Result<(), io::Error> {
+fn write_pb<W: Write>(writer: &mut W, pb: &PBConstraint, opts: Options) -> Result<(), io::Error> {
+    let mut iter_a;
+    let mut iter_b;
+    let neg_lit = |(l, w): &(Lit, usize)| (!*l, *w);
     if opts.no_negated_lits {
-        let (lits, bound, op) = match pb {
+        let (lits, bound, op): (&mut dyn Iterator<Item = (Lit, usize)>, _, _) = match pb {
             PBConstraint::UB(constr) => {
-                let (lits, bound) = constr.decompose();
+                let (lits, bound) = constr.decompose_ref();
                 let weight_sum = lits.iter().fold(0, |sum, (_, w)| sum + w);
                 // Flip operator by negating literals
-                let lits = lits.into_iter().map(|(l, w)| (!l, w)).collect();
-                (lits, weight_sum as isize - bound, ">=")
+                iter_a = lits.iter().map(neg_lit);
+                (&mut iter_a, weight_sum as isize - bound, ">=")
             }
             PBConstraint::LB(constr) => {
-                let (lits, bound) = constr.decompose();
-                (lits, bound, ">=")
+                let (lits, bound) = constr.decompose_ref();
+                iter_b = lits.iter().copied();
+                (&mut iter_b, *bound, ">=")
             }
             PBConstraint::EQ(constr) => {
-                let (lits, bound) = constr.decompose();
-                (lits, bound, "=")
+                let (lits, bound) = constr.decompose_ref();
+                iter_b = lits.iter().copied();
+                (&mut iter_b, *bound, "=")
             }
         };
         let mut offset: isize = 0;
-        lits.into_iter().try_for_each(|(l, w)| {
+        for (l, w) in lits {
             if l.is_pos() {
-                write!(writer, "{} x{} ", w, l.vidx32() + opts.first_var_idx)
+                write!(writer, "{} x{} ", w, l.vidx32() + opts.first_var_idx)?;
             } else {
                 // TODO: consider returning error for usize -> isize cast
                 let w = w as isize;
                 offset += w;
-                write!(writer, "{} x{} ", -w, l.vidx32() + opts.first_var_idx)
+                write!(writer, "{} x{} ", -w, l.vidx32() + opts.first_var_idx)?;
             }
-        })?;
+        }
         writeln!(writer, "{} {};", op, bound - offset)
     } else {
-        let (lits, bound, op) = match pb {
+        let (lits, bound, op): (&mut dyn Iterator<Item = (Lit, usize)>, _, _) = match pb {
             PBConstraint::UB(constr) => {
-                let (lits, bound) = constr.decompose();
+                let (lits, bound) = constr.decompose_ref();
                 let weight_sum = lits.iter().fold(0, |sum, (_, w)| sum + w);
                 // Flip operator by negating literals
-                let lits = lits.into_iter().map(|(l, w)| (!l, w)).collect();
-                (lits, weight_sum as isize - bound, ">=")
+                iter_a = lits.iter().map(neg_lit);
+                (&mut iter_a, weight_sum as isize - bound, ">=")
             }
             PBConstraint::LB(constr) => {
-                let (lits, bound) = constr.decompose();
-                (lits, bound, ">=")
+                let (lits, bound) = constr.decompose_ref();
+                iter_b = lits.iter().copied();
+                (&mut iter_b, *bound, ">=")
             }
             PBConstraint::EQ(constr) => {
-                let (lits, bound) = constr.decompose();
-                (lits, bound, "=")
+                let (lits, bound) = constr.decompose_ref();
+                iter_b = lits.iter().copied();
+                (&mut iter_b, *bound, "=")
             }
         };
-        lits.into_iter().try_for_each(|(l, w)| {
+        for (l, w) in lits {
             if l.is_pos() {
-                write!(writer, "{} x{} ", w, l.vidx32() + opts.first_var_idx)
+                write!(writer, "{} x{} ", w, l.vidx32() + opts.first_var_idx)?;
             } else {
-                write!(writer, "{} ~x{} ", w, l.vidx32() + opts.first_var_idx)
+                write!(writer, "{} ~x{} ", w, l.vidx32() + opts.first_var_idx)?;
             }
-        })?;
+        }
         writeln!(writer, "{} {};", op, bound)
     }
 }
@@ -925,19 +916,19 @@ mod test {
 
         let mut cursor = Cursor::new(vec![]);
 
-        write_clause(&mut cursor, cl.clone(), Options::default()).unwrap();
+        write_clause(&mut cursor, &cl, Options::default()).unwrap();
 
         cursor.rewind().unwrap();
 
         let (cnf, _) = super::parse_sat::<_, BasicVarManager>(cursor, Options::default())
             .unwrap()
-            .as_cnf();
+            .into_cnf();
 
         assert_eq!(cnf.len(), 1);
         assert_eq!(cnf.into_iter().next().unwrap().normalize(), cl.normalize());
     }
 
-    fn write_parse_inst_test(in_inst: SatInstance, true_inst: SatInstance, opts: Options) {
+    fn write_parse_inst_test(in_inst: &SatInstance, true_inst: SatInstance, opts: Options) {
         let mut cursor = Cursor::new(vec![]);
 
         write_sat(&mut cursor, in_inst, opts).unwrap();
@@ -946,8 +937,8 @@ mod test {
 
         let parsed_inst: SatInstance = super::parse_sat(cursor, opts).unwrap();
 
-        let (parsed_cnf, parsed_vm) = parsed_inst.as_cnf();
-        let (true_cnf, true_vm) = true_inst.as_cnf();
+        let (parsed_cnf, parsed_vm) = parsed_inst.into_cnf();
+        let (true_cnf, true_vm) = true_inst.into_cnf();
 
         assert_eq!(parsed_vm, true_vm);
         assert_eq!(parsed_cnf.normalize(), true_cnf.normalize());
@@ -967,19 +958,19 @@ mod test {
         in_inst.add_card_constr(CardConstraint::new_ub(vec![!lit![3], lit![4], !lit![5]], 2));
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_ub(lits.clone(), 2));
-        write_parse_inst_test(in_inst, true_inst, Options::default());
+        write_parse_inst_test(&in_inst, true_inst, Options::default());
 
         let mut in_inst: SatInstance = SatInstance::new();
         in_inst.add_card_constr(CardConstraint::new_eq(vec![!lit![3], lit![4], !lit![5]], 2));
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_eq(lits.clone(), 2));
-        write_parse_inst_test(in_inst, true_inst, Options::default());
+        write_parse_inst_test(&in_inst, true_inst, Options::default());
 
         let mut in_inst: SatInstance = SatInstance::new();
         in_inst.add_card_constr(CardConstraint::new_lb(vec![!lit![3], lit![4], !lit![5]], 2));
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_lb(lits.clone(), 2));
-        write_parse_inst_test(in_inst, true_inst, Options::default());
+        write_parse_inst_test(&in_inst, true_inst, Options::default());
     }
 
     #[test]
@@ -992,26 +983,28 @@ mod test {
         // constraint as well.
         let lits = vec![(!lit![3], 1), (lit![4], 1), (!lit![5], 1)];
 
-        let mut alt_opb_opts = Options::default();
-        alt_opb_opts.no_negated_lits = false;
+        let alt_opb_opts = Options {
+            no_negated_lits: false,
+            ..Default::default()
+        };
 
         let mut in_inst: SatInstance = SatInstance::new();
         in_inst.add_card_constr(CardConstraint::new_ub(vec![!lit![3], lit![4], !lit![5]], 2));
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_ub(lits.clone(), 2));
-        write_parse_inst_test(in_inst, true_inst, alt_opb_opts);
+        write_parse_inst_test(&in_inst, true_inst, alt_opb_opts);
 
         let mut in_inst: SatInstance = SatInstance::new();
         in_inst.add_card_constr(CardConstraint::new_eq(vec![!lit![3], lit![4], !lit![5]], 2));
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_eq(lits.clone(), 2));
-        write_parse_inst_test(in_inst, true_inst, alt_opb_opts);
+        write_parse_inst_test(&in_inst, true_inst, alt_opb_opts);
 
         let mut in_inst: SatInstance = SatInstance::new();
         in_inst.add_card_constr(CardConstraint::new_lb(vec![!lit![3], lit![4], !lit![5]], 2));
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_lb(lits.clone(), 2));
-        write_parse_inst_test(in_inst, true_inst, alt_opb_opts);
+        write_parse_inst_test(&in_inst, true_inst, alt_opb_opts);
     }
 
     #[test]
@@ -1020,34 +1013,36 @@ mod test {
 
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_ub(lits.clone(), 2));
-        write_parse_inst_test(true_inst.clone(), true_inst, Options::default());
+        write_parse_inst_test(&true_inst, true_inst.clone(), Options::default());
 
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_eq(lits.clone(), 2));
-        write_parse_inst_test(true_inst.clone(), true_inst, Options::default());
+        write_parse_inst_test(&true_inst, true_inst.clone(), Options::default());
 
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_lb(lits.clone(), 2));
-        write_parse_inst_test(true_inst.clone(), true_inst, Options::default());
+        write_parse_inst_test(&true_inst, true_inst.clone(), Options::default());
     }
 
     #[test]
     fn write_parse_pb_neg_lits() {
         let lits = vec![(!lit![6], 3), (!lit![7], -5), (lit![8], 2), (lit![9], -4)];
 
-        let mut alt_opb_opts = Options::default();
-        alt_opb_opts.no_negated_lits = false;
+        let alt_opb_opts = Options {
+            no_negated_lits: false,
+            ..Default::default()
+        };
 
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_ub(lits.clone(), 2));
-        write_parse_inst_test(true_inst.clone(), true_inst, alt_opb_opts);
+        write_parse_inst_test(&true_inst, true_inst.clone(), alt_opb_opts);
 
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_eq(lits.clone(), 2));
-        write_parse_inst_test(true_inst.clone(), true_inst, alt_opb_opts);
+        write_parse_inst_test(&true_inst, true_inst.clone(), alt_opb_opts);
 
         let mut true_inst: SatInstance = SatInstance::new();
         true_inst.add_pb_constr(PBConstraint::new_lb(lits.clone(), 2));
-        write_parse_inst_test(true_inst.clone(), true_inst, alt_opb_opts);
+        write_parse_inst_test(&true_inst, true_inst.clone(), alt_opb_opts);
     }
 }
diff --git a/rustsat/src/instances/multiopt.rs b/rustsat/src/instances/multiopt.rs
index 53ed0aa3..4ebeb142 100644
--- a/rustsat/src/instances/multiopt.rs
+++ b/rustsat/src/instances/multiopt.rs
@@ -8,6 +8,7 @@ use crate::{
         constraints::{CardConstraint, PBConstraint},
         Assignment, Lit, Var, WClsIter, WLitIter,
     },
+    RequiresClausal, RequiresSoftLits,
 };
 
 use super::{
@@ -40,7 +41,7 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     pub fn compose(mut constraints: SatInstance<VM>, objectives: Vec<Objective>) -> Self {
         objectives.iter().for_each(|o| {
             if let Some(mv) = o.max_var() {
-                constraints.var_manager().increase_next_free(mv + 1);
+                constraints.var_manager_mut().increase_next_free(mv + 1);
             }
         });
         MultiOptInstance {
@@ -67,35 +68,67 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     }
 
     /// Gets a mutable reference to the hard constraints for modifying them
+    #[deprecated(
+        since = "0.5.0",
+        note = "get_constraints has been renamed to constraints_mut and will be removed in a future release"
+    )]
     pub fn get_constraints(&mut self) -> &mut SatInstance<VM> {
         &mut self.constrs
     }
 
+    /// Gets a mutable reference to the hard constraints for modifying them
+    pub fn constraints_mut(&mut self) -> &mut SatInstance<VM> {
+        &mut self.constrs
+    }
+
+    /// Gets a reference to the hard constraints
+    pub fn constraints_ref(&self) -> &SatInstance<VM> {
+        &self.constrs
+    }
+
     /// Reserves a new variable in the internal variable manager. This is a
     /// shortcut for `inst.get_constraints().var_manager().new_var()`.
     pub fn new_var(&mut self) -> Var {
-        self.get_constraints().var_manager().new_var()
+        self.constraints_mut().var_manager_mut().new_var()
     }
 
     /// Reserves a new variable in the internal variable manager. This is a
     /// shortcut for `inst.get_constraints().var_manager().new_lit()`.
     pub fn new_lit(&mut self) -> Lit {
-        self.get_constraints().var_manager().new_lit()
+        self.constraints_mut().var_manager_mut().new_lit()
     }
 
     /// Gets the used variable with the highest index. This is a shortcut
     /// for `inst.get_constraints().var_manager().max_var()`.
-    pub fn max_var(&mut self) -> Option<Var> {
-        self.get_constraints().var_manager().max_var()
+    pub fn max_var(&self) -> Option<Var> {
+        self.constraints_ref().var_manager_ref().max_var()
     }
 
     /// Gets a mutable reference to the first objective for modifying it.
     /// Make sure `obj_idx` does not exceed the number of objectives in the instance.
+    #[deprecated(
+        since = "0.5.0",
+        note = "get_objective has been renamed to objective_mut and will be removed in a future release"
+    )]
     pub fn get_objective(&mut self, obj_idx: usize) -> &mut Objective {
         assert!(obj_idx < self.objs.len());
         &mut self.objs[obj_idx]
     }
 
+    /// Gets a mutable reference to the objective with index `obj_idx` for modifying it.
+    /// Make sure `obj_idx` does not exceed the number of objectives in the instance.
+    pub fn objective_mut(&mut self, obj_idx: usize) -> &mut Objective {
+        assert!(obj_idx < self.objs.len());
+        &mut self.objs[obj_idx]
+    }
+
+    /// Gets a reference to the objective with index `obj_idx`.
+    /// Make sure `obj_idx` does not exceed the number of objectives in the instance.
+    pub fn objective_ref(&self, obj_idx: usize) -> &Objective {
+        assert!(obj_idx < self.objs.len());
+        &self.objs[obj_idx]
+    }
+
     /// Returns an iterator over references to the objectives
     pub fn iter_obj(&self) -> impl Iterator<Item = &Objective> {
         self.objs.iter()
@@ -107,8 +140,17 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     }
 
     /// Converts the instance to a set of hard and soft clauses
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_hard_cls_soft_cls has been renamed to into_hard_cls_soft_cls and will be removed in a future release"
+    )]
     pub fn as_hard_cls_soft_cls(self) -> (Cnf, Vec<(impl WClsIter, isize)>, VM) {
-        let (cnf, mut vm) = self.constrs.as_cnf();
+        self.into_hard_cls_soft_cls()
+    }
+
+    /// Converts the instance to a set of hard and soft clauses
+    pub fn into_hard_cls_soft_cls(self) -> (Cnf, Vec<(impl WClsIter, isize)>, VM) {
+        let (cnf, mut vm) = self.constrs.into_cnf();
         let omv = self.objs.iter().fold(Var::new(0), |v, o| {
             if let Some(mv) = o.max_var() {
                 return std::cmp::max(v, mv);
@@ -116,13 +158,22 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
             v
         });
         vm.increase_next_free(omv + 1);
-        let soft_cls = self.objs.into_iter().map(|o| o.as_soft_cls()).collect();
+        let soft_cls = self.objs.into_iter().map(|o| o.into_soft_cls()).collect();
         (cnf, soft_cls, vm)
     }
 
     /// Converts the instance to a set of hard clauses and soft literals
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_hard_cls_soft_lits has been renamed to into_hard_cls_soft_lits and will be removed in a future release"
+    )]
     pub fn as_hard_cls_soft_lits(self) -> (Cnf, Vec<(impl WLitIter, isize)>, VM) {
-        let (mut cnf, mut vm) = self.constrs.as_cnf();
+        self.into_hard_cls_soft_lits()
+    }
+
+    /// Converts the instance to a set of hard clauses and soft literals
+    pub fn into_hard_cls_soft_lits(self) -> (Cnf, Vec<(impl WLitIter, isize)>, VM) {
+        let (mut cnf, mut vm) = self.constrs.into_cnf();
         let omv = self.objs.iter().fold(Var::new(0), |v, o| {
             if let Some(mv) = o.max_var() {
                 return std::cmp::max(v, mv);
@@ -134,7 +185,7 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
             .objs
             .into_iter()
             .map(|o| {
-                let (hards, softs) = o.as_soft_lits(&mut vm);
+                let (hards, softs) = o.into_soft_lits(&mut vm);
                 cnf.extend(hards);
                 softs
             })
@@ -182,13 +233,17 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     /// # Performance
     ///
     /// For performance, consider using a [`std::io::BufWriter`] instance.
+    #[deprecated(since = "0.5.0", note = "use write_dimacs_path instead")]
     pub fn to_dimacs_path<P: AsRef<Path>>(self, path: P) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        #[allow(deprecated)]
         self.to_dimacs(&mut writer)
     }
 
     /// Write to DIMACS MCNF
+    #[deprecated(since = "0.5.0", note = "use write_dimacs instead")]
     pub fn to_dimacs<W: io::Write>(self, writer: &mut W) -> Result<(), io::Error> {
+        #[allow(deprecated)]
         self.to_dimacs_with_encoders(
             card::default_encode_cardinality_constraint,
             pb::default_encode_pb_constraint,
@@ -198,6 +253,10 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
 
     /// Writes the instance to DIMACS MCNF converting non-clausal constraints
     /// with specific encoders.
+    #[deprecated(
+        since = "0.5.0",
+        note = "use convert_to_cnf_with_encoders and write_dimacs instead"
+    )]
     pub fn to_dimacs_with_encoders<W, CardEnc, PBEnc>(
         self,
         card_encoder: CardEnc,
@@ -209,9 +268,57 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
         CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars),
         PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars),
     {
-        let (cnf, vm) = self.constrs.as_cnf_with_encoders(card_encoder, pb_encoder);
-        let soft_cls = self.objs.into_iter().map(|o| o.as_soft_cls()).collect();
-        fio::dimacs::write_mcnf_annotated(writer, cnf, soft_cls, vm.max_var())
+        let (cnf, vm) = self
+            .constrs
+            .into_cnf_with_encoders(card_encoder, pb_encoder);
+        let soft_cls = self.objs.into_iter().map(|o| o.into_soft_cls());
+        fio::dimacs::write_mcnf_annotated(writer, &cnf, soft_cls, Some(vm.n_used()))
+    }
+
+    /// Writes the instance to a DIMACS MCNF file at a path
+    ///
+    /// This requires that the instance is clausal, i.e., does not contain any non-converted
+    /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by
+    /// [`SatInstance::convert_to_cnf`] or [`SatInstance::convert_to_cnf_with_encoders`] first.
+    ///
+    /// # Errors
+    ///
+    /// - If the instance is not clausal, returns [`NonClausal`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_dimacs_path<P: AsRef<Path>>(&self, path: P) -> anyhow::Result<()> {
+        let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        self.write_dimacs(&mut writer)
+    }
+
+    /// Write to DIMACS MCNF
+    ///
+    /// This requires that the instance is clausal, i.e., does not contain any non-converted
+    /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by
+    /// [`SatInstance::convert_to_cnf`] or [`SatInstance::convert_to_cnf_with_encoders`] first.
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
+    ///
+    /// # Errors
+    ///
+    /// - If the instance is not clausal, returns [`NonClausal`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_dimacs<W: io::Write>(&self, writer: &mut W) -> anyhow::Result<()> {
+        if self.constrs.n_cards() > 0 || self.constrs.n_pbs() > 0 {
+            return Err(RequiresClausal.into());
+        }
+        let n_vars = self.constrs.n_vars();
+        let iter = self.objs.iter().map(|o| {
+            let offset = o.offset();
+            (o.iter_soft_cls(), offset)
+        });
+        Ok(fio::dimacs::write_mcnf_annotated(
+            writer,
+            &self.constrs.cnf,
+            iter,
+            Some(n_vars),
+        )?)
     }
 
     /// Writes the instance to an OPB file at a path
@@ -219,22 +326,87 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     /// # Performance
     ///
     /// For performance, consider using a [`std::io::BufWriter`] instance.
+    #[deprecated(since = "0.5.0", note = "use write_opb_path instead")]
     pub fn to_opb_path<P: AsRef<Path>>(
         self,
         path: P,
         opts: fio::opb::Options,
     ) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        #[allow(deprecated)]
         self.to_opb(&mut writer, opts)
     }
 
     /// Writes the instance to an OPB file
+    #[deprecated(since = "0.5.0", note = "use write_opb instead")]
     pub fn to_opb<W: io::Write>(
-        self,
+        mut self,
         writer: &mut W,
         opts: fio::opb::Options,
     ) -> Result<(), io::Error> {
-        fio::opb::write_multi_opt::<W, VM>(writer, self, opts)
+        for obj in &mut self.objs {
+            let vm = self.constrs.var_manager_mut();
+            let hardened = obj.convert_to_soft_lits(vm);
+            self.constrs.cnf.extend(hardened);
+        }
+        let objs = self.objs.iter().map(|o| {
+            let offset = o.offset();
+            (o.iter_soft_lits().unwrap(), offset)
+        });
+        fio::opb::write_multi_opt::<W, VM, _, _>(writer, &self.constrs, objs, opts)
+    }
+
+    /// Writes the instance to an OPB file at a path
+    ///
+    /// This requires that the objective does not contain soft clauses. If it does, use
+    /// [`Objective::convert_to_soft_lits`] first.
+    ///
+    /// # Errors
+    ///
+    /// - If the objective containes soft literals, returns [`RequiresSoftLits`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_opb_path<P: AsRef<Path>>(
+        &self,
+        path: P,
+        opts: fio::opb::Options,
+    ) -> anyhow::Result<()> {
+        let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        self.write_opb(&mut writer, opts)
+    }
+
+    /// Writes the instance to an OPB file
+    ///
+    /// This requires that the objective does not contain soft clauses. If it does, use
+    /// [`Objective::convert_to_soft_lits`] first.
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance(crate).
+    ///
+    /// # Errors
+    ///
+    /// - If the objective containes soft literals, returns [`RequiresSoftLits`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_opb<W: io::Write>(
+        &self,
+        writer: &mut W,
+        opts: fio::opb::Options,
+    ) -> anyhow::Result<()> {
+        let objs: Result<Vec<_>, RequiresSoftLits> = self
+            .objs
+            .iter()
+            .map(|o| {
+                let offset = o.offset();
+                Ok((o.iter_soft_lits()?, offset))
+            })
+            .collect();
+        let objs = objs?;
+        Ok(fio::opb::write_multi_opt::<W, VM, _, _>(
+            writer,
+            &self.constrs,
+            objs.into_iter(),
+            opts,
+        )?)
     }
 
     /// Calculates the objective values of an assignment. Returns [`None`] if the
@@ -283,7 +455,7 @@ impl<VM: ManageVars + Default> MultiOptInstance<VM> {
     /// positive number preceded by an 'o', indicating what objective this soft
     /// clause belongs to. After that, the format is identical to a soft clause
     /// in a WCNF file.
-    pub fn from_dimacs<R: io::Read>(reader: R) -> anyhow::Result<Self> {
+    pub fn from_dimacs<R: io::BufRead>(reader: R) -> anyhow::Result<Self> {
         fio::dimacs::parse_mcnf(reader)
     }
 
@@ -302,7 +474,7 @@ impl<VM: ManageVars + Default> MultiOptInstance<VM> {
     /// pseudo-boolean optimization instances with multiple objectives defined.
     /// For details on the file format see
     /// [here](https://www.cril.univ-artois.fr/PB12/format.pdf).
-    pub fn from_opb<R: io::Read>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+    pub fn from_opb<R: io::BufRead>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
         fio::opb::parse_multi_opt(reader, opts)
     }
 
@@ -321,12 +493,12 @@ impl<VM: ManageVars + Default> FromIterator<McnfLine> for MultiOptInstance<VM> {
         for line in iter {
             match line {
                 McnfLine::Comment(_) => (),
-                McnfLine::Hard(cl) => inst.get_constraints().add_clause(cl),
+                McnfLine::Hard(cl) => inst.constraints_mut().add_clause(cl),
                 McnfLine::Soft(cl, w, oidx) => {
                     if oidx >= inst.objs.len() {
                         inst.objs.resize(oidx + 1, Default::default())
                     }
-                    inst.get_objective(oidx).add_soft_clause(w, cl);
+                    inst.objective_mut(oidx).add_soft_clause(w, cl);
                 }
             }
         }
diff --git a/rustsat/src/instances/opt.rs b/rustsat/src/instances/opt.rs
index 84bbd64c..9c6e6193 100644
--- a/rustsat/src/instances/opt.rs
+++ b/rustsat/src/instances/opt.rs
@@ -1,6 +1,6 @@
 //! # Optimization Instance Representations
 
-use std::{cmp, io, path::Path};
+use std::{cmp, collections::hash_map, io, path::Path, slice};
 
 use crate::{
     clause,
@@ -9,6 +9,7 @@ use crate::{
         constraints::{CardConstraint, PBConstraint},
         Assignment, Clause, ClsIter, Lit, LitIter, RsHashMap, TernaryVal, Var, WClsIter, WLitIter,
     },
+    RequiresClausal, RequiresSoftLits,
 };
 
 /// Internal objective type for not exposing variants
@@ -305,10 +306,10 @@ impl Objective {
                 if let Some(unit_weight) = unit_weight {
                     *self = IntObj::Weighted {
                         offset: *offset,
-                        soft_lits: soft_lits.iter_mut().map(|l| (*l, *unit_weight)).collect(),
+                        soft_lits: soft_lits.drain(..).map(|l| (l, *unit_weight)).collect(),
                         soft_clauses: soft_clauses
-                            .iter_mut()
-                            .map(|cl| (cl.clone(), *unit_weight))
+                            .drain(..)
+                            .map(|cl| (cl, *unit_weight))
                             .collect(),
                     }
                     .into()
@@ -335,12 +336,12 @@ impl Objective {
             } => {
                 let mut soft_unit_lits = vec![];
                 soft_lits
-                    .iter_mut()
-                    .for_each(|(l, w)| soft_unit_lits.resize(soft_unit_lits.len() + *w, *l));
+                    .drain()
+                    .for_each(|(l, w)| soft_unit_lits.resize(soft_unit_lits.len() + w, l));
                 let mut soft_unit_clauses = vec![];
-                soft_clauses.iter_mut().for_each(|(cl, w)| {
-                    soft_unit_clauses.resize(soft_unit_clauses.len() + *w, cl.clone())
-                });
+                soft_clauses
+                    .drain()
+                    .for_each(|(cl, w)| soft_unit_clauses.resize(soft_unit_clauses.len() + w, cl));
                 *self = IntObj::Unweighted {
                     offset: *offset,
                     unit_weight: Some(1),
@@ -547,7 +548,16 @@ impl Objective {
     }
 
     /// Converts the objective to a set of soft clauses and an offset
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_soft_cls has been renamed to into_soft_cls and will be removed in a future release"
+    )]
     pub fn as_soft_cls(self) -> (impl WClsIter, isize) {
+        self.into_soft_cls()
+    }
+
+    /// Converts the objective to a set of soft clauses and an offset
+    pub fn into_soft_cls(self) -> (impl WClsIter, isize) {
         match self.0 {
             IntObj::Unweighted {
                 mut soft_clauses,
@@ -583,7 +593,18 @@ impl Objective {
     /// Converts the objective to unweighted soft clauses, a unit weight and an offset. If the
     /// objective is weighted, the soft clause will appear as often as its
     /// weight in the output vector.
-    pub fn as_unweighted_soft_cls(mut self) -> (impl ClsIter, usize, isize) {
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_unweighted_soft_cls has been renamed to into_unweighted_soft_cls and will be removed in a future release"
+    )]
+    pub fn as_unweighted_soft_cls(self) -> (impl ClsIter, usize, isize) {
+        self.into_unweighted_soft_cls()
+    }
+
+    /// Converts the objective to unweighted soft clauses, a unit weight and an offset. If the
+    /// objective is weighted, the soft clause will appear as often as its
+    /// weight in the output vector.
+    pub fn into_unweighted_soft_cls(mut self) -> (impl ClsIter, usize, isize) {
         self.weighted_2_unweighted();
         match self.0 {
             IntObj::Weighted { .. } => panic!(),
@@ -606,33 +627,79 @@ impl Objective {
         }
     }
 
+    /// Converts the objective to soft literals in place, returning hardened clauses produced in
+    /// the conversion.
+    ///
+    /// See [`Self::into_soft_lits`] if you do not need to convert in place.
+    pub fn convert_to_soft_lits<VM>(&mut self, var_manager: &mut VM) -> Cnf
+    where
+        VM: ManageVars,
+    {
+        let mut cnf = Cnf::new();
+        match &mut self.0 {
+            IntObj::Weighted {
+                soft_lits,
+                soft_clauses,
+                ..
+            } => {
+                cnf.clauses.reserve(soft_clauses.len());
+                soft_lits.reserve(soft_clauses.len());
+                for (mut cl, w) in soft_clauses.drain() {
+                    debug_assert!(cl.len() > 1);
+                    let relax_lit = var_manager.new_var().pos_lit();
+                    cl.add(relax_lit);
+                    cnf.add_clause(cl);
+                    soft_lits.insert(relax_lit, w);
+                }
+            }
+            IntObj::Unweighted {
+                soft_lits,
+                soft_clauses,
+                ..
+            } => {
+                cnf.clauses.reserve(soft_clauses.len());
+                soft_lits.reserve(soft_clauses.len());
+                for mut cl in soft_clauses.drain(..) {
+                    debug_assert!(cl.len() > 1);
+                    let relax_lit = var_manager.new_var().pos_lit();
+                    cl.add(relax_lit);
+                    cnf.add_clause(cl);
+                    soft_lits.push(relax_lit);
+                }
+            }
+        }
+        cnf
+    }
+
     /// Converts the objective to a set of hard clauses, soft literals and an offset
-    pub fn as_soft_lits<VM>(mut self, var_manager: &mut VM) -> (Cnf, (impl WLitIter, isize))
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_soft_lits has been renamed to into_soft_lits and will be removed in a future release"
+    )]
+    pub fn as_soft_lits<VM>(self, var_manager: &mut VM) -> (Cnf, (impl WLitIter, isize))
     where
         VM: ManageVars,
     {
+        self.into_soft_lits(var_manager)
+    }
+
+    /// Converts the objective to a set of hard clauses, soft literals and an offset
+    ///
+    /// See [`Self::convert_to_soft_lits`] for converting in place
+    pub fn into_soft_lits<VM>(mut self, var_manager: &mut VM) -> (Cnf, (impl WLitIter, isize))
+    where
+        VM: ManageVars,
+    {
+        let cnf = self.convert_to_soft_lits(var_manager);
         self.unweighted_2_weighted();
         match self.0 {
-            IntObj::Unweighted { .. } => panic!(),
+            IntObj::Unweighted { .. } => unreachable!(),
             IntObj::Weighted {
-                mut soft_lits,
+                soft_lits,
                 soft_clauses,
                 offset,
             } => {
-                let mut cnf = Cnf::new();
-                cnf.clauses.reserve(soft_clauses.len());
-                soft_lits.reserve(soft_clauses.len());
-                for (mut cl, w) in soft_clauses {
-                    if cl.len() > 1 {
-                        let relax_lit = var_manager.new_var().pos_lit();
-                        cl.add(relax_lit);
-                        cnf.add_clause(cl);
-                        soft_lits.insert(relax_lit, w);
-                    } else {
-                        assert!(cl.len() == 1);
-                        soft_lits.insert(!cl[0], w);
-                    }
-                }
+                debug_assert!(soft_clauses.is_empty());
                 (cnf, (soft_lits, offset))
             }
         }
@@ -641,6 +708,10 @@ impl Objective {
     /// Converts the objective to hard clauses, unweighted soft literals, a unit
     /// weight and an offset. If the objective is weighted, the soft literals
     /// will appear as often as its weight in the output vector.
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_unweighted_soft_lits has been renamed to into_unweighted_soft_lits and will be removed in a future release"
+    )]
     pub fn as_unweighted_soft_lits<VM>(
         self,
         var_manager: &mut VM,
@@ -648,37 +719,41 @@ impl Objective {
     where
         VM: ManageVars,
     {
+        self.into_unweighted_soft_lits(var_manager)
+    }
+
+    /// Converts the objective to hard clauses, unweighted soft literals, a unit
+    /// weight and an offset. If the objective is weighted, the soft literals
+    /// will appear as often as its weight in the output vector.
+    pub fn into_unweighted_soft_lits<VM>(
+        mut self,
+        var_manager: &mut VM,
+    ) -> (Cnf, impl LitIter, usize, isize)
+    where
+        VM: ManageVars,
+    {
+        let cnf = self.convert_to_soft_lits(var_manager);
         match self.0 {
-            IntObj::Weighted { .. } => {
-                let (cnf, softs) = self.as_soft_lits(var_manager);
+            IntObj::Weighted {
+                soft_lits,
+                soft_clauses,
+                offset,
+            } => {
+                debug_assert!(soft_clauses.is_empty());
                 let mut soft_unit_lits = vec![];
-                softs
-                    .0
+                soft_lits
                     .into_iter()
                     .for_each(|(l, w)| soft_unit_lits.resize(soft_unit_lits.len() + w, l));
-                (cnf, soft_unit_lits, 1, softs.1)
+                (cnf, soft_unit_lits, 1, offset)
             }
             IntObj::Unweighted {
                 offset,
                 unit_weight,
-                mut soft_lits,
+                soft_lits,
                 soft_clauses,
             } => {
+                debug_assert!(soft_clauses.is_empty());
                 if let Some(unit_weight) = unit_weight {
-                    let mut cnf = Cnf::new();
-                    cnf.clauses.reserve(soft_clauses.len());
-                    soft_lits.reserve(soft_clauses.len());
-                    for mut cl in soft_clauses {
-                        if cl.len() > 1 {
-                            let relax_lit = var_manager.new_var().pos_lit();
-                            cl.add(relax_lit);
-                            cnf.add_clause(cl);
-                            soft_lits.push(relax_lit);
-                        } else {
-                            assert!(cl.len() == 1);
-                            soft_lits.push(!cl[0]);
-                        }
-                    }
                     (cnf, soft_lits, unit_weight, offset)
                 } else {
                     (Cnf::new(), vec![], 1, offset)
@@ -813,6 +888,94 @@ impl Objective {
         };
         self
     }
+
+    /// Gets a weighted literal iterator over only the soft literals
+    ///
+    /// # Errors
+    ///
+    /// If the objective contains soft clauses that this iterator would miss, returns
+    /// [`RequiresSoftLits`]
+    pub fn iter_soft_lits(&self) -> Result<impl WLitIter + '_, RequiresSoftLits> {
+        if self.n_clauses() > 0 {
+            return Err(RequiresSoftLits);
+        }
+        Ok(match &self.0 {
+            IntObj::Weighted { soft_lits, .. } => ObjSoftLitIter::Weighted(soft_lits.iter()),
+            IntObj::Unweighted {
+                soft_lits,
+                unit_weight,
+                ..
+            } => ObjSoftLitIter::Unweighted(soft_lits.iter(), unit_weight.unwrap_or(0)),
+        })
+    }
+
+    /// Gets an iterator over the entire objective as soft clauses
+    pub fn iter_soft_cls(&self) -> impl WClsIter + '_ {
+        match &self.0 {
+            IntObj::Weighted {
+                soft_lits,
+                soft_clauses,
+                ..
+            } => ObjSoftClauseIter::Weighted(soft_lits.iter(), soft_clauses.iter()),
+            IntObj::Unweighted {
+                unit_weight,
+                soft_lits,
+                soft_clauses,
+                ..
+            } => ObjSoftClauseIter::Unweighted(
+                soft_lits.iter(),
+                soft_clauses.iter(),
+                unit_weight.unwrap_or(0),
+            ),
+        }
+    }
+}
+
+/// A wrapper type for iterators over soft literals in an objective
+enum ObjSoftLitIter<'a> {
+    Weighted(hash_map::Iter<'a, Lit, usize>),
+    Unweighted(slice::Iter<'a, Lit>, usize),
+}
+
+impl Iterator for ObjSoftLitIter<'_> {
+    type Item = (Lit, usize);
+
+    fn next(&mut self) -> Option<Self::Item> {
+        match self {
+            ObjSoftLitIter::Weighted(iter) => iter.next().map(|(&l, &w)| (l, w)),
+            ObjSoftLitIter::Unweighted(iter, w) => iter.next().map(|&l| (l, *w)),
+        }
+    }
+}
+
+/// A wrapper type for iterators over soft clauses in an objective
+enum ObjSoftClauseIter<'a> {
+    Weighted(
+        hash_map::Iter<'a, Lit, usize>,
+        hash_map::Iter<'a, Clause, usize>,
+    ),
+    Unweighted(slice::Iter<'a, Lit>, slice::Iter<'a, Clause>, usize),
+}
+
+impl Iterator for ObjSoftClauseIter<'_> {
+    type Item = (Clause, usize);
+
+    fn next(&mut self) -> Option<Self::Item> {
+        match self {
+            ObjSoftClauseIter::Weighted(lit_iter, cl_iter) => {
+                if let Some((&l, &w)) = lit_iter.next() {
+                    return Some((clause![!l], w));
+                }
+                cl_iter.next().map(|(cl, &w)| (cl.clone(), w))
+            }
+            ObjSoftClauseIter::Unweighted(lit_iter, cl_iter, w) => {
+                if let Some(&l) = lit_iter.next() {
+                    return Some((clause![!l], *w));
+                }
+                cl_iter.next().map(|cl| (cl.clone(), *w))
+            }
+        }
+    }
 }
 
 impl FromIterator<(Lit, usize)> for Objective {
@@ -865,7 +1028,7 @@ impl<VM: ManageVars> OptInstance<VM> {
     /// Creates a new optimization instance from constraints and an objective
     pub fn compose(mut constraints: SatInstance<VM>, objective: Objective) -> Self {
         if let Some(mv) = objective.max_var() {
-            constraints.var_manager().increase_next_free(mv);
+            constraints.var_manager_mut().increase_next_free(mv);
         }
         OptInstance {
             constrs: constraints,
@@ -876,57 +1039,85 @@ impl<VM: ManageVars> OptInstance<VM> {
     /// Decomposes the optimization instance to a [`SatInstance`] and an [`Objective`]
     pub fn decompose(mut self) -> (SatInstance<VM>, Objective) {
         if let Some(mv) = self.obj.max_var() {
-            self.constrs.var_manager.increase_next_free(mv + 1);
+            self.constrs.var_manager_mut().increase_next_free(mv + 1);
         }
         (self.constrs, self.obj)
     }
 
     /// Gets a mutable reference to the hard constraints for modifying them
+    #[deprecated(
+        since = "0.5.0",
+        note = "get_constraints has been renamed to constraints_mut and will be removed in a future release"
+    )]
     pub fn get_constraints(&mut self) -> &mut SatInstance<VM> {
         &mut self.constrs
     }
 
+    /// Gets a mutable reference to the hard constraints for modifying them
+    pub fn constraints_mut(&mut self) -> &mut SatInstance<VM> {
+        &mut self.constrs
+    }
+
+    /// Gets a reference to the hard constraints
+    pub fn constraints_ref(&self) -> &SatInstance<VM> {
+        &self.constrs
+    }
+
     /// Gets a mutable reference to the objective for modifying it
+    #[deprecated(
+        since = "0.5.0",
+        note = "get_objective has been renamed to objective_mut and will be removed in a future release"
+    )]
     pub fn get_objective(&mut self) -> &mut Objective {
         &mut self.obj
     }
 
+    /// Gets a mutable reference to the objective for modifying it
+    pub fn objective_mut(&mut self) -> &mut Objective {
+        &mut self.obj
+    }
+
+    /// Gets a reference to the objective
+    pub fn objective_ref(&self) -> &Objective {
+        &self.obj
+    }
+
     /// Reserves a new variable in the internal variable manager. This is a
     /// shortcut for `inst.get_constraints().var_manager().new_var()`.
     pub fn new_var(&mut self) -> Var {
-        self.get_constraints().var_manager().new_var()
+        self.constraints_mut().var_manager_mut().new_var()
     }
 
     /// Reserves a new variable in the internal variable manager. This is a
     /// shortcut for `inst.get_constraints().var_manager().new_lit()`.
     pub fn new_lit(&mut self) -> Lit {
-        self.get_constraints().var_manager().new_lit()
+        self.constraints_mut().var_manager_mut().new_lit()
     }
 
     /// Gets the used variable with the highest index. This is a shortcut
     /// for `inst.get_constraints().var_manager().max_var()`.
-    pub fn max_var(&mut self) -> Option<Var> {
-        self.get_constraints().var_manager().max_var()
+    pub fn max_var(&self) -> Option<Var> {
+        self.constraints_ref().var_manager_ref().max_var()
     }
 
     /// Converts the instance to a set of hard and soft clauses, an objective
     /// offset and a variable manager
-    pub fn as_hard_cls_soft_cls(self) -> (Cnf, (impl WClsIter, isize), VM) {
-        let (cnf, mut vm) = self.constrs.as_cnf();
+    pub fn into_hard_cls_soft_cls(self) -> (Cnf, (impl WClsIter, isize), VM) {
+        let (cnf, mut vm) = self.constrs.into_cnf();
         if let Some(mv) = self.obj.max_var() {
             vm.increase_next_free(mv + 1);
         }
-        (cnf, self.obj.as_soft_cls(), vm)
+        (cnf, self.obj.into_soft_cls(), vm)
     }
 
     /// Converts the instance to a set of hard clauses and soft literals, an
     /// objective offset and a variable manager
-    pub fn as_hard_cls_soft_lits(self) -> (Cnf, (impl WLitIter, isize), VM) {
-        let (mut cnf, mut vm) = self.constrs.as_cnf();
+    pub fn into_hard_cls_soft_lits(self) -> (Cnf, (impl WLitIter, isize), VM) {
+        let (mut cnf, mut vm) = self.constrs.into_cnf();
         if let Some(mv) = self.obj.max_var() {
             vm.increase_next_free(mv + 1);
         }
-        let (hard_softs, softs) = self.obj.as_soft_lits(&mut vm);
+        let (hard_softs, softs) = self.obj.into_soft_lits(&mut vm);
         cnf.extend(hard_softs);
         (cnf, softs, vm)
     }
@@ -967,13 +1158,17 @@ impl<VM: ManageVars> OptInstance<VM> {
     /// # Performance
     ///
     /// For performance, consider using a [`std::io::BufWriter`] instance.
+    #[deprecated(since = "0.5.0", note = "use write_dimacs_path instead")]
     pub fn to_dimacs_path<P: AsRef<Path>>(self, path: P) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        #[allow(deprecated)]
         self.to_dimacs(&mut writer)
     }
 
     /// Write to DIMACS WCNF (post 22)
+    #[deprecated(since = "0.5.0", note = "use write_dimacs instead")]
     pub fn to_dimacs<W: io::Write>(self, writer: &mut W) -> Result<(), io::Error> {
+        #[allow(deprecated)]
         self.to_dimacs_with_encoders(
             card::default_encode_cardinality_constraint,
             pb::default_encode_pb_constraint,
@@ -983,6 +1178,10 @@ impl<VM: ManageVars> OptInstance<VM> {
 
     /// Writes the instance to DIMACS WCNF (post 22) converting non-clausal
     /// constraints with specific encoders.
+    #[deprecated(
+        since = "0.5.0",
+        note = "use convert_to_cnf_with_encoders and write_dimacs instead"
+    )]
     pub fn to_dimacs_with_encoders<W, CardEnc, PBEnc>(
         self,
         card_encoder: CardEnc,
@@ -994,9 +1193,55 @@ impl<VM: ManageVars> OptInstance<VM> {
         CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars),
         PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars),
     {
-        let (cnf, vm) = self.constrs.as_cnf_with_encoders(card_encoder, pb_encoder);
-        let soft_cls = self.obj.as_soft_cls();
-        fio::dimacs::write_wcnf_annotated(writer, cnf, soft_cls, vm.max_var())
+        let (cnf, vm) = self
+            .constrs
+            .into_cnf_with_encoders(card_encoder, pb_encoder);
+        let soft_cls = self.obj.into_soft_cls();
+        fio::dimacs::write_wcnf_annotated(writer, &cnf, soft_cls, Some(vm.n_used()))
+    }
+
+    /// Writes the instance to a DIMACS WCNF file at a path
+    ///
+    /// This requires that the instance is clausal, i.e., does not contain any non-converted
+    /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by
+    /// [`SatInstance::convert_to_cnf`] or [`SatInstance::convert_to_cnf_with_encoders`] first.
+    ///
+    /// # Errors
+    ///
+    /// - If the instance is not clausal, returns [`NonClausal`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_dimacs_path<P: AsRef<Path>>(&self, path: P) -> anyhow::Result<()> {
+        let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        self.write_dimacs(&mut writer)
+    }
+
+    /// Write to DIMACS WCNF (post 22)
+    ///
+    /// This requires that the instance is clausal, i.e., does not contain any non-converted
+    /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by
+    /// [`SatInstance::convert_to_cnf`] or [`SatInstance::convert_to_cnf_with_encoders`] first.
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
+    ///
+    /// # Errors
+    ///
+    /// - If the instance is not clausal, returns [`NonClausal`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_dimacs<W: io::Write>(&self, writer: &mut W) -> anyhow::Result<()> {
+        if self.constrs.n_cards() > 0 || self.constrs.n_pbs() > 0 {
+            return Err(RequiresClausal.into());
+        }
+        let n_vars = self.constrs.n_vars();
+        let offset = self.obj.offset();
+        let soft_cls = self.obj.iter_soft_cls();
+        Ok(fio::dimacs::write_wcnf_annotated(
+            writer,
+            &self.constrs.cnf,
+            (soft_cls, offset),
+            Some(n_vars),
+        )?)
     }
 
     /// Writes the instance to an OPB file at a path
@@ -1004,22 +1249,75 @@ impl<VM: ManageVars> OptInstance<VM> {
     /// # Performance
     ///
     /// For performance, consider using a [`std::io::BufWriter`] instance.
+    #[deprecated(since = "0.5.0", note = "use write_opb_path instead")]
     pub fn to_opb_path<P: AsRef<Path>>(
         self,
         path: P,
         opts: fio::opb::Options,
     ) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        #[allow(deprecated)]
         self.to_opb(&mut writer, opts)
     }
 
     /// Writes the instance to an OPB file
+    #[deprecated(since = "0.5.0", note = "use write_opb instead")]
     pub fn to_opb<W: io::Write>(
-        self,
+        mut self,
         writer: &mut W,
         opts: fio::opb::Options,
     ) -> Result<(), io::Error> {
-        fio::opb::write_opt::<W, VM>(writer, self, opts)
+        let var_manager = self.constrs.var_manager_mut();
+        self.obj.convert_to_soft_lits(var_manager);
+        let offset = self.obj.offset();
+        let iter = self.obj.iter_soft_lits().unwrap();
+        fio::opb::write_opt::<W, VM, _>(writer, &self.constrs, (iter, offset), opts)
+    }
+
+    /// Writes the instance to an OPB file at a path
+    ///
+    /// This requires that the objective does not contain soft clauses. If it does, use
+    /// [`Objective::convert_to_soft_lits`] first.
+    ///
+    /// # Errors
+    ///
+    /// - If the objective containes soft literals, returns [`RequiresSoftLits`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_opb_path<P: AsRef<Path>>(
+        &self,
+        path: P,
+        opts: fio::opb::Options,
+    ) -> anyhow::Result<()> {
+        let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        self.write_opb(&mut writer, opts)
+    }
+
+    /// Writes the instance to an OPB file
+    ///
+    /// This requires that the objective does not contain soft clauses. If it does, use
+    /// [`Objective::convert_to_soft_lits`] first.
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance(crate).
+    ///
+    /// # Errors
+    ///
+    /// - If the objective containes soft literals, returns [`RequiresSoftLits`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_opb<W: io::Write>(
+        &self,
+        writer: &mut W,
+        opts: fio::opb::Options,
+    ) -> anyhow::Result<()> {
+        let offset = self.obj.offset();
+        let iter = self.obj.iter_soft_lits()?;
+        Ok(fio::opb::write_opt::<W, VM, _>(
+            writer,
+            &self.constrs,
+            (iter, offset),
+            opts,
+        )?)
     }
 
     /// Calculates the objective value of an assignment. Returns [`None`] if the
@@ -1053,14 +1351,14 @@ impl<VM: ManageVars + Default> OptInstance<VM> {
     ///
     /// If a DIMACS MCNF file is passed to this function, all objectives but the
     /// first are ignored.
-    pub fn from_dimacs<R: io::Read>(reader: R) -> anyhow::Result<Self> {
+    pub fn from_dimacs<R: io::BufRead>(reader: R) -> anyhow::Result<Self> {
         Self::from_dimacs_with_idx(reader, 0)
     }
 
     /// Parses a DIMACS instance from a reader object, selecting the objective
     /// with index `obj_idx` if multiple are available. The index starts at 0.
     /// For more details see [`OptInstance::from_dimacs`].
-    pub fn from_dimacs_with_idx<R: io::Read>(reader: R, obj_idx: usize) -> anyhow::Result<Self> {
+    pub fn from_dimacs_with_idx<R: io::BufRead>(reader: R, obj_idx: usize) -> anyhow::Result<Self> {
         fio::dimacs::parse_wcnf_with_idx(reader, obj_idx)
     }
 
@@ -1090,14 +1388,14 @@ impl<VM: ManageVars + Default> OptInstance<VM> {
     /// The file format expected by this parser is the OPB format for
     /// pseudo-boolean optimization instances. For details on the file format
     /// see [here](https://www.cril.univ-artois.fr/PB12/format.pdf).
-    pub fn from_opb<R: io::Read>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+    pub fn from_opb<R: io::BufRead>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
         Self::from_opb_with_idx(reader, 0, opts)
     }
 
     /// Parses an OPB instance from a reader object, selecting the objective
     /// with index `obj_idx` if multiple are available. The index starts at 0.
     /// For more details see [`OptInstance::from_opb`].
-    pub fn from_opb_with_idx<R: io::Read>(
+    pub fn from_opb_with_idx<R: io::BufRead>(
         reader: R,
         obj_idx: usize,
         opts: fio::opb::Options,
@@ -1134,9 +1432,9 @@ impl<VM: ManageVars + Default> FromIterator<WcnfLine> for OptInstance<VM> {
         for line in iter {
             match line {
                 WcnfLine::Comment(_) => (),
-                WcnfLine::Hard(cl) => inst.get_constraints().add_clause(cl),
+                WcnfLine::Hard(cl) => inst.constraints_mut().add_clause(cl),
                 WcnfLine::Soft(cl, w) => {
-                    inst.get_objective().add_soft_clause(w, cl);
+                    inst.objective_mut().add_soft_clause(w, cl);
                 }
             }
         }
diff --git a/rustsat/src/instances/sat.rs b/rustsat/src/instances/sat.rs
index 69e77524..287cc81d 100644
--- a/rustsat/src/instances/sat.rs
+++ b/rustsat/src/instances/sat.rs
@@ -10,6 +10,7 @@ use crate::{
         constraints::{CardConstraint, PBConstraint},
         Assignment, Clause, Lit, Var,
     },
+    RequiresClausal,
 };
 
 use anyhow::Context;
@@ -77,6 +78,11 @@ impl Cnf {
         self.clauses.len()
     }
 
+    /// Adds a clause from a slice of literals
+    pub fn add_nary(&mut self, lits: &[Lit]) {
+        self.add_clause(lits.into())
+    }
+
     /// See [`atomics::lit_impl_lit`]
     pub fn add_lit_impl_lit(&mut self, a: Lit, b: Lit) {
         self.add_clause(atomics::lit_impl_lit(a, b))
@@ -190,6 +196,21 @@ impl Cnf {
     pub fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) {
         self.add_clause(clause![lit1, lit2, lit3])
     }
+
+    /// Writes the CNF to a DIMACS CNF file at a path
+    pub fn write_dimacs_path<P: AsRef<Path>>(&self, path: P, n_vars: u32) -> Result<(), io::Error> {
+        let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        self.write_dimacs(&mut writer, n_vars)
+    }
+
+    /// Writes the CNF to DIMACS CNF
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
+    pub fn write_dimacs<W: io::Write>(&self, writer: &mut W, n_vars: u32) -> Result<(), io::Error> {
+        fio::dimacs::write_cnf_annotated(writer, self, n_vars)
+    }
 }
 
 impl CollectClauses for Cnf {
@@ -283,6 +304,11 @@ impl<VM: ManageVars> SatInstance<VM> {
         self.cnf.add_clause(cl);
     }
 
+    /// Adds a clause from a slice of literals
+    pub fn add_nary(&mut self, lits: &[Lit]) {
+        self.add_clause(lits.into())
+    }
+
     /// Adds a unit clause to the instance
     pub fn add_unit(&mut self, unit: Lit) {
         self.add_clause(clause![unit])
@@ -401,27 +427,51 @@ impl<VM: ManageVars> SatInstance<VM> {
         self.pbs.push(pb)
     }
 
+    /// Gets a reference to the internal CNF
+    pub fn cnf(&self) -> &Cnf {
+        &self.cnf
+    }
+
     /// Gets a reference to the variable manager
+    #[deprecated(
+        since = "0.5.0",
+        note = "var_manager has been renamed to var_manager_mut and will be removed in a future release"
+    )]
     pub fn var_manager(&mut self) -> &mut VM {
         &mut self.var_manager
     }
 
+    /// Gets a mutable reference to the variable manager
+    pub fn var_manager_mut(&mut self) -> &mut VM {
+        &mut self.var_manager
+    }
+
+    /// Gets a reference to the variable manager
+    pub fn var_manager_ref(&self) -> &VM {
+        &self.var_manager
+    }
+
     /// Reserves a new variable in the internal variable manager. This is a
     /// shortcut for `inst.var_manager().new_var()`.
     pub fn new_var(&mut self) -> Var {
-        self.var_manager().new_var()
+        self.var_manager_mut().new_var()
     }
 
     /// Reserves a new variable in the internal variable manager. This is a
     /// shortcut for `inst.var_manager().new_lit()`.
     pub fn new_lit(&mut self) -> Lit {
-        self.var_manager().new_lit()
+        self.var_manager_mut().new_lit()
     }
 
     /// Gets the used variable with the highest index. This is a shortcut
     /// for `inst.var_manager().max_var()`.
-    pub fn max_var(&mut self) -> Option<Var> {
-        self.var_manager().max_var()
+    pub fn max_var(&self) -> Option<Var> {
+        self.var_manager_ref().max_var()
+    }
+
+    /// Returns the number of variables in the variable manager of the instance
+    pub fn n_vars(&self) -> u32 {
+        self.var_manager_ref().n_used()
     }
 
     /// Converts the included variable manager to a different type
@@ -443,8 +493,31 @@ impl<VM: ManageVars> SatInstance<VM> {
 
     /// Converts the instance to a set of clauses.
     /// Uses the default encoders from the `encodings` module.
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_cnf has been renamed to into_cnf and will be removed in a future release"
+    )]
     pub fn as_cnf(self) -> (Cnf, VM) {
-        self.as_cnf_with_encoders(
+        self.into_cnf()
+    }
+
+    /// Converts the instance to a set of clauses.
+    /// Uses the default encoders from the `encodings` module.
+    ///
+    /// See [`Self::convert_to_cnf`] for converting in place
+    pub fn into_cnf(self) -> (Cnf, VM) {
+        self.into_cnf_with_encoders(
+            card::default_encode_cardinality_constraint,
+            pb::default_encode_pb_constraint,
+        )
+    }
+
+    /// Converts the instance to a set of clauses inplace.
+    /// Uses the default encoders from the `encodings` module.
+    ///
+    /// See [`Self::into_cnf`] if you don't need to convert in place
+    pub fn convert_to_cnf(&mut self) {
+        self.convert_to_cnf_with_encoders(
             card::default_encode_cardinality_constraint,
             pb::default_encode_pb_constraint,
         )
@@ -452,22 +525,57 @@ impl<VM: ManageVars> SatInstance<VM> {
 
     /// Converts the instance to a set of clauses with explicitly specified
     /// converters for non-clausal constraints.
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_cnf_with_encoders has been renamed to into_cnf_with_encoders and will be removed in a future release"
+    )]
     pub fn as_cnf_with_encoders<CardEnc, PBEnc>(
+        self,
+        card_encoder: CardEnc,
+        pb_encoder: PBEnc,
+    ) -> (Cnf, VM)
+    where
+        CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars),
+        PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars),
+    {
+        self.into_cnf_with_encoders(card_encoder, pb_encoder)
+    }
+
+    /// Converts the instance to a set of clauses with explicitly specified
+    /// converters for non-clausal constraints.
+    ///
+    /// See [`Self::into_cnf_with_encoders`] to convert in place
+    pub fn into_cnf_with_encoders<CardEnc, PBEnc>(
         mut self,
-        mut card_encoder: CardEnc,
-        mut pb_encoder: PBEnc,
+        card_encoder: CardEnc,
+        pb_encoder: PBEnc,
     ) -> (Cnf, VM)
     where
         CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars),
         PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars),
+    {
+        self.convert_to_cnf_with_encoders(card_encoder, pb_encoder);
+        (self.cnf, self.var_manager)
+    }
+
+    /// Converts the instance inplace to a set of clauses with explicitly specified
+    /// converters for non-clausal constraints.
+    ///
+    /// See [`Self::into_cnf_with_encoders`] if you don't need to convert in place
+    pub fn convert_to_cnf_with_encoders<CardEnc, PBEnc>(
+        &mut self,
+        mut card_encoder: CardEnc,
+        mut pb_encoder: PBEnc,
+    ) where
+        CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars),
+        PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars),
     {
         self.cards
-            .into_iter()
+            .drain(..)
             .for_each(|constr| card_encoder(constr, &mut self.cnf, &mut self.var_manager));
         self.pbs
-            .into_iter()
+            .drain(..)
             .for_each(|constr| pb_encoder(constr, &mut self.cnf, &mut self.var_manager));
-        (self.cnf, self.var_manager)
     }
 
     /// Extends the instance by another instance
@@ -512,13 +620,17 @@ impl<VM: ManageVars> SatInstance<VM> {
     /// # Performance
     ///
     /// For performance, consider using a [`std::io::BufWriter`] instance.
+    #[deprecated(since = "0.5.0", note = "use write_dimacs_path instead")]
     pub fn to_dimacs_path<P: AsRef<Path>>(self, path: P) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        #[allow(deprecated)]
         self.to_dimacs(&mut writer)
     }
 
     /// Writes the instance to DIMACS CNF
+    #[deprecated(since = "0.5.0", note = "use write_dimacs instead")]
     pub fn to_dimacs<W: io::Write>(self, writer: &mut W) -> Result<(), io::Error> {
+        #[allow(deprecated)]
         self.to_dimacs_with_encoders(
             card::default_encode_cardinality_constraint,
             pb::default_encode_pb_constraint,
@@ -528,6 +640,10 @@ impl<VM: ManageVars> SatInstance<VM> {
 
     /// Writes the instance to DIMACS CNF converting non-clausal constraints
     /// with specific encoders.
+    #[deprecated(
+        since = "0.5.0",
+        note = "use convert_to_cnf_with_encoders and write_dimacs instead"
+    )]
     pub fn to_dimacs_with_encoders<W, CardEnc, PBEnc>(
         self,
         card_encoder: CardEnc,
@@ -539,8 +655,45 @@ impl<VM: ManageVars> SatInstance<VM> {
         CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars),
         PBEnc: FnMut(PBConstraint, &mut Cnf, &mut dyn ManageVars),
     {
-        let (cnf, vm) = self.as_cnf_with_encoders(card_encoder, pb_encoder);
-        fio::dimacs::write_cnf_annotated(writer, cnf, vm.max_var())
+        let (cnf, vm) = self.into_cnf_with_encoders(card_encoder, pb_encoder);
+        fio::dimacs::write_cnf_annotated(writer, &cnf, vm.n_used())
+    }
+
+    /// Writes the instance to a DIMACS CNF file at a path
+    ///
+    /// This requires that the instance is clausal, i.e., does not contain any non-converted
+    /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by
+    /// [`Self::convert_to_cnf`] or [`Self::convert_to_cnf_with_encoders`] first.
+    ///
+    /// # Errors
+    ///
+    /// - If the instance is not clausal, returns [`NonClausal`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_dimacs_path<P: AsRef<Path>>(&self, path: P) -> anyhow::Result<()> {
+        let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        self.write_dimacs(&mut writer)
+    }
+
+    /// Writes the instance to DIMACS CNF
+    ///
+    /// This requires that the instance is clausal, i.e., does not contain any non-converted
+    /// cardinality of pseudo-boolean constraints. If necessary, the instance can be converted by
+    /// [`Self::convert_to_cnf`] or [`Self::convert_to_cnf_with_encoders`] first.
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
+    ///
+    /// # Errors
+    ///
+    /// - If the instance is not clausal, returns [`NonClausal`]
+    /// - Returns [`io::Error`] on errors during writing
+    pub fn write_dimacs<W: io::Write>(&self, writer: &mut W) -> anyhow::Result<()> {
+        if self.n_cards() > 0 || self.n_pbs() > 0 {
+            return Err(RequiresClausal.into());
+        }
+        let n_vars = self.n_vars();
+        Ok(fio::dimacs::write_cnf_annotated(writer, &self.cnf, n_vars)?)
     }
 
     /// Writes the instance to an OPB file at a path
@@ -548,20 +701,46 @@ impl<VM: ManageVars> SatInstance<VM> {
     /// # Performance
     ///
     /// For performance, consider using a [`std::io::BufWriter`] instance.
+    #[deprecated(since = "0.5.0", note = "use write_opb_path instead")]
     pub fn to_opb_path<P: AsRef<Path>>(
         self,
         path: P,
         opts: fio::opb::Options,
     ) -> Result<(), io::Error> {
         let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        #[allow(deprecated)]
         self.to_opb(&mut writer, opts)
     }
 
     /// Writes the instance to an OPB file
+    #[deprecated(since = "0.5.0", note = "use write_opb instead")]
     pub fn to_opb<W: io::Write>(
         self,
         writer: &mut W,
         opts: fio::opb::Options,
+    ) -> Result<(), io::Error> {
+        fio::opb::write_sat(writer, &self, opts)
+    }
+
+    /// Writes the instance to an OPB file at a path
+    pub fn write_opb_path<P: AsRef<Path>>(
+        &self,
+        path: P,
+        opts: fio::opb::Options,
+    ) -> Result<(), io::Error> {
+        let mut writer = fio::open_compressed_uncompressed_write(path)?;
+        self.write_opb(&mut writer, opts)
+    }
+
+    /// Writes the instance to an OPB file
+    ///
+    /// # Performance
+    ///
+    /// For performance, consider using a [`std::io::BufWriter`] instance.
+    pub fn write_opb<W: io::Write>(
+        &self,
+        writer: &mut W,
+        opts: fio::opb::Options,
     ) -> Result<(), io::Error> {
         fio::opb::write_sat(writer, self, opts)
     }
@@ -599,11 +778,11 @@ impl<VM: ManageVars> SatInstance<VM> {
                     return None;
                 }
                 if pb.is_clause() {
-                    cnf.add_clause(pb.as_clause().unwrap());
+                    cnf.add_clause(pb.into_clause().unwrap());
                     return None;
                 }
                 if pb.is_card() {
-                    cards.push(pb.as_card_constr().unwrap());
+                    cards.push(pb.into_card_constr().unwrap());
                     return None;
                 }
                 Some(pb)
@@ -630,7 +809,7 @@ impl<VM: ManageVars> SatInstance<VM> {
                     return None;
                 }
                 if card.is_clause() {
-                    cnf.add_clause(card.as_clause().unwrap());
+                    cnf.add_clause(card.into_clause().unwrap());
                     return None;
                 }
                 Some(card)
@@ -688,7 +867,7 @@ impl<VM: ManageVars + Default> SatInstance<VM> {
     ///
     /// If a DIMACS WCNF or MCNF file is parsed with this method, the objectives
     /// are ignored and only the constraints returned.
-    pub fn from_dimacs<R: io::Read>(reader: R) -> anyhow::Result<Self> {
+    pub fn from_dimacs<R: io::BufRead>(reader: R) -> anyhow::Result<Self> {
         fio::dimacs::parse_cnf(reader)
     }
 
@@ -708,7 +887,7 @@ impl<VM: ManageVars + Default> SatInstance<VM> {
     /// The file format expected by this parser is the OPB format for
     /// pseudo-boolean satisfaction instances. For details on the file format
     /// see [here](https://www.cril.univ-artois.fr/PB12/format.pdf).
-    pub fn from_opb<R: io::Read>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
+    pub fn from_opb<R: io::BufRead>(reader: R, opts: fio::opb::Options) -> anyhow::Result<Self> {
         fio::opb::parse_sat(reader, opts)
     }
 
diff --git a/rustsat/src/lib.rs b/rustsat/src/lib.rs
index d05d0f33..3095fcfc 100644
--- a/rustsat/src/lib.rs
+++ b/rustsat/src/lib.rs
@@ -88,3 +88,11 @@ impl fmt::Display for NotAllowed {
 #[cfg(feature = "bench")]
 #[cfg(test)]
 mod bench;
+
+#[derive(Error, Debug)]
+#[error("operation requires a clausal constraint(s) but it is not")]
+pub struct RequiresClausal;
+
+#[derive(Error, Debug)]
+#[error("operation requires an objective only consisting of soft literals")]
+pub struct RequiresSoftLits;
diff --git a/rustsat/src/solvers.rs b/rustsat/src/solvers.rs
index cc979a8a..08917610 100644
--- a/rustsat/src/solvers.rs
+++ b/rustsat/src/solvers.rs
@@ -96,7 +96,7 @@ use thiserror::Error;
 /// Trait for all SAT solvers in this library.
 /// Solvers outside of this library can also implement this trait to be able to
 /// use them with this library.
-pub trait Solve: Extend<Clause> {
+pub trait Solve: Extend<Clause> + for<'a> Extend<&'a Clause> {
     /// Gets a signature of the solver implementation
     fn signature(&self) -> &'static str;
     /// Reserves memory in the solver until a maximum variables, if the solver
@@ -175,10 +175,19 @@ pub trait Solve: Extend<Clause> {
     /// - If the solver is not in the satisfied state
     /// - A specific implementation might return other errors
     fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal>;
-    /// Adds a clause to the solver
+    /// Adds a clause to the solver.
     /// If the solver is in the satisfied or unsatisfied state before, it is in
     /// the input state afterwards.
-    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()>;
+    ///
+    /// This method can be implemented by solvers that can truly take ownership of the clause.
+    /// Otherwise, it will fall back to the mandatory [`Solve::add_clause_ref`] method.
+    fn add_clause(&mut self, clause: Clause) -> anyhow::Result<()> {
+        self.add_clause_ref(&clause)
+    }
+    /// Adds a clause to the solver by reference.
+    /// If the solver is in the satisfied or unsatisfied state before, it is in
+    /// the input state afterwards.
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()>;
     /// Like [`Solve::add_clause`] but for unit clauses (clauses with one literal).
     fn add_unit(&mut self, lit: Lit) -> anyhow::Result<()> {
         self.add_clause(clause![lit])
@@ -195,6 +204,10 @@ pub trait Solve: Extend<Clause> {
     fn add_cnf(&mut self, cnf: Cnf) -> anyhow::Result<()> {
         cnf.into_iter().try_for_each(|cl| self.add_clause(cl))
     }
+    /// Adds all clauses from a [`Cnf`] instance by reference.
+    fn add_cnf_ref(&mut self, cnf: &Cnf) -> anyhow::Result<()> {
+        cnf.iter().try_for_each(|cl| self.add_clause_ref(cl))
+    }
 }
 
 /// Trait for all SAT solvers in this library.
diff --git a/rustsat/src/types/constraints.rs b/rustsat/src/types/constraints.rs
index 2856b9b8..664298d9 100644
--- a/rustsat/src/types/constraints.rs
+++ b/rustsat/src/types/constraints.rs
@@ -13,6 +13,8 @@ use thiserror::Error;
 
 use super::{Assignment, IWLitIter, Lit, LitIter, RsHashSet, TernaryVal, WLitIter};
 
+use crate::RequiresClausal;
+
 /// Type representing a clause.
 /// Wrapper around a std collection to allow for changing the data structure.
 /// Optional clauses as sets will be included in the future.
@@ -433,16 +435,25 @@ impl CardConstraint {
     }
 
     /// Converts the constraint into a clause, if possible
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_clause has been slightly changed and renamed to into_clause and will be removed in a future release"
+    )]
     pub fn as_clause(self) -> Option<Clause> {
+        self.into_clause().ok()
+    }
+
+    /// Converts the constraint into a clause, if possible
+    pub fn into_clause(self) -> Result<Clause, RequiresClausal> {
         if !self.is_clause() {
-            return None;
+            return Err(RequiresClausal);
         }
         match self {
             CardConstraint::UB(constr) => {
-                Some(Clause::from_iter(constr.lits.into_iter().map(Lit::not)))
+                Ok(Clause::from_iter(constr.lits.into_iter().map(Lit::not)))
             }
-            CardConstraint::LB(constr) => Some(Clause::from_iter(constr.lits)),
-            CardConstraint::EQ(_) => panic!(),
+            CardConstraint::LB(constr) => Ok(Clause::from_iter(constr.lits)),
+            CardConstraint::EQ(_) => unreachable!(),
         }
     }
 
@@ -494,6 +505,11 @@ impl CardUBConstr {
         (self.lits, self.b)
     }
 
+    /// Get references to the constraints internals
+    pub(crate) fn decompose_ref(&self) -> (&Vec<Lit>, &usize) {
+        (&self.lits, &self.b)
+    }
+
     /// Checks if the constraint is always satisfied
     pub fn is_tautology(&self) -> bool {
         self.b >= self.lits.len()
@@ -523,6 +539,11 @@ impl CardLBConstr {
         (self.lits, self.b)
     }
 
+    /// Get references to the constraints internals
+    pub(crate) fn decompose_ref(&self) -> (&Vec<Lit>, &usize) {
+        (&self.lits, &self.b)
+    }
+
     /// Checks if the constraint is always satisfied
     pub fn is_tautology(&self) -> bool {
         self.b == 0
@@ -557,6 +578,11 @@ impl CardEQConstr {
         (self.lits, self.b)
     }
 
+    /// Get references to the constraints internals
+    pub(crate) fn decompose_ref(&self) -> (&Vec<Lit>, &usize) {
+        (&self.lits, &self.b)
+    }
+
     /// Checks if the constraint is unsatisfiable
     pub fn is_unsat(&self) -> bool {
         self.b > self.lits.len()
@@ -763,7 +789,16 @@ impl PBConstraint {
     }
 
     /// Converts the pseudo-boolean constraint into a cardinality constraint, if possible
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_card_constr has been renamed to into_card_constr"
+    )]
     pub fn as_card_constr(self) -> Result<CardConstraint, PBToCardError> {
+        self.into_card_constr()
+    }
+
+    /// Converts the pseudo-boolean constraint into a cardinality constraint, if possible
+    pub fn into_card_constr(self) -> Result<CardConstraint, PBToCardError> {
         if self.is_tautology() {
             return Err(PBToCardError::Tautology);
         }
@@ -816,18 +851,27 @@ impl PBConstraint {
     }
 
     /// Converts the constraint into a clause, if possible
+    #[deprecated(
+        since = "0.5.0",
+        note = "as_clause has been slightly changed and renamed to into_clause and will be removed in a future release"
+    )]
     pub fn as_clause(self) -> Option<Clause> {
+        self.into_clause().ok()
+    }
+
+    /// Converts the constraint into a clause, if possible
+    pub fn into_clause(self) -> Result<Clause, RequiresClausal> {
         if !self.is_clause() {
-            return None;
+            return Err(RequiresClausal);
         }
         match self {
-            PBConstraint::UB(constr) => Some(Clause::from_iter(
+            PBConstraint::UB(constr) => Ok(Clause::from_iter(
                 constr.lits.into_iter().map(|(lit, _)| !lit),
             )),
-            PBConstraint::LB(constr) => Some(Clause::from_iter(
+            PBConstraint::LB(constr) => Ok(Clause::from_iter(
                 constr.lits.into_iter().map(|(lit, _)| lit),
             )),
-            PBConstraint::EQ(_) => panic!(),
+            PBConstraint::EQ(_) => unreachable!(),
         }
     }
 
@@ -907,6 +951,11 @@ impl PBUBConstr {
         (self.lits, self.b)
     }
 
+    /// Gets references to the constraints internals
+    pub(crate) fn decompose_ref(&self) -> (&Vec<(Lit, usize)>, &isize) {
+        (&self.lits, &self.b)
+    }
+
     /// Checks if the constraint is always satisfied
     pub fn is_tautology(&self) -> bool {
         if self.b < 0 {
@@ -977,6 +1026,11 @@ impl PBLBConstr {
         (self.lits, self.b)
     }
 
+    /// Gets references to the constraints internals
+    pub(crate) fn decompose_ref(&self) -> (&Vec<(Lit, usize)>, &isize) {
+        (&self.lits, &self.b)
+    }
+
     /// Checks if the constraint is always satisfied
     pub fn is_tautology(&self) -> bool {
         self.b <= 0
@@ -1048,6 +1102,11 @@ impl PBEQConstr {
         (self.lits, self.b)
     }
 
+    /// Gets references to the constraints internals
+    pub(crate) fn decompose_ref(&self) -> (&Vec<(Lit, usize)>, &isize) {
+        (&self.lits, &self.b)
+    }
+
     /// Checks if the constraint is unsatisfiable
     pub fn is_unsat(&self) -> bool {
         if self.b < 0 {
diff --git a/tools/Cargo.toml b/tools/Cargo.toml
index 22c9cc1a..8dfda761 100644
--- a/tools/Cargo.toml
+++ b/tools/Cargo.toml
@@ -27,6 +27,7 @@ atty = { version = "0.2.14" }
 nom = "7.1.3"
 rand = "0.8.5"
 rand_chacha = "0.3.1"
+anyhow = { version = "1.0.80" }
 
 [features]
 default = ["minisat"]
diff --git a/tools/src/bin/cnf2opb.rs b/tools/src/bin/cnf2opb.rs
index c0153dcc..6242c3f9 100644
--- a/tools/src/bin/cnf2opb.rs
+++ b/tools/src/bin/cnf2opb.rs
@@ -2,6 +2,7 @@
 //!
 //! A small tool for converting DIMACS CNF files to OPB.
 
+use anyhow::Context;
 use clap::Parser;
 use rustsat::instances::{fio::opb::Options as OpbOptions, SatInstance};
 use std::{io, path::PathBuf};
@@ -21,7 +22,7 @@ struct Args {
     avoid_negated_lits: bool,
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     let args = Args::parse();
     let opb_opts = OpbOptions {
         first_var_idx: args.first_var_idx,
@@ -29,16 +30,17 @@ fn main() {
     };
 
     let inst: SatInstance = if let Some(in_path) = args.in_path {
-        SatInstance::from_dimacs_path(in_path).expect("error parsing the input file")
+        SatInstance::from_dimacs_path(in_path).context("error parsing the input file")?
     } else {
-        SatInstance::from_dimacs(io::stdin()).expect("error parsing input")
+        SatInstance::from_dimacs(io::BufReader::new(io::stdin())).context("error parsing input")?
     };
 
     if let Some(out_path) = args.out_path {
-        inst.to_opb_path(out_path, opb_opts)
-            .expect("io error writing the output file");
+        inst.write_opb_path(out_path, opb_opts)
+            .context("error writing the output file")?;
     } else {
-        inst.to_opb(&mut io::stdout(), opb_opts)
-            .expect("io error writing the output file");
+        inst.write_opb(&mut io::stdout(), opb_opts)
+            .context("error writing the output file")?;
     }
+    Ok(())
 }
diff --git a/tools/src/bin/encodings.rs b/tools/src/bin/encodings.rs
index fc28c61f..95768524 100644
--- a/tools/src/bin/encodings.rs
+++ b/tools/src/bin/encodings.rs
@@ -14,7 +14,7 @@
 use clap::{Args, Parser, Subcommand};
 use rustsat::{encodings::pb, instances::fio::dimacs};
 use rustsat_tools::encodings::{
-    clustering::{self, saturating_map, scaling_map, Encoding, Error, Variant},
+    clustering::{self, saturating_map, scaling_map, Encoding, Variant},
     knapsack,
 };
 use std::{fs::File, io, path::PathBuf};
@@ -93,7 +93,7 @@ struct KnapsackArgs {
     seed: u64,
 }
 
-fn clustering(args: ClusteringArgs) -> Result<(), Error> {
+fn clustering(args: ClusteringArgs) -> anyhow::Result<()> {
     let mcnf_to_wcnf = |line: dimacs::McnfLine| match line {
         dimacs::McnfLine::Comment(c) => dimacs::WcnfLine::Comment(c),
         dimacs::McnfLine::Hard(cl) => dimacs::WcnfLine::Hard(cl),
@@ -149,7 +149,7 @@ fn clustering(args: ClusteringArgs) -> Result<(), Error> {
     Ok(())
 }
 
-fn knapsack(args: KnapsackArgs) -> Result<(), Error> {
+fn knapsack(args: KnapsackArgs) -> anyhow::Result<()> {
     let encoding = knapsack::Encoding::new::<pb::DynamicPolyWatchdog>(knapsack::Knapsack::random(
         args.n_items,
         args.n_objectives,
@@ -167,7 +167,7 @@ fn knapsack(args: KnapsackArgs) -> Result<(), Error> {
     Ok(())
 }
 
-fn main() -> Result<(), Error> {
+fn main() -> anyhow::Result<()> {
     let args = CliArgs::parse();
 
     match args.cmd {
diff --git a/tools/src/bin/enumerator.rs b/tools/src/bin/enumerator.rs
index b885503f..2c2efcf8 100644
--- a/tools/src/bin/enumerator.rs
+++ b/tools/src/bin/enumerator.rs
@@ -4,6 +4,7 @@
 //!
 //! Usage: enumerator [dimacs cnf file]
 
+use anyhow::Context;
 use rustsat::{
     instances::{ManageVars, SatInstance},
     solvers::{self, Solve, SolveIncremental},
@@ -45,17 +46,17 @@ impl<S: SolveIncremental> Iterator for Enumerator<S> {
     }
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     let in_path = std::env::args().nth(1).unwrap_or_else(|| print_usage!());
 
     let inst: SatInstance =
-        SatInstance::from_dimacs_path(in_path).expect("error parsing the input file");
-    let (cnf, vm) = inst.as_cnf();
+        SatInstance::from_dimacs_path(in_path).context("error parsing the input file")?;
+    let (cnf, vm) = inst.into_cnf();
 
     let mut solver = rustsat_tools::Solver::default();
     solver
         .reserve(vm.max_var().expect("no variables in instance"))
-        .expect("error reserving memory in solver");
+        .context("error reserving memory in solver")?;
     solver.add_cnf(cnf).expect("error adding cnf to solver");
 
     let enumerator = Enumerator {
@@ -63,5 +64,6 @@ fn main() {
         max_var: vm.max_var().unwrap(),
     };
 
-    enumerator.for_each(|sol| println!("s {}", sol))
+    enumerator.for_each(|sol| println!("s {}", sol));
+    Ok(())
 }
diff --git a/tools/src/bin/gbmosplit.rs b/tools/src/bin/gbmosplit.rs
index 7c48f45b..e7d2de7c 100644
--- a/tools/src/bin/gbmosplit.rs
+++ b/tools/src/bin/gbmosplit.rs
@@ -252,7 +252,7 @@ fn split<VM: ManageVars>(
         );
     }
 
-    let (softs, offset) = obj.as_soft_cls();
+    let (softs, offset) = obj.into_soft_cls();
 
     if offset != 0 {
         cli.warning(&format!(
@@ -475,7 +475,7 @@ fn main() {
 
     if let Some(out_path) = &cli.out_path {
         if found_split || cli.always_dump {
-            mo_inst.to_dimacs_path(out_path).unwrap_or_else(|e| {
+            mo_inst.write_dimacs_path(out_path).unwrap_or_else(|e| {
                 cli.error(&format!("io error writing the output file: {}", e));
                 panic!()
             });
diff --git a/tools/src/bin/mcnf2opb.rs b/tools/src/bin/mcnf2opb.rs
index 9830083d..345d06b4 100644
--- a/tools/src/bin/mcnf2opb.rs
+++ b/tools/src/bin/mcnf2opb.rs
@@ -2,6 +2,7 @@
 //!
 //! A small tool for converting DIMACS MCNF files to OPB.
 
+use anyhow::Context;
 use clap::Parser;
 use rustsat::instances::{fio::opb::Options as OpbOptions, MultiOptInstance};
 use std::{io, path::PathBuf};
@@ -21,7 +22,7 @@ struct Args {
     avoid_negated_lits: bool,
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     let args = Args::parse();
     let opb_opts = OpbOptions {
         first_var_idx: args.first_var_idx,
@@ -29,16 +30,25 @@ fn main() {
     };
 
     let inst: MultiOptInstance = if let Some(in_path) = args.in_path {
-        MultiOptInstance::from_dimacs_path(in_path).expect("error parsing the input file")
+        MultiOptInstance::from_dimacs_path(in_path).context("error parsing the input file")?
     } else {
-        MultiOptInstance::from_dimacs(io::stdin()).expect("error parsing input")
+        MultiOptInstance::from_dimacs(io::BufReader::new(io::stdin()))
+            .context("error parsing input")?
     };
 
+    let (mut constr, mut objs) = inst.decompose();
+    for obj in &mut objs {
+        let hardened = obj.convert_to_soft_lits(constr.var_manager_mut());
+        constr.extend(hardened.into());
+    }
+    let inst = MultiOptInstance::compose(constr, objs);
+
     if let Some(out_path) = args.out_path {
-        inst.to_opb_path(out_path, opb_opts)
-            .expect("io error writing the output file");
+        inst.write_opb_path(out_path, opb_opts)
+            .context("error writing the output file")?;
     } else {
-        inst.to_opb(&mut io::stdout(), opb_opts)
-            .expect("io error writing the output file");
+        inst.write_opb(&mut io::stdout(), opb_opts)
+            .context("error writing the output file")?;
     }
+    Ok(())
 }
diff --git a/tools/src/bin/opb2cnf.rs b/tools/src/bin/opb2cnf.rs
index 9bc13768..0d8244f3 100644
--- a/tools/src/bin/opb2cnf.rs
+++ b/tools/src/bin/opb2cnf.rs
@@ -2,6 +2,7 @@
 //!
 //! A small tool for converting OPB files to DIMACS CNF.
 
+use anyhow::Context;
 use clap::Parser;
 use rustsat::instances::{fio::opb::Options as OpbOptions, SatInstance};
 use std::{io, path::PathBuf};
@@ -18,28 +19,32 @@ struct Args {
     first_var_idx: usize,
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     let args = Args::parse();
     let opb_opts = OpbOptions {
         first_var_idx: 0,
         ..Default::default()
     };
 
-    let inst: SatInstance = if let Some(in_path) = args.in_path {
-        SatInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file")
+    let mut inst: SatInstance = if let Some(in_path) = args.in_path {
+        SatInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")?
     } else {
-        SatInstance::from_opb(io::stdin(), opb_opts).expect("error parsing input")
+        SatInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts)
+            .context("error parsing input")?
     };
 
     println!("{} clauses", inst.n_clauses());
     println!("{} cards", inst.n_cards());
     println!("{} pbs", inst.n_pbs());
 
+    inst.convert_to_cnf();
+
     if let Some(out_path) = args.out_path {
-        inst.to_dimacs_path(out_path)
-            .expect("io error writing the output file");
+        inst.write_dimacs_path(out_path)
+            .context("error writing the output file")?;
     } else {
-        inst.to_dimacs(&mut io::stdout())
-            .expect("io error writing to stdout");
+        inst.write_dimacs(&mut io::stdout())
+            .context("error writing to stdout")?;
     }
+    Ok(())
 }
diff --git a/tools/src/bin/opb2mcnf.rs b/tools/src/bin/opb2mcnf.rs
index a7127f8b..0bb9c873 100644
--- a/tools/src/bin/opb2mcnf.rs
+++ b/tools/src/bin/opb2mcnf.rs
@@ -2,6 +2,7 @@
 //!
 //! A small tool for converting OPB files to DIMACS MCNF.
 
+use anyhow::Context;
 use clap::Parser;
 use rustsat::instances::{fio::opb::Options as OpbOptions, MultiOptInstance};
 use std::{io, path::PathBuf};
@@ -18,7 +19,7 @@ struct Args {
     first_var_idx: usize,
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     let args = Args::parse();
     let opb_opts = OpbOptions {
         first_var_idx: 0,
@@ -26,9 +27,11 @@ fn main() {
     };
 
     let inst: MultiOptInstance = if let Some(in_path) = args.in_path {
-        MultiOptInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file")
+        MultiOptInstance::from_opb_path(in_path, opb_opts)
+            .context("error parsing the input file")?
     } else {
-        MultiOptInstance::from_opb(io::stdin(), opb_opts).expect("error parsing input")
+        MultiOptInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts)
+            .context("error parsing input")?
     };
 
     let (constrs, objs) = inst.decompose();
@@ -39,13 +42,15 @@ fn main() {
     println!("c {} pbs", constrs.n_pbs());
     println!("c {} objectives", objs.len());
 
-    let inst = MultiOptInstance::compose(constrs, objs);
+    let mut inst = MultiOptInstance::compose(constrs, objs);
+    inst.constraints_mut().convert_to_cnf();
 
     if let Some(out_path) = args.out_path {
-        inst.to_dimacs_path(out_path)
-            .expect("io error writing the output file");
+        inst.write_dimacs_path(out_path)
+            .context("error writing the output file")?;
     } else {
-        inst.to_dimacs(&mut io::stdout())
-            .expect("io error writing to stdout");
+        inst.write_dimacs(&mut io::stdout())
+            .context("error writing to stdout")?;
     }
+    Ok(())
 }
diff --git a/tools/src/bin/opb2wcnf.rs b/tools/src/bin/opb2wcnf.rs
index 3e075a84..f2fdf3a0 100644
--- a/tools/src/bin/opb2wcnf.rs
+++ b/tools/src/bin/opb2wcnf.rs
@@ -2,6 +2,7 @@
 //!
 //! A small tool for converting OPB files to DIMACS WCNF.
 
+use anyhow::Context;
 use clap::Parser;
 use rustsat::instances::{fio::opb::Options as OpbOptions, OptInstance};
 use std::{io, path::PathBuf};
@@ -18,7 +19,7 @@ struct Args {
     first_var_idx: usize,
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     let args = Args::parse();
     let opb_opts = OpbOptions {
         first_var_idx: 0,
@@ -26,25 +27,28 @@ fn main() {
     };
 
     let inst: OptInstance = if let Some(in_path) = args.in_path {
-        OptInstance::from_opb_path(in_path, opb_opts).expect("error parsing the input file")
+        OptInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")?
     } else {
-        OptInstance::from_opb(io::stdin(), opb_opts).expect("error parsing input")
+        OptInstance::from_opb(io::BufReader::new(io::stdin()), opb_opts)
+            .context("error parsing input")?
     };
 
     let (constrs, obj) = inst.decompose();
-    let constrs = constrs.sanitize();
+    let mut constrs = constrs.sanitize();
 
     println!("c {} clauses", constrs.n_clauses());
     println!("c {} cards", constrs.n_cards());
     println!("c {} pbs", constrs.n_pbs());
 
+    constrs.convert_to_cnf();
     let inst = OptInstance::compose(constrs, obj);
 
     if let Some(out_path) = args.out_path {
-        inst.to_dimacs_path(out_path)
-            .expect("io error writing the output file");
+        inst.write_dimacs_path(out_path)
+            .context("io error writing the output file")?;
     } else {
-        inst.to_dimacs(&mut io::stdout())
-            .expect("io error writing to stdout");
+        inst.write_dimacs(&mut io::stdout())
+            .context("io error writing to stdout")?;
     }
+    Ok(())
 }
diff --git a/tools/src/bin/shuffledimacs.rs b/tools/src/bin/shuffledimacs.rs
index 645d1568..e10c61e9 100644
--- a/tools/src/bin/shuffledimacs.rs
+++ b/tools/src/bin/shuffledimacs.rs
@@ -7,7 +7,8 @@
 
 use std::path::{Path, PathBuf};
 
-use rustsat::instances::{self, BasicVarManager, ManageVars, RandReindVarManager};
+use anyhow::Context;
+use rustsat::instances::{self, BasicVarManager, RandReindVarManager};
 
 macro_rules! print_usage {
     () => {{
@@ -22,43 +23,43 @@ enum FileType {
     Mcnf,
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     let in_path = PathBuf::from(&std::env::args().nth(1).unwrap_or_else(|| print_usage!()));
     let out_path = PathBuf::from(&std::env::args().nth(2).unwrap_or_else(|| print_usage!()));
 
     match determine_file_type(&in_path) {
         FileType::Cnf => {
-            let mut inst = instances::SatInstance::<BasicVarManager>::from_dimacs_path(in_path)
-                .expect("Could not parse CNF");
-            let n_vars = inst.var_manager().n_used();
+            let inst = instances::SatInstance::<BasicVarManager>::from_dimacs_path(in_path)
+                .context("Could not parse CNF")?;
+            let n_vars = inst.n_vars();
             let rand_reindexer = RandReindVarManager::init(n_vars);
             inst.reindex(rand_reindexer)
                 .shuffle()
-                .to_dimacs_path(out_path)
-                .expect("Could not write CNF");
+                .write_dimacs_path(out_path)
+                .context("Could not write CNF")?;
         }
         FileType::Wcnf => {
-            let mut inst = instances::OptInstance::<BasicVarManager>::from_dimacs_path(in_path)
-                .expect("Could not parse WCNF");
-            let n_vars = inst.get_constraints().var_manager().n_used();
+            let inst = instances::OptInstance::<BasicVarManager>::from_dimacs_path(in_path)
+                .context("Could not parse WCNF")?;
+            let n_vars = inst.constraints_ref().n_vars();
             let rand_reindexer = RandReindVarManager::init(n_vars);
             inst.reindex(rand_reindexer)
                 .shuffle()
-                .to_dimacs_path(out_path)
-                .expect("Could not write WCNF");
+                .write_dimacs_path(out_path)
+                .context("Could not write WCNF")?;
         }
         FileType::Mcnf => {
-            let mut inst =
-                instances::MultiOptInstance::<BasicVarManager>::from_dimacs_path(in_path)
-                    .expect("Could not parse MCNF");
-            let n_vars = inst.get_constraints().var_manager().n_used();
+            let inst = instances::MultiOptInstance::<BasicVarManager>::from_dimacs_path(in_path)
+                .context("Could not parse MCNF")?;
+            let n_vars = inst.constraints_ref().n_vars();
             let rand_reindexer = RandReindVarManager::init(n_vars);
             inst.reindex(rand_reindexer)
                 .shuffle()
-                .to_dimacs_path(out_path)
-                .expect("Could not write MCNF");
+                .write_dimacs_path(out_path)
+                .context("Could not write MCNF")?;
         }
     }
+    Ok(())
 }
 
 macro_rules! is_one_of {
diff --git a/tools/src/bin/wcnf2opb.rs b/tools/src/bin/wcnf2opb.rs
index 115ee609..6be8aea7 100644
--- a/tools/src/bin/wcnf2opb.rs
+++ b/tools/src/bin/wcnf2opb.rs
@@ -2,6 +2,7 @@
 //!
 //! A small tool for converting DIMACS WCNF files to OPB.
 
+use anyhow::Context;
 use clap::Parser;
 use rustsat::instances::{fio::opb::Options as OpbOptions, OptInstance};
 use std::{io, path::PathBuf};
@@ -21,7 +22,7 @@ struct Args {
     avoid_negated_lits: bool,
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     let args = Args::parse();
     let opb_opts = OpbOptions {
         first_var_idx: args.first_var_idx,
@@ -29,16 +30,22 @@ fn main() {
     };
 
     let inst: OptInstance = if let Some(in_path) = args.in_path {
-        OptInstance::from_dimacs_path(in_path).expect("error parsing the input file")
+        OptInstance::from_dimacs_path(in_path).context("error parsing the input file")?
     } else {
-        OptInstance::from_dimacs(io::stdin()).expect("error parsing input")
+        OptInstance::from_dimacs(io::BufReader::new(io::stdin())).context("error parsing input")?
     };
 
+    let (mut constr, mut obj) = inst.decompose();
+    let hardened = obj.convert_to_soft_lits(constr.var_manager_mut());
+    constr.extend(hardened.into());
+    let inst = OptInstance::compose(constr, obj);
+
     if let Some(out_path) = args.out_path {
-        inst.to_opb_path(out_path, opb_opts)
-            .expect("io error writing the output file");
+        inst.write_opb_path(out_path, opb_opts)
+            .context("error writing the output file")?;
     } else {
-        inst.to_opb(&mut io::stdout(), opb_opts)
-            .expect("io error writing to stdout");
+        inst.write_opb(&mut io::stdout(), opb_opts)
+            .context("io error writing to stdout")?;
     };
+    Ok(())
 }
diff --git a/tools/src/encodings/clustering.rs b/tools/src/encodings/clustering.rs
index 00b1387b..d8b078f8 100644
--- a/tools/src/encodings/clustering.rs
+++ b/tools/src/encodings/clustering.rs
@@ -123,24 +123,6 @@ impl Default for VarManager {
     }
 }
 
-#[derive(Debug)]
-pub enum Error {
-    Io(io::Error),
-    Parsing(String),
-}
-
-impl From<io::Error> for Error {
-    fn from(value: io::Error) -> Self {
-        Error::Io(value)
-    }
-}
-
-impl From<nom::Err<nom::error::Error<&str>>> for Error {
-    fn from(value: nom::Err<nom::error::Error<&str>>) -> Self {
-        Error::Parsing(value.to_string())
-    }
-}
-
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
 pub enum Similarity {
     Similar(usize),
@@ -179,7 +161,7 @@ impl Encoding {
         in_reader: R,
         variant: Variant,
         sim_map: Map,
-    ) -> Result<Self, Error> {
+    ) -> anyhow::Result<Self> {
         if variant != Variant::Binary {
             panic!("only the binary encoding is implemented so far");
         }
@@ -187,7 +169,7 @@ impl Encoding {
         let mut ident_map = RsHashMap::default();
         let mut next_idx: u32 = 0;
         let process_line =
-            |line: Result<String, io::Error>| -> Option<Result<(String, String, f64), Error>> {
+            |line: Result<String, io::Error>| -> Option<anyhow::Result<(String, String, f64)>> {
                 let line = line.ok()?;
                 let line = line.trim_start();
                 if line.starts_with('%') {


Test patch:
diff --git a/rustsat/tests/compression.rs b/rustsat/tests/compression.rs
index 36f88f7e..cb131106 100644
--- a/rustsat/tests/compression.rs
+++ b/rustsat/tests/compression.rs
@@ -9,7 +9,7 @@ fn small_sat_instance_gzip() {
     let inst: SatInstance<BasicVarManager> =
         SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.gz").unwrap();
     let mut solver = rustsat_minisat::core::Minisat::default();
-    solver.add_cnf(inst.as_cnf().0).unwrap();
+    solver.add_cnf(inst.into_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Sat);
 }
@@ -22,7 +22,7 @@ fn small_unsat_instance_gzip() {
     )
     .unwrap();
     let mut solver = rustsat_minisat::core::Minisat::default();
-    solver.add_cnf(inst.as_cnf().0).unwrap();
+    solver.add_cnf(inst.into_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Unsat);
 }
@@ -32,7 +32,7 @@ fn small_sat_instance_bz2() {
     let inst: SatInstance<BasicVarManager> =
         SatInstance::from_dimacs_path("./data/AProVE11-12.cnf.bz2").unwrap();
     let mut solver = rustsat_minisat::core::Minisat::default();
-    solver.add_cnf(inst.as_cnf().0).unwrap();
+    solver.add_cnf(inst.into_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Sat);
 }
@@ -45,7 +45,7 @@ fn small_unsat_instance_bz2() {
     )
     .unwrap();
     let mut solver = rustsat_minisat::core::Minisat::default();
-    solver.add_cnf(inst.as_cnf().0).unwrap();
+    solver.add_cnf(inst.into_cnf().0).unwrap();
     let res = solver.solve().unwrap();
     assert_eq!(res, SolverResult::Unsat);
 }
diff --git a/rustsat/tests/constraints.rs b/rustsat/tests/constraints.rs
index 37aa58e7..1fc3c206 100644
--- a/rustsat/tests/constraints.rs
+++ b/rustsat/tests/constraints.rs
@@ -12,7 +12,7 @@ macro_rules! test_card {
     ( $constr:expr, $sat_assump:expr, $unsat_assump:expr ) => {{
         let mut inst: SatInstance = SatInstance::new();
         inst.add_card_constr($constr);
-        let (cnf, _) = inst.as_cnf();
+        let (cnf, _) = inst.into_cnf();
         println!("{:?}", cnf);
         let mut solver = rustsat_tools::Solver::default();
         solver.add_cnf(cnf).unwrap();
@@ -31,7 +31,7 @@ macro_rules! test_pb {
     ( $constr:expr, $sat_assump:expr, $unsat_assump:expr ) => {{
         let mut inst: SatInstance = SatInstance::new();
         inst.add_pb_constr($constr);
-        let (cnf, _) = inst.as_cnf();
+        let (cnf, _) = inst.into_cnf();
         println!("{:?}", cnf);
         let mut solver = rustsat_tools::Solver::default();
         solver.add_cnf(cnf).unwrap();
diff --git a/rustsat/tests/opb.rs b/rustsat/tests/opb.rs
index f0ccdc5a..8f18f8bc 100644
--- a/rustsat/tests/opb.rs
+++ b/rustsat/tests/opb.rs
@@ -14,7 +14,7 @@ use rustsat::{
 macro_rules! opb_test {
     ($path:expr, $expect:expr) => {{
         let inst: SatInstance = SatInstance::from_opb_path($path, Options::default()).unwrap();
-        let (cnf, _) = inst.as_cnf();
+        let (cnf, _) = inst.into_cnf();
         println!("{:?}", cnf);
         let mut solver = rustsat_minisat::core::Minisat::default();
         solver.add_cnf(cnf).unwrap();
diff --git a/solvertests/src/integration.rs b/solvertests/src/integration.rs
index 67aefabd..f3dee2ee 100644
--- a/solvertests/src/integration.rs
+++ b/solvertests/src/integration.rs
@@ -21,7 +21,7 @@ pub fn base(input: MacroInput) -> TokenStream {
                 let mut solver = <$slv>::default();
                 let inst = rustsat::instances::SatInstance::<rustsat::instances::BasicVarManager>::from_dimacs_path($inst)
                     .expect("failed to parse instance");
-                rustsat::solvers::Solve::add_cnf(&mut solver, inst.as_cnf().0)
+                rustsat::solvers::Solve::add_cnf(&mut solver, inst.into_cnf().0)
                     .expect("failed to add cnf to solver");
                 let res = rustsat::solvers::Solve::solve(&mut solver).expect("failed solving");
                 assert_eq!(res, $res);
@@ -30,7 +30,7 @@ pub fn base(input: MacroInput) -> TokenStream {
                 let mut solver = $init;
                 let inst = rustsat::instances::SatInstance::<rustsat::instances::BasicVarManager>::from_dimacs_path($inst)
                     .expect("failed to parse instance");
-                rustsat::solvers::Solve::add_cnf(&mut solver, inst.as_cnf().0)
+                rustsat::solvers::Solve::add_cnf(&mut solver, inst.into_cnf().0)
                     .expect("failed to add cnf to solver");
                 let res = rustsat::solvers::Solve::solve(&mut solver).expect("failed solving");
                 assert_eq!(res, $res);
@@ -97,7 +97,7 @@ pub fn incremental(input: MacroInput) -> TokenStream {
             let mut solver = init_slv!(#slv);
             let inst: SatInstance =
                 SatInstance::from_dimacs_path("./data/small.cnf").unwrap();
-            solver.add_cnf(inst.as_cnf().0).unwrap();
+            solver.add_cnf(inst.into_cnf().0).unwrap();
             let res = solver.solve().unwrap();
             assert_eq!(res, Sat);
             let res = solver.solve_assumps(&[!lit![0], !lit![1]]).unwrap();
@@ -205,7 +205,7 @@ pub fn phasing(input: MacroInput) -> TokenStream {
             let mut solver = init_slv!(#slv);
             let inst: SatInstance =
                 SatInstance::from_dimacs_path("./data/small.cnf").unwrap();
-            solver.add_cnf(inst.as_cnf().0).unwrap();
+            solver.add_cnf(inst.into_cnf().0).unwrap();
             solver.phase_lit(lit![0]).unwrap();
             solver.phase_lit(!lit![1]).unwrap();
             solver.phase_lit(lit![2]).unwrap();