Repository: chrjabs/rustsat (language: python)

Issue:
Add parser for OPB
This includes adding inequality constraints to SAT instances.
Split out from #3


Discussion / hints:

Fix patch:
diff --git a/data/tiny-opt.opb b/data/tiny-opt.opb
new file mode 100644
index 00000000..1407c482
--- /dev/null
+++ b/data/tiny-opt.opb
@@ -0,0 +1,6 @@
+* A handwritten OPB sat instance for basic testing
+min: 1 x0 2 x1;
+min: 2 x2 -3 ~x3;
+5 x0 -3 x1 >= 4;
+5 x2 -3 x3 >= 2;
+5 ~x3 >= 4;
diff --git a/data/tiny-sat.opb b/data/tiny-sat.opb
new file mode 100644
index 00000000..4dfde6d4
--- /dev/null
+++ b/data/tiny-sat.opb
@@ -0,0 +1,4 @@
+* A handwritten OPB sat instance for basic testing
+5 x0 -3 x1 >= 4;
+5 x2 -3 x3 >= 2;
+5 ~x3 >= 4;
diff --git a/data/tiny-unsat.opb b/data/tiny-unsat.opb
new file mode 100644
index 00000000..12470f18
--- /dev/null
+++ b/data/tiny-unsat.opb
@@ -0,0 +1,5 @@
+* A handwritten OPB sat instance for basic testing
+5 x0 -3 x1 >= 4;
+5 x2 -3 x3 >= 2;
+5 ~x3 >= 4;
+3 ~x0 >= 2;
diff --git a/src/encodings/card.rs b/src/encodings/card.rs
index 775dc4c5..be2f3fc3 100644
--- a/src/encodings/card.rs
+++ b/src/encodings/card.rs
@@ -40,7 +40,10 @@
 use super::EncodingError;
 use crate::{
     instances::{ManageVars, CNF},
-    types::Lit,
+    types::{
+        constraints::{CardConstraint, CardEQConstr, CardLBConstr, CardUBConstr},
+        Clause, Lit,
+    },
 };
 
 mod totalizer;
@@ -88,6 +91,24 @@ pub trait UBCard: EncodeCard {
     /// and nothing has been called afterwards, otherwise
     /// [`EncodingError::NotEncoded`] will be returned.
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, EncodingError>;
+    /// Encodes an upper bound cardinality constraint to CNF
+    fn encode_ub_constr(
+        constr: CardUBConstr,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<CNF, EncodingError>
+    where
+        Self: Sized,
+    {
+        let mut enc = Self::new();
+        let (lits, ub) = constr.decompose();
+        enc.add(lits);
+        let mut cnf = enc.encode_ub(ub, ub, var_manager)?;
+        enc.enforce_ub(ub)
+            .unwrap()
+            .into_iter()
+            .for_each(|unit| cnf.add_unit(unit));
+        Ok(cnf)
+    }
 }
 
 /// Trait for cardinality encodings that allow upper bounding of the form `sum
@@ -111,6 +132,24 @@ pub trait LBCard: EncodeCard {
     /// the number of literals in the encoding, [`EncodingError::Unsat`] is
     /// returned.
     fn enforce_lb(&self, lb: usize) -> Result<Vec<Lit>, EncodingError>;
+    /// Encodes a lower bound cardinality constraint to CNF
+    fn encode_lb_constr(
+        constr: CardLBConstr,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<CNF, EncodingError>
+    where
+        Self: Sized,
+    {
+        let mut enc = Self::new();
+        let (lits, lb) = constr.decompose();
+        enc.add(lits);
+        let mut cnf = enc.encode_lb(lb, lb, var_manager)?;
+        enc.enforce_lb(lb)
+            .unwrap()
+            .into_iter()
+            .for_each(|unit| cnf.add_unit(unit));
+        Ok(cnf)
+    }
 }
 
 /// Trait for cardinality encodings that allow upper and lower bounding
@@ -142,6 +181,38 @@ pub trait BothBCard: UBCard + LBCard {
         assumps.extend(self.enforce_lb(b)?);
         Ok(assumps)
     }
+    /// Encodes an equality cardinality constraint to CNF
+    fn encode_eq_constr(
+        constr: CardEQConstr,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<CNF, EncodingError>
+    where
+        Self: Sized,
+    {
+        let mut enc = Self::new();
+        let (lits, b) = constr.decompose();
+        enc.add(lits);
+        let mut cnf = enc.encode_both(b, b, var_manager)?;
+        enc.enforce_eq(b)
+            .unwrap()
+            .into_iter()
+            .for_each(|unit| cnf.add_unit(unit));
+        Ok(cnf)
+    }
+    /// Encodes any cardinality constraint to CNF
+    fn encode_constr(
+        constr: CardConstraint,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<CNF, EncodingError>
+    where
+        Self: Sized,
+    {
+        match constr {
+            CardConstraint::UB(constr) => Self::encode_ub_constr(constr, var_manager),
+            CardConstraint::LB(constr) => Self::encode_lb_constr(constr, var_manager),
+            CardConstraint::EQ(constr) => Self::encode_eq_constr(constr, var_manager),
+        }
+    }
 }
 
 /// Trait for all cardinality encodings of form `sum of lits <> rhs`
@@ -252,3 +323,32 @@ pub fn new_default_inc_lb() -> Box<dyn LBCard> {
 pub fn new_default_inc_both() -> Box<dyn BothBCard> {
     Box::new(Totalizer::new())
 }
+
+/// A default encoder for any cardinality constraint.
+/// This uses a [`Totalizer`] to encode non-trivial constraints.
+pub fn default_encode_cardinality_constraint(
+    constr: CardConstraint,
+    var_manager: &mut dyn ManageVars,
+) -> CNF {
+    if constr.is_tautology() {
+        return CNF::new();
+    }
+    if constr.is_unsat() {
+        let mut cnf = CNF::new();
+        cnf.add_clause(Clause::new());
+        return cnf;
+    }
+    if constr.is_assignment() {
+        let mut cnf = CNF::new();
+        let lits = constr.into_lits();
+        lits.into_iter().for_each(|l| cnf.add_unit(l));
+        return cnf;
+    }
+    if constr.is_clause() {
+        let lits = constr.into_lits();
+        let mut cnf = CNF::new();
+        cnf.add_clause(Clause::from(lits.into_iter()));
+        return cnf;
+    }
+    Totalizer::encode_constr(constr, var_manager).unwrap()
+}
diff --git a/src/encodings/pb.rs b/src/encodings/pb.rs
index 49d3655e..febea367 100644
--- a/src/encodings/pb.rs
+++ b/src/encodings/pb.rs
@@ -44,10 +44,13 @@
 //! assert_eq!(res, SolverResult::UNSAT);
 //! ```
 
-use super::EncodingError;
+use super::{card, EncodingError};
 use crate::{
     instances::{ManageVars, CNF},
-    types::Lit,
+    types::{
+        constraints::{PBConstraint, PBEQConstr, PBLBConstr, PBUBConstr},
+        Clause, Lit,
+    },
 };
 use std::collections::HashMap;
 
@@ -99,6 +102,29 @@ pub trait UBPB: EncodePB {
     /// adequately and nothing has been called afterwards, otherwise
     /// [`EncodingError::NotEncoded`] will be returned.
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, EncodingError>;
+    /// Encodes an upper bound pseudo-boolean constraint to CNF
+    fn encode_ub_constr(
+        constr: PBUBConstr,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<CNF, EncodingError>
+    where
+        Self: Sized,
+    {
+        let mut enc = Self::new();
+        let (lits, ub) = constr.decompose();
+        let ub = if ub < 0 {
+            return Err(EncodingError::Unsat);
+        } else {
+            ub as usize
+        };
+        enc.add(lits);
+        let mut cnf = enc.encode_ub(ub, ub, var_manager)?;
+        enc.enforce_ub(ub)
+            .unwrap()
+            .into_iter()
+            .for_each(|unit| cnf.add_unit(unit));
+        Ok(cnf)
+    }
 }
 
 /// Trait for pseudo-boolean encodings that allow upper bounding of the form `sum
@@ -122,6 +148,29 @@ pub trait LBPB: EncodePB {
     /// the weighted sum of literals in the encoding, [`EncodingError::Unsat`]
     /// is returned.
     fn enforce_lb(&self, lb: usize) -> Result<Vec<Lit>, EncodingError>;
+    /// Encodes a lower bound pseudo-boolean constraint to CNF
+    fn encode_lb_constr(
+        constr: PBLBConstr,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<CNF, EncodingError>
+    where
+        Self: Sized,
+    {
+        let mut enc = Self::new();
+        let (lits, lb) = constr.decompose();
+        let lb = if lb < 0 {
+            return Ok(CNF::new()); // tautology
+        } else {
+            lb as usize
+        };
+        enc.add(lits);
+        let mut cnf = enc.encode_lb(lb, lb, var_manager)?;
+        enc.enforce_lb(lb)
+            .unwrap()
+            .into_iter()
+            .for_each(|unit| cnf.add_unit(unit));
+        Ok(cnf)
+    }
 }
 
 /// Trait for pseudo-boolean encodings that allow upper and lower bounding
@@ -153,6 +202,43 @@ pub trait BothBPB: UBPB + LBPB {
         assumps.extend(self.enforce_lb(b)?);
         Ok(assumps)
     }
+    /// Encodes an equality pseudo-boolean constraint to CNF
+    fn encode_eq_constr(
+        constr: PBEQConstr,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<CNF, EncodingError>
+    where
+        Self: Sized,
+    {
+        let mut enc = Self::new();
+        let (lits, b) = constr.decompose();
+        let b = if b < 0 {
+            return Err(EncodingError::Unsat);
+        } else {
+            b as usize
+        };
+        enc.add(lits);
+        let mut cnf = enc.encode_both(b, b, var_manager)?;
+        enc.enforce_eq(b)
+            .unwrap()
+            .into_iter()
+            .for_each(|unit| cnf.add_unit(unit));
+        Ok(cnf)
+    }
+    /// Encodes any pseudo-boolean constraint to CNF
+    fn encode_constr(
+        constr: PBConstraint,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<CNF, EncodingError>
+    where
+        Self: Sized,
+    {
+        match constr {
+            PBConstraint::UB(constr) => Self::encode_ub_constr(constr, var_manager),
+            PBConstraint::LB(constr) => Self::encode_lb_constr(constr, var_manager),
+            PBConstraint::EQ(constr) => Self::encode_eq_constr(constr, var_manager),
+        }
+    }
 }
 
 /// Trait for all pseudo-boolean encodings of form `sum of lits <> rhs`
@@ -263,3 +349,28 @@ pub fn new_default_inc_lb() -> Box<dyn LBPB> {
 pub fn new_default_inc_both() -> Box<dyn BothBPB> {
     Box::new(DoubleGeneralizedTotalizer::new())
 }
+
+/// A default encoder for any pseudo-boolean constraint. This uses a
+/// [`DoubleGeneralizedTotalizer`] to encode true pseudo-boolean constraints and
+/// [`card::default_encode_cardinality_constraint`] for cardinality constraints.
+pub fn default_encode_pb_constraint(constr: PBConstraint, var_manager: &mut dyn ManageVars) -> CNF {
+    if constr.is_tautology() {
+        return CNF::new();
+    }
+    if constr.is_unsat() {
+        let mut cnf = CNF::new();
+        cnf.add_clause(Clause::new());
+        return cnf;
+    }
+    if constr.is_assignment() {
+        let mut cnf = CNF::new();
+        let lits = constr.into_lits();
+        lits.into_iter().for_each(|(l, _)| cnf.add_unit(l));
+        return cnf;
+    }
+    if constr.is_card() {
+        let card = constr.as_card_constr().unwrap();
+        return card::default_encode_cardinality_constraint(card, var_manager);
+    }
+    DoubleGeneralizedTotalizer::encode_constr(constr, var_manager).unwrap()
+}
diff --git a/src/instances.rs b/src/instances.rs
index ab983e75..b796d1fb 100644
--- a/src/instances.rs
+++ b/src/instances.rs
@@ -18,7 +18,11 @@ use std::{
 
 use crate::{
     clause,
-    types::{Clause, Lit, Var},
+    encodings::{card, pb},
+    types::{
+        constraints::{CardConstraint, PBConstraint},
+        Clause, Lit, Var,
+    },
 };
 
 #[cfg(feature = "compression")]
@@ -28,9 +32,14 @@ use flate2::read::GzDecoder;
 #[cfg(feature = "compression")]
 use std::ffi::OsStr;
 
+/// DIMACS parsing module
 mod dimacs;
 pub use dimacs::DimacsError;
 
+/// OPB parsing module
+mod opb;
+pub use opb::OpbError;
+
 /// Combined Parsing Errors
 #[derive(Debug)]
 pub enum ParsingError {
@@ -38,6 +47,8 @@ pub enum ParsingError {
     IO(std::io::Error),
     /// Dimacs Parsing Error
     Dimacs(DimacsError),
+    /// OPB Parsing Error
+    Opb(OpbError),
 }
 
 impl fmt::Display for ParsingError {
@@ -45,6 +56,7 @@ impl fmt::Display for ParsingError {
         match self {
             ParsingError::IO(ioe) => write!(f, "IO error: {}", ioe),
             ParsingError::Dimacs(de) => write!(f, "Dimacs error: {}", de),
+            ParsingError::Opb(oe) => write!(f, "OPB error: {}", oe),
         }
     }
 }
@@ -91,6 +103,21 @@ impl CNF {
         self.clauses.push(clause);
     }
 
+    /// Adds a unit clause to the CNF
+    pub fn add_unit(&mut self, unit: Lit) {
+        self.add_clause(clause![unit])
+    }
+
+    /// Adds a binary clause to the CNF
+    pub fn add_binary(&mut self, lit1: Lit, lit2: Lit) {
+        self.add_clause(clause![lit1, lit2])
+    }
+
+    /// Adds a ternary clause to the CNF
+    pub fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) {
+        self.add_clause(clause![lit1, lit2, lit3])
+    }
+
     /// Returns the number of clauses in the instance
     pub fn n_clauses(&self) -> usize {
         self.clauses.len()
@@ -187,11 +214,13 @@ impl IntoIterator for CNF {
     }
 }
 
-/// Type representing a satisfiability instance.
-/// For now this only supports clausal constraints, but more will be added.
+/// Type representing a satisfiability instance. Supported constraints are
+/// clauses, cardinality constraints and pseudo-boolean constraints.
 #[derive(Clone, Debug, PartialEq)]
 pub struct SatInstance<VM: ManageVars = BasicVarManager> {
     cnf: CNF,
+    cards: Vec<CardConstraint>,
+    pbs: Vec<PBConstraint>,
     var_manager: VM,
 }
 
@@ -200,6 +229,8 @@ impl<VM: ManageVars> SatInstance<VM> {
     pub fn new() -> SatInstance<VM> {
         SatInstance {
             cnf: CNF::new(),
+            cards: vec![],
+            pbs: vec![],
             var_manager: VM::new(),
         }
     }
@@ -208,12 +239,13 @@ impl<VM: ManageVars> SatInstance<VM> {
     pub fn new_with_manager(var_manager: VM) -> Self {
         SatInstance {
             cnf: CNF::new(),
+            cards: vec![],
+            pbs: vec![],
             var_manager,
         }
     }
 
-    /// Parse a DIMACS instance from a reader object with a specific variable
-    /// manager.
+    /// Parses a DIMACS instance from a reader object.
     ///
     /// # File Format
     ///
@@ -235,8 +267,9 @@ impl<VM: ManageVars> SatInstance<VM> {
         }
     }
 
-    /// Parse a DIMACS instance from a file path with a specific variable
-    /// manager. For more details see [`SatInstance::from_dimacs_reader`].
+    /// Parses a DIMACS instance from a file path. For more details see
+    /// [`SatInstance::from_dimacs_reader`]. With feature `compression` supports
+    /// bzip2 and gzip compression, detected by the file extension.
     pub fn from_dimacs_path(path: &Path) -> Result<Self, ParsingError> {
         match open_compressed_uncompressed(path) {
             Err(why) => Err(ParsingError::IO(why)),
@@ -244,6 +277,38 @@ impl<VM: ManageVars> SatInstance<VM> {
         }
     }
 
+    /// Parses an OPB instance from a reader object.
+    ///
+    /// # File Format
+    ///
+    /// 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_reader<R: Read>(reader: R) -> Result<Self, ParsingError> {
+        match opb::parse_sat(reader) {
+            Err(opb_error) => Err(ParsingError::Opb(opb_error)),
+            Ok(inst) => {
+                let inst = inst.change_var_manager(|mut vm| {
+                    let nfv = vm.next_free();
+                    let mut vm2 = VM::new();
+                    vm2.increase_next_free(nfv);
+                    vm2
+                });
+                Ok(inst)
+            }
+        }
+    }
+
+    /// Parses an OPB instance from a file path. For more details see
+    /// [`SatInstance::from_opb_reader`]. With feature `compression` supports
+    /// bzip2 and gzip compression, detected by the file extension.
+    pub fn from_opb_path(path: &Path) -> Result<Self, ParsingError> {
+        match open_compressed_uncompressed(path) {
+            Err(why) => Err(ParsingError::IO(why)),
+            Ok(reader) => SatInstance::from_opb_reader(reader),
+        }
+    }
+
     /// Returns the number of clauses in the instance
     pub fn n_clauses(&self) -> usize {
         self.cnf.n_clauses()
@@ -252,56 +317,129 @@ impl<VM: ManageVars> SatInstance<VM> {
     /// Adds a clause to the instance
     pub fn add_clause(&mut self, cl: Clause) {
         cl.iter().for_each(|l| {
-            self.var_manager.increase_next_free(l.var());
+            self.var_manager.mark_used(l.var());
         });
         self.cnf.add_clause(cl);
     }
 
+    /// Adds a unit clause to the instance
+    pub fn add_unit(&mut self, unit: Lit) {
+        self.add_clause(clause![unit])
+    }
+
+    /// Adds a binary clause to the instance
+    pub fn add_binary(&mut self, lit1: Lit, lit2: Lit) {
+        self.add_clause(clause![lit1, lit2])
+    }
+
+    /// Adds a ternary clause to the instance
+    pub fn add_ternary(&mut self, lit1: Lit, lit2: Lit, lit3: Lit) {
+        self.add_clause(clause![lit1, lit2, lit3])
+    }
+
     /// Adds an implication of form (a -> b) to the instance
     pub fn add_lit_impl_lit(&mut self, a: Lit, b: Lit) {
+        self.var_manager.mark_used(a.var());
+        self.var_manager.mark_used(b.var());
         self.cnf.add_lit_impl_lit(a, b);
     }
 
     /// Adds an implication of form a -> (b1 | b2 | ... | bm)
     pub fn add_lit_impl_clause(&mut self, a: Lit, b: Vec<Lit>) {
+        self.var_manager.mark_used(a.var());
+        b.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
         self.cnf.add_lit_impl_clause(a, b);
     }
 
     /// Adds an implication of form a -> (b1 & b2 & ... & bm)
     pub fn add_lit_impl_cube(&mut self, a: Lit, b: Vec<Lit>) {
+        self.var_manager.mark_used(a.var());
+        b.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
         self.cnf.add_lit_impl_cube(a, b);
     }
 
     /// Adds an implication of form (a1 & a2 & ... & an) -> b
     pub fn add_cube_impl_lit(&mut self, a: Vec<Lit>, b: Lit) {
+        a.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
+        self.var_manager.mark_used(b.var());
         self.cnf.add_cube_impl_lit(a, b);
     }
 
     /// Adds an implication of form (a1 | a2 | ... | an) -> b
     pub fn add_clause_impl_lit(&mut self, a: Vec<Lit>, b: Lit) {
+        a.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
+        self.var_manager.mark_used(b.var());
         self.cnf.add_clause_impl_lit(a, b);
     }
 
     /// Adds an implication of form (a1 & a2 & ... & an) -> (b1 | b2 | ... | bm)
     pub fn add_cube_impl_clause(&mut self, a: Vec<Lit>, b: Vec<Lit>) {
+        a.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
+        b.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
         self.cnf.add_cube_impl_clause(a, b);
     }
 
     /// Adds an implication of form (a1 | a2 | ... | an) -> (b1 | b2 | ... | bm)
     pub fn add_clause_impl_clause(&mut self, a: Vec<Lit>, b: Vec<Lit>) {
+        a.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
+        b.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
         self.cnf.add_clause_impl_clause(a, b);
     }
 
     /// Adds an implication of form (a1 | a2 | ... | an) -> (b1 & b2 & ... & bm)
     pub fn add_clause_impl_cube(&mut self, a: Vec<Lit>, b: Vec<Lit>) {
+        a.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
+        b.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
         self.cnf.add_clause_impl_cube(a, b);
     }
 
     /// Adds an implication of form (a1 & a2 & ... & an) -> (b1 & b2 & ... & bm)
     pub fn add_cube_impl_cube(&mut self, a: Vec<Lit>, b: Vec<Lit>) {
+        a.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
+        b.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
         self.cnf.add_cube_impl_cube(a, b);
     }
 
+    /// Adds a cardinality constraint
+    pub fn add_card_constr(&mut self, card: CardConstraint) {
+        card.iter().for_each(|l| {
+            self.var_manager.mark_used(l.var());
+        });
+        self.cards.push(card)
+    }
+
+    /// Adds a cardinality constraint
+    pub fn add_pb_constr(&mut self, pb: PBConstraint) {
+        pb.iter().for_each(|(l, _)| {
+            self.var_manager.mark_used(l.var());
+        });
+        self.pbs.push(pb)
+    }
+
     /// Get a reference to the variable manager
     pub fn var_manager(&mut self) -> &mut VM {
         &mut self.var_manager
@@ -315,12 +453,38 @@ impl<VM: ManageVars> SatInstance<VM> {
     {
         SatInstance {
             cnf: self.cnf,
+            cards: self.cards,
+            pbs: self.pbs,
             var_manager: vm_converter(self.var_manager),
         }
     }
 
-    /// Converts the instance to a set of clauses
+    /// Converts the instance to a set of clauses.
+    /// Uses the default encoders from the `encodings` module.
     pub fn as_cnf(self) -> (CNF, VM) {
+        self.as_cnf_with_encoders(
+            card::default_encode_cardinality_constraint,
+            pb::default_encode_pb_constraint,
+        )
+    }
+
+    /// Converts the instance to a set of clauses with explicitly specified
+    /// converters for non-clausal constraints.
+    pub fn as_cnf_with_encoders<CardEnc, PBEnc>(
+        mut self,
+        mut card_encoder: CardEnc,
+        mut pb_encoder: PBEnc,
+    ) -> (CNF, VM)
+    where
+        CardEnc: FnMut(CardConstraint, &mut dyn ManageVars) -> CNF,
+        PBEnc: FnMut(PBConstraint, &mut dyn ManageVars) -> CNF,
+    {
+        self.cards
+            .into_iter()
+            .for_each(|constr| self.cnf.extend(card_encoder(constr, &mut self.var_manager)));
+        self.pbs
+            .into_iter()
+            .for_each(|constr| self.cnf.extend(pb_encoder(constr, &mut self.var_manager)));
         (self.cnf, self.var_manager)
     }
 
@@ -334,10 +498,12 @@ impl<VM: ManageVars> SatInstance<VM> {
 #[cfg(feature = "optimization")]
 /// Type representing an optimization objective.
 /// This type currently supports soft clauses and soft literals.
+/// All objectives are considered minimization objectives.
 #[derive(Clone, Debug, PartialEq)]
 pub struct Objective {
     soft_lits: HashMap<Lit, usize>,
     soft_clauses: HashMap<Clause, usize>,
+    offset: isize,
 }
 
 #[cfg(feature = "optimization")]
@@ -347,14 +513,42 @@ impl Objective {
         Objective {
             soft_lits: HashMap::new(),
             soft_clauses: HashMap::new(),
+            offset: 0,
         }
     }
 
+    /// Sets the value offset
+    pub fn set_offset(&mut self, offset: isize) {
+        self.offset = offset
+    }
+
+    /// Gets the global value offset
+    pub fn offset(&self) -> isize {
+        self.offset
+    }
+
+    /// Increases the value offset
+    pub fn increase_offset(&mut self, offset_incr: isize) {
+        self.offset += offset_incr
+    }
+
     /// Adds a soft literal or updates its weight
     pub fn add_soft_lit(&mut self, w: usize, l: Lit) {
         self.soft_lits.insert(l, w);
     }
 
+    /// Add a soft literal with negative weight. Internally all weights are
+    /// positive, negative weights are represented by a global value offset and
+    /// negated literals.
+    pub fn add_soft_lit_int(&mut self, w: isize, l: Lit) {
+        if w < 0 {
+            self.increase_offset(w);
+            self.add_soft_lit(-w as usize, !l);
+        } else {
+            self.add_soft_lit(w as usize, l);
+        }
+    }
+
     /// Adds a soft clause or updates its weight
     pub fn add_soft_clause(&mut self, w: usize, cl: Clause) {
         if cl.len() == 1 {
@@ -435,7 +629,7 @@ impl<VM: ManageVars> OptInstance<VM> {
         (self.constr, self.obj)
     }
 
-    /// Parse a DIMACS instance from a reader object.
+    /// Parses a DIMACS instance from a reader object.
     ///
     /// # File Format
     ///
@@ -459,8 +653,9 @@ impl<VM: ManageVars> OptInstance<VM> {
         }
     }
 
-    /// Parse a DIMACS instance from a file path. For more details see
-    /// [`OptInstance::from_dimacs_reader`].
+    /// Parses a DIMACS instance from a file path. For more details see
+    /// [`OptInstance::from_dimacs_reader`]. With feature `compression` supports
+    /// bzip2 and gzip compression, detected by the file extension.
     pub fn from_dimacs_path(path: &Path) -> Result<Self, ParsingError> {
         match open_compressed_uncompressed(path) {
             Err(why) => Err(ParsingError::IO(why)),
@@ -468,6 +663,60 @@ impl<VM: ManageVars> OptInstance<VM> {
         }
     }
 
+    /// Parses an OPB instance from a reader object.
+    ///
+    /// # File Format
+    ///
+    /// 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_reader<R: Read>(reader: R) -> Result<Self, ParsingError> {
+        OptInstance::from_opb_reader_with_idx(reader, 0)
+    }
+
+    /// Parses an OPB instance from a reader object, selecting the objective
+    /// with index `obj_idx` if multiple are available. The index starts from 0.
+    /// For more details see [`OptInstance::from_opb_reader`].
+    pub fn from_opb_reader_with_idx<R: Read>(
+        reader: R,
+        obj_idx: usize,
+    ) -> Result<Self, ParsingError> {
+        match opb::parse_opt_with_idx(reader, obj_idx) {
+            Err(opb_error) => Err(ParsingError::Opb(opb_error)),
+            Ok(inst) => {
+                let inst = inst.change_var_manager(|mut vm| {
+                    let nfv = vm.next_free();
+                    let mut vm2 = VM::new();
+                    vm2.increase_next_free(nfv);
+                    vm2
+                });
+                Ok(inst)
+            }
+        }
+    }
+
+    /// Parses an OPB instance from a file path. For more details see
+    /// [`OptInstance::from_opb_reader`]. With feature `compression` supports
+    /// bzip2 and gzip compression, detected by the file extension.
+    pub fn from_opb_path(path: &Path) -> Result<Self, ParsingError> {
+        match open_compressed_uncompressed(path) {
+            Err(why) => Err(ParsingError::IO(why)),
+            Ok(reader) => OptInstance::from_opb_reader(reader),
+        }
+    }
+
+    /// Parses an OPB instance from a file path, selecting the objective with
+    /// index `obj_idx` if multiple are available. The index starts from 0. For
+    /// more details see [`OptInstance::from_opb_reader`]. With feature
+    /// `compression` supports bzip2 and gzip compression, detected by the file
+    /// extension.
+    pub fn from_opb_path_with_idx(path: &Path, obj_idx: usize) -> Result<Self, ParsingError> {
+        match open_compressed_uncompressed(path) {
+            Err(why) => Err(ParsingError::IO(why)),
+            Ok(reader) => OptInstance::from_opb_reader_with_idx(reader, obj_idx),
+        }
+    }
+
     /// Gets a mutable reference to the hard constraints for modifying them
     pub fn get_constraints(&mut self) -> &mut SatInstance<VM> {
         &mut self.constr
@@ -647,7 +896,6 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
         (self.constr, self.objs)
     }
 
-    /// Gets a mutable reference to the hard constraints for modifying them
     /// Parse a DIMACS instance from a reader object.
     ///
     /// # File Format
@@ -688,7 +936,7 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
         }
     }
 
-    /// Parse a DIMACS instance from a file path. For more details see
+    /// Parses a DIMACS instance from a file path. For more details see
     /// [`OptInstance::from_dimacs_reader`].
     pub fn from_dimacs_path(path: &Path) -> Result<Self, ParsingError> {
         match open_compressed_uncompressed(path) {
@@ -697,6 +945,40 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
         }
     }
 
+    /// Parses an OPB instance from a reader object.
+    ///
+    /// # File Format
+    ///
+    /// The file format expected by this parser is the OPB format for
+    /// 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_reader<R: Read>(reader: R) -> Result<Self, ParsingError> {
+        match opb::parse_multi_opt(reader) {
+            Err(opb_error) => Err(ParsingError::Opb(opb_error)),
+            Ok(inst) => {
+                let inst = inst.change_var_manager(|mut vm| {
+                    let nfv = vm.next_free();
+                    let mut vm2 = VM::new();
+                    vm2.increase_next_free(nfv);
+                    vm2
+                });
+                Ok(inst)
+            }
+        }
+    }
+
+    /// Parses an OPB instance from a file path. For more details see
+    /// [`MultiOptInstance::from_opb_reader`]. With feature `compression` supports
+    /// bzip2 and gzip compression, detected by the file extension.
+    pub fn from_opb_path(path: &Path) -> Result<Self, ParsingError> {
+        match open_compressed_uncompressed(path) {
+            Err(why) => Err(ParsingError::IO(why)),
+            Ok(reader) => MultiOptInstance::from_opb_reader(reader),
+        }
+    }
+
+    /// Gets a mutable reference to the hard constraints for modifying them
     pub fn get_constraints(&mut self) -> &mut SatInstance<VM> {
         &mut self.constr
     }
@@ -758,6 +1040,12 @@ pub trait ManageVars {
     /// Returns true if the next free index has been increased and false otherwise.
     fn increase_next_free(&mut self, v: Var) -> bool;
 
+    /// Marks variables up to the given one as used. Returns true if the next
+    /// free index has been increased and false otherwise.
+    fn mark_used(&mut self, v: Var) -> bool {
+        self.increase_next_free(v + 1)
+    }
+
     /// Combines two variable managers.
     /// In case an object is in both object maps, the one of `other` has precedence.
     fn combine(&mut self, other: Self)
diff --git a/src/instances/dimacs.rs b/src/instances/dimacs.rs
index 1267e084..e61ba553 100644
--- a/src/instances/dimacs.rs
+++ b/src/instances/dimacs.rs
@@ -1,8 +1,14 @@
-//! # Parsing DIMACS CNF and WCNF Files
+//! # Parsing DIMACS Files
 //!
 //! Internal module containing functions for parsing DIMACS files.
 //! The approach is to accept input instances, even if they are not technically
 //! in spec, as long as the input is still reasonable.
+//! 
+//! ## References
+//! 
+//! - [DIMACS CNF](http://www.satcompetition.org/2011/format-benchmarks2011.html)
+//! - [DIMACS WCNF pre22](https://maxsat-evaluations.github.io/2017/rules.html#input)
+//! - [DIMACS WCNF post22](https://maxsat-evaluations.github.io/2022/rules.html#input)
 
 use super::SatInstance;
 use crate::types::{Clause, Lit};
diff --git a/src/instances/opb.rs b/src/instances/opb.rs
new file mode 100644
index 00000000..3d668257
--- /dev/null
+++ b/src/instances/opb.rs
@@ -0,0 +1,487 @@
+//! # Parsing OPB Files
+//!
+//! Internal module containing functions for parsing linear OPB files.
+//! The approach is to accept input instances, even if they are not technically
+//! in spec, as long as the input is still reasonable.
+//!
+//! ## References
+//!
+//! - [OPB](https://www.cril.univ-artois.fr/PB12/format.pdf)
+
+use super::SatInstance;
+use crate::types::{constraints::PBConstraint, Lit, Var};
+use nom::{
+    branch::alt,
+    bytes::complete::tag,
+    character::complete::{anychar, i64, line_ending, space0, space1, u64},
+    combinator::{map_res, opt, recognize},
+    error::Error,
+    multi::{many0, many1, many_till},
+    sequence::{pair, tuple},
+    IResult,
+};
+use std::{
+    collections::HashMap,
+    fmt,
+    io::{BufRead, BufReader, Read},
+    num::TryFromIntError,
+};
+
+#[cfg(feature = "multiopt")]
+use super::MultiOptInstance;
+#[cfg(feature = "optimization")]
+use super::{Objective, OptInstance};
+
+/// Errors occuring within the OPB parsing module
+#[derive(Debug, PartialEq, Eq)]
+pub enum OpbError {
+    /// The requested objective does not exist
+    ObjectiveNotFound,
+    /// Encountered an unexpected line in the OPB file
+    InvalidLine(String),
+    /// Error while reading input data
+    IOError,
+}
+
+impl fmt::Display for OpbError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            OpbError::ObjectiveNotFound => write!(f, "No matching objective found in file"),
+            OpbError::InvalidLine(line) => write!(f, "Invalid OPB line: {}", line),
+            OpbError::IOError => write!(f, "Encountered error reading file"),
+        }
+    }
+}
+
+/// Possible relational operators
+#[derive(Debug, PartialEq, Eq)]
+enum OpbOperator {
+    /// <=
+    LE,
+    /// >=
+    GE,
+    /// <
+    LT,
+    /// >
+    GT,
+    /// =
+    EQ,
+}
+
+/// Possible parsing results for comment or constraint or objective
+#[derive(Debug, PartialEq)]
+enum OpbData {
+    /// A comment
+    Cmt(String),
+    /// A constraint
+    Constr(PBConstraint),
+    /// An objective
+    Obj(
+        #[cfg(feature = "optimization")] Objective,
+        #[cfg(not(feature = "optimization"))] String,
+    ),
+}
+
+/// Parses the constraints from an OPB file as a [`SatInstance`]
+pub fn parse_sat<R: Read>(reader: R) -> Result<SatInstance, OpbError> {
+    let data = parse_opb_data(reader)?;
+    let mut inst = SatInstance::new();
+    data.into_iter().for_each(|d| {
+        if let OpbData::Constr(constr) = d {
+            inst.add_pb_constr(constr);
+        }
+    });
+    Ok(inst)
+}
+
+#[cfg(feature = "optimization")]
+/// Parses an OPB file as an [`OptInstance`] using the objective with the given
+/// index (starting from 0).
+pub fn parse_opt_with_idx<R: Read>(reader: R, obj_idx: usize) -> Result<OptInstance, OpbError> {
+    let data = parse_opb_data(reader)?;
+    let mut sat_inst = SatInstance::new();
+    let mut obj_cnt = 0;
+    let obj = data.into_iter().fold(Objective::new(), |o, d| match d {
+        OpbData::Cmt(_) => o,
+        OpbData::Constr(constr) => {
+            sat_inst.add_pb_constr(constr);
+            o
+        }
+        OpbData::Obj(obj) => {
+            obj_cnt += 1;
+            if obj_cnt - 1 == obj_idx {
+                obj
+            } else {
+                o
+            }
+        }
+    });
+    if obj_cnt <= obj_idx {
+        Err(OpbError::ObjectiveNotFound)
+    } else {
+        Ok(OptInstance::compose(sat_inst, obj))
+    }
+}
+
+#[cfg(feature = "multiopt")]
+/// Parses an OPB file as an [`OptInstance`] using the objective with the given
+/// index (starting from 0).
+pub fn parse_multi_opt<R: Read>(reader: R) -> Result<MultiOptInstance, OpbError> {
+    let data = parse_opb_data(reader)?;
+    let mut sat_inst = SatInstance::new();
+    let mut objs = vec![];
+    data.into_iter().for_each(|d| match d {
+        OpbData::Cmt(_) => (),
+        OpbData::Constr(constr) => sat_inst.add_pb_constr(constr),
+        OpbData::Obj(obj) => objs.push(obj),
+    });
+    Ok(MultiOptInstance::compose(sat_inst, objs))
+}
+
+/// Parses all OPB data of a reader
+fn parse_opb_data<R: Read>(reader: R) -> Result<Vec<OpbData>, OpbError> {
+    let mut reader = BufReader::new(reader);
+    let mut buf = String::new();
+    let mut data = vec![];
+    while let Ok(len) = reader.read_line(&mut buf) {
+        if len == 0 {
+            return Ok(data);
+        }
+        match many0(opb_data)(&buf) {
+            Ok((rem, new_data)) => {
+                if rem.len() > 0 {
+                    return Err(OpbError::InvalidLine(buf.clone()));
+                } else {
+                    data.extend(new_data)
+                }
+            }
+            Err(_) => return Err(OpbError::InvalidLine(buf.clone())),
+        }
+        buf.clear();
+    }
+    return Err(OpbError::IOError);
+}
+
+/// Matches an OPB comment
+fn comment(input: &str) -> IResult<&str, &str> {
+    recognize(pair(
+        tag("*"),
+        alt((
+            recognize(many_till(anychar, line_ending)),
+            recognize(many0(anychar)),
+        )),
+    ))(input)
+}
+
+/// Parses an OPB variable
+fn variable(input: &str) -> IResult<&str, Var> {
+    let (input, _) = tag("x")(input)?;
+    map_res(u64, |idx| {
+        let idx = idx.try_into()?;
+        Ok::<Var, TryFromIntError>(Var::new(idx))
+    })(input)
+}
+
+/// Parses a literal. The spec for linear OPB instances only allows for
+/// variables but we allow negated literals with '~' as in non-linear OPB
+/// instances.
+fn literal(input: &str) -> IResult<&str, Lit> {
+    match tag::<_, _, Error<_>>("~")(input) {
+        Ok((input, _)) => map_res(variable, |v| Ok::<_, ()>(v.neg_lit()))(input),
+        Err(_) => map_res(variable, |v| Ok::<_, ()>(v.pos_lit()))(input),
+    }
+}
+
+/// Parses an OPB relational operator. We admit more operators than the spec.
+fn operator(input: &str) -> IResult<&str, OpbOperator> {
+    let (input, op_str) = alt((tag("<="), tag(">="), tag("<"), tag(">"), tag("=")))(input)?;
+    Ok((
+        input,
+        if op_str == "<=" {
+            OpbOperator::LE
+        } else if op_str == ">=" {
+            OpbOperator::GE
+        } else if op_str == "<" {
+            OpbOperator::LT
+        } else if op_str == ">" {
+            OpbOperator::GT
+        } else {
+            OpbOperator::EQ
+        },
+    ))
+}
+
+/// Parses an OPB weight
+fn weight(input: &str) -> IResult<&str, isize> {
+    map_res(i64, |i| i.try_into())(input)
+}
+
+/// Parses an OPB weighted term
+fn weighted_literal(input: &str) -> IResult<&str, (Lit, isize)> {
+    map_res(tuple((weight, space1, literal, space0)), |(w, _, l, _)| {
+        Ok::<_, ()>((l, w))
+    })(input)
+}
+
+/// Parses an OPB sum
+fn weighted_lit_sum(input: &str) -> IResult<&str, Vec<(Lit, isize)>> {
+    many1(weighted_literal)(input)
+}
+
+/// Leniently parses OPB constraint or objective ending as ';' or a line ending
+fn opb_ending(input: &str) -> IResult<&str, &str> {
+    recognize(pair(
+        space0,
+        opt(pair(
+            alt((
+                recognize(tuple((tag(";"), space0, line_ending))),
+                line_ending,
+                tag(";"),
+            )),
+            space0,
+        )),
+    ))(input)
+}
+
+/// Parses an OPB constraint
+fn constraint(input: &str) -> IResult<&str, PBConstraint> {
+    map_res(
+        tuple((weighted_lit_sum, operator, space0, weight, opb_ending)),
+        |(wls, op, _, b, _)| {
+            let lits = HashMap::from_iter(wls.into_iter());
+            Ok::<_, ()>(match op {
+                OpbOperator::LE => PBConstraint::new_ub(lits, b),
+                OpbOperator::GE => PBConstraint::new_lb(lits, b),
+                OpbOperator::LT => PBConstraint::new_ub(lits, b + 1),
+                OpbOperator::GT => PBConstraint::new_lb(lits, b + 1),
+                OpbOperator::EQ => PBConstraint::new_eq(lits, b),
+            })
+        },
+    )(input)
+}
+
+#[cfg(feature = "optimization")]
+/// Parses an OPB objective
+fn objective(input: &str) -> IResult<&str, Objective> {
+    map_res(
+        tuple((tag("min:"), space0, weighted_lit_sum, opb_ending)),
+        |(_, _, wsl, _)| {
+            let mut obj = Objective::new();
+            wsl.into_iter()
+                .for_each(|(l, w)| obj.add_soft_lit_int(w, l));
+            Ok::<_, ()>(obj)
+        },
+    )(input)
+}
+
+#[cfg(not(feature = "optimization"))]
+/// Matches an OPB objective
+fn objective(input: &str) -> IResult<&str, &str> {
+    recognize(tuple((tag("min:"), space0, weighted_lit_sum, opb_ending)))(input)
+}
+
+/// Top level string parser applied to lines
+fn opb_data(input: &str) -> IResult<&str, OpbData> {
+    alt((
+        map_res(comment, |cmt| Ok::<_, ()>(OpbData::Cmt(String::from(cmt)))),
+        map_res(constraint, |constr| Ok::<_, ()>(OpbData::Constr(constr))),
+        #[cfg(feature = "optimization")]
+        map_res(objective, |obj| Ok::<_, ()>(OpbData::Obj(obj))),
+        #[cfg(not(feature = "optimization"))]
+        map_res(objective, |obj| {
+            Ok::<_, ()>(OpbData::Obj(String::from(obj)))
+        }),
+    ))(input)
+}
+
+#[cfg(test)]
+mod test {
+    use std::{
+        collections::HashMap,
+        io::{BufReader, Cursor},
+    };
+
+    use super::{
+        comment, constraint, literal, objective, opb_data, opb_ending, operator, parse_opb_data,
+        variable, weight, weighted_lit_sum, weighted_literal, OpbData, OpbError, OpbOperator,
+    };
+    use crate::{
+        instances::Objective,
+        lit,
+        types::{constraints::PBConstraint, Lit, Var},
+        var,
+    };
+    use nom::error::{Error, ErrorKind};
+
+    #[test]
+    fn match_comment() {
+        assert_eq!(comment("* test\n"), Ok(("", "* test\n")));
+        assert_eq!(comment("* test"), Ok(("", "* test")));
+        assert_eq!(comment("*\n"), Ok(("", "*\n")));
+        assert_eq!(
+            comment(" test\n"),
+            Err(nom::Err::Error(Error::new(" test\n", ErrorKind::Tag)))
+        );
+    }
+
+    #[test]
+    fn parse_variable() {
+        assert_eq!(variable("x5 test"), Ok((" test", var![5])));
+        assert_eq!(variable("x2 test"), Ok((" test", var![2])));
+        assert_eq!(
+            variable(" test\n"),
+            Err(nom::Err::Error(Error::new(" test\n", ErrorKind::Tag)))
+        );
+    }
+
+    #[test]
+    fn parse_literal() {
+        assert_eq!(literal("x5 test"), Ok((" test", lit![5])));
+        assert_eq!(literal("x2 test"), Ok((" test", lit![2])));
+        assert_eq!(literal("~x5 test"), Ok((" test", !lit![5])));
+        assert_eq!(literal("~x2 test"), Ok((" test", !lit![2])));
+    }
+
+    #[test]
+    fn parse_operator() {
+        assert_eq!(operator("<= test"), Ok((" test", OpbOperator::LE)));
+        assert_eq!(operator(">= test"), Ok((" test", OpbOperator::GE)));
+        assert_eq!(operator("< test"), Ok((" test", OpbOperator::LT)));
+        assert_eq!(operator("> test"), Ok((" test", OpbOperator::GT)));
+        assert_eq!(operator("= test"), Ok((" test", OpbOperator::EQ)));
+    }
+
+    #[test]
+    fn parse_weight() {
+        assert_eq!(weight("5 test"), Ok((" test", 5)));
+        assert_eq!(weight("+5 test"), Ok((" test", 5)));
+        assert_eq!(weight("-5 test"), Ok((" test", -5)));
+    }
+
+    #[test]
+    fn parse_weighted_literal() {
+        assert_eq!(weighted_literal("5 x1 test"), Ok(("test", (lit![1], 5))));
+        assert_eq!(weighted_literal("-5  x1 test"), Ok(("test", (lit![1], -5))));
+        assert_eq!(weighted_literal("5 ~x1  test"), Ok(("test", (!lit![1], 5))));
+        assert_eq!(
+            weighted_literal("-5 ~x1 test"),
+            Ok(("test", (!lit![1], -5)))
+        );
+    }
+
+    #[test]
+    fn parse_weighted_lit_sum() {
+        assert_eq!(
+            weighted_lit_sum("5  x1    -3 ~x2  test"),
+            Ok(("test", vec![(lit![1], 5), (!lit![2], -3)]))
+        );
+    }
+
+    #[test]
+    fn parse_opb_ending() {
+        assert_eq!(opb_ending("   ; test"), Ok(("test", "   ; ")));
+        assert_eq!(opb_ending("   \n test"), Ok(("test", "   \n ")));
+        assert_eq!(opb_ending("  ; \n test"), Ok(("test", "  ; \n ")));
+        assert_eq!(opb_ending("  "), Ok(("", "  ")));
+    }
+
+    #[test]
+    fn parse_constraint() {
+        match constraint("3 x1 -2 ~x2 <= 4;") {
+            Ok((rest, constr)) => match constr {
+                PBConstraint::UB(constr) => {
+                    assert_eq!(rest, "");
+                    let (lits, b) = constr.decompose();
+                    let mut should_be_lits = HashMap::new();
+                    should_be_lits.insert(lit![1], 3);
+                    should_be_lits.insert(lit![2], 2);
+                    assert_eq!(lits, should_be_lits);
+                    assert_eq!(b, 6);
+                }
+                PBConstraint::LB(_) => panic!(),
+                PBConstraint::EQ(_) => panic!(),
+            },
+            Err(_) => panic!(),
+        }
+    }
+
+    #[cfg(feature = "optimization")]
+    #[test]
+    fn parse_objective() {
+        match objective("min: 3 x1 -2 ~x2;") {
+            Ok((rest, obj)) => {
+                assert_eq!(rest, "");
+                let mut should_be_obj = Objective::new();
+                should_be_obj.add_soft_lit_int(3, lit![1]);
+                should_be_obj.add_soft_lit_int(-2, !lit![2]);
+                assert_eq!(obj, should_be_obj);
+            }
+            Err(_) => panic!(),
+        }
+        match objective("min: x0;") {
+            Ok(_) => panic!(),
+            Err(err) => assert_eq!(err, nom::Err::Error(Error::new("x0;", ErrorKind::Digit))),
+        }
+    }
+
+    #[cfg(not(feature = "optimization"))]
+    #[test]
+    fn parse_objective() {
+        assert_eq!(objective("min: 3 x1 -2 ~x2;"), Ok(("", "min: 3 x1 -2 ~x2")));
+    }
+
+    #[test]
+    fn single_opb_data() {
+        assert_eq!(
+            opb_data("* test\n"),
+            Ok(("", OpbData::Cmt(String::from("* test\n"))))
+        );
+        let mut lits = HashMap::new();
+        lits.insert(lit![1], 3);
+        lits.insert(!lit![2], -2);
+        let should_be_constr = PBConstraint::new_ub(lits, 4);
+        assert_eq!(
+            opb_data("3 x1 -2 ~x2 <= 4;\n"),
+            Ok(("", OpbData::Constr(should_be_constr)))
+        );
+        let mut obj = Objective::new();
+        obj.add_soft_lit_int(-3, lit![0]);
+        obj.add_soft_lit_int(4, lit![1]);
+        assert_eq!(opb_data("min: -3 x0 4 x1;"), Ok(("", OpbData::Obj(obj))));
+        assert_eq!(
+            opb_data("min: x0;"),
+            Err(nom::Err::Error(Error::new("x0;", ErrorKind::Digit)))
+        );
+    }
+
+    #[test]
+    fn multi_opb_data() {
+        let data = "* test\n5 x0 -3 x1 >= 4;\nmin: 1 x0;";
+        let reader = Cursor::new(data);
+        let reader = BufReader::new(reader);
+        match parse_opb_data(reader) {
+            Ok(data) => {
+                assert_eq!(data.len(), 3);
+                assert_eq!(data[0], OpbData::Cmt(String::from("* test\n")));
+                if let OpbData::Constr(_) = data[1] {
+                    ()
+                } else {
+                    panic!()
+                }
+                if let OpbData::Obj(_) = data[2] {
+                    ()
+                } else {
+                    panic!()
+                }
+            }
+            Err(_) => panic!(),
+        }
+        let data = "* test\n5 x0 -3 x1 >= 4;\nmin: x0;";
+        let reader = Cursor::new(data);
+        let reader = BufReader::new(reader);
+        assert_eq!(
+            parse_opb_data(reader),
+            Err(OpbError::InvalidLine(String::from("min: x0;")))
+        );
+    }
+}
diff --git a/src/solvers.rs b/src/solvers.rs
index d40054d0..10357d37 100644
--- a/src/solvers.rs
+++ b/src/solvers.rs
@@ -60,7 +60,7 @@ pub trait Solve {
         self.add_clause(clause![lit])
     }
     /// Like [`Solve::add_clause`] but for clauses with two literals.
-    fn add_pair(&mut self, lit1: Lit, lit2: Lit) {
+    fn add_binary(&mut self, lit1: Lit, lit2: Lit) {
         self.add_clause(clause![lit1, lit2])
     }
     /// Like [`Solve::add_clause`] but for clauses with three literals.
diff --git a/src/solvers/cadical.rs b/src/solvers/cadical.rs
index 8a9346ba..84d5c08c 100644
--- a/src/solvers/cadical.rs
+++ b/src/solvers/cadical.rs
@@ -679,8 +679,8 @@ mod test {
     #[test]
     fn tiny_instance() {
         let mut solver = CaDiCaL::new();
-        solver.add_pair(lit![0], !lit![1]);
-        solver.add_pair(lit![1], !lit![2]);
+        solver.add_binary(lit![0], !lit![1]);
+        solver.add_binary(lit![1], !lit![2]);
         let ret = solver.solve();
         match ret {
             Err(e) => panic!("got error when solving: {}", e),
@@ -691,15 +691,15 @@ mod test {
     #[test]
     fn termination_callback() {
         let mut solver = CaDiCaL::new();
-        solver.add_pair(lit![0], !lit![1]);
-        solver.add_pair(lit![1], !lit![2]);
-        solver.add_pair(lit![2], !lit![3]);
-        solver.add_pair(lit![3], !lit![4]);
-        solver.add_pair(lit![4], !lit![5]);
-        solver.add_pair(lit![5], !lit![6]);
-        solver.add_pair(lit![6], !lit![7]);
-        solver.add_pair(lit![7], !lit![8]);
-        solver.add_pair(lit![8], !lit![9]);
+        solver.add_binary(lit![0], !lit![1]);
+        solver.add_binary(lit![1], !lit![2]);
+        solver.add_binary(lit![2], !lit![3]);
+        solver.add_binary(lit![3], !lit![4]);
+        solver.add_binary(lit![4], !lit![5]);
+        solver.add_binary(lit![5], !lit![6]);
+        solver.add_binary(lit![6], !lit![7]);
+        solver.add_binary(lit![7], !lit![8]);
+        solver.add_binary(lit![8], !lit![9]);
 
         solver.set_terminator(|| ControlSignal::Terminate);
 
@@ -718,15 +718,15 @@ mod test {
     #[test]
     fn learner_callback() {
         let mut solver = CaDiCaL::new();
-        solver.add_pair(lit![0], !lit![1]);
-        solver.add_pair(lit![1], !lit![2]);
-        solver.add_pair(lit![2], !lit![3]);
-        solver.add_pair(lit![3], !lit![4]);
-        solver.add_pair(lit![4], !lit![5]);
-        solver.add_pair(lit![5], !lit![6]);
-        solver.add_pair(lit![6], !lit![7]);
-        solver.add_pair(lit![7], !lit![8]);
-        solver.add_pair(lit![8], !lit![9]);
+        solver.add_binary(lit![0], !lit![1]);
+        solver.add_binary(lit![1], !lit![2]);
+        solver.add_binary(lit![2], !lit![3]);
+        solver.add_binary(lit![3], !lit![4]);
+        solver.add_binary(lit![4], !lit![5]);
+        solver.add_binary(lit![5], !lit![6]);
+        solver.add_binary(lit![6], !lit![7]);
+        solver.add_binary(lit![7], !lit![8]);
+        solver.add_binary(lit![8], !lit![9]);
         solver.add_unit(lit![9]);
         solver.add_unit(!lit![0]);
 
@@ -788,15 +788,15 @@ mod test {
     #[test]
     fn backend_stats() {
         let mut solver = CaDiCaL::new();
-        solver.add_pair(lit![0], !lit![1]);
-        solver.add_pair(lit![1], !lit![2]);
-        solver.add_pair(lit![2], !lit![3]);
-        solver.add_pair(lit![3], !lit![4]);
-        solver.add_pair(lit![4], !lit![5]);
-        solver.add_pair(lit![5], !lit![6]);
-        solver.add_pair(lit![6], !lit![7]);
-        solver.add_pair(lit![7], !lit![8]);
-        solver.add_pair(lit![8], !lit![9]);
+        solver.add_binary(lit![0], !lit![1]);
+        solver.add_binary(lit![1], !lit![2]);
+        solver.add_binary(lit![2], !lit![3]);
+        solver.add_binary(lit![3], !lit![4]);
+        solver.add_binary(lit![4], !lit![5]);
+        solver.add_binary(lit![5], !lit![6]);
+        solver.add_binary(lit![6], !lit![7]);
+        solver.add_binary(lit![7], !lit![8]);
+        solver.add_binary(lit![8], !lit![9]);
 
         assert_eq!(solver.get_active(), 10);
         assert_eq!(solver.get_irredundant(), 9);
@@ -807,7 +807,7 @@ mod test {
     #[test]
     fn freezing() {
         let mut solver = CaDiCaL::new();
-        solver.add_pair(lit![0], !lit![1]);
+        solver.add_binary(lit![0], !lit![1]);
 
         solver.freeze_lit(lit![0]);
 
diff --git a/src/solvers/ipasir.rs b/src/solvers/ipasir.rs
index b5fac583..cccc9a45 100644
--- a/src/solvers/ipasir.rs
+++ b/src/solvers/ipasir.rs
@@ -338,8 +338,8 @@ mod test {
     #[test]
     fn tiny_instance() {
         let mut solver = IpasirSolver::new();
-        solver.add_pair(lit![0], !lit![1]);
-        solver.add_pair(lit![1], !lit![2]);
+        solver.add_binary(lit![0], !lit![1]);
+        solver.add_binary(lit![1], !lit![2]);
         let ret = solver.solve();
         match ret {
             Err(e) => panic!("got error when solving: {}", e),
@@ -350,15 +350,15 @@ mod test {
     #[test]
     fn termination_callback() {
         let mut solver = IpasirSolver::new();
-        solver.add_pair(lit![0], !lit![1]);
-        solver.add_pair(lit![1], !lit![2]);
-        solver.add_pair(lit![2], !lit![3]);
-        solver.add_pair(lit![3], !lit![4]);
-        solver.add_pair(lit![4], !lit![5]);
-        solver.add_pair(lit![5], !lit![6]);
-        solver.add_pair(lit![6], !lit![7]);
-        solver.add_pair(lit![7], !lit![8]);
-        solver.add_pair(lit![8], !lit![9]);
+        solver.add_binary(lit![0], !lit![1]);
+        solver.add_binary(lit![1], !lit![2]);
+        solver.add_binary(lit![2], !lit![3]);
+        solver.add_binary(lit![3], !lit![4]);
+        solver.add_binary(lit![4], !lit![5]);
+        solver.add_binary(lit![5], !lit![6]);
+        solver.add_binary(lit![6], !lit![7]);
+        solver.add_binary(lit![7], !lit![8]);
+        solver.add_binary(lit![8], !lit![9]);
 
         solver.set_terminator(|| ControlSignal::Terminate);
 
@@ -377,15 +377,15 @@ mod test {
     #[test]
     fn learner_callback() {
         let mut solver = IpasirSolver::new();
-        solver.add_pair(lit![0], !lit![1]);
-        solver.add_pair(lit![1], !lit![2]);
-        solver.add_pair(lit![2], !lit![3]);
-        solver.add_pair(lit![3], !lit![4]);
-        solver.add_pair(lit![4], !lit![5]);
-        solver.add_pair(lit![5], !lit![6]);
-        solver.add_pair(lit![6], !lit![7]);
-        solver.add_pair(lit![7], !lit![8]);
-        solver.add_pair(lit![8], !lit![9]);
+        solver.add_binary(lit![0], !lit![1]);
+        solver.add_binary(lit![1], !lit![2]);
+        solver.add_binary(lit![2], !lit![3]);
+        solver.add_binary(lit![3], !lit![4]);
+        solver.add_binary(lit![4], !lit![5]);
+        solver.add_binary(lit![5], !lit![6]);
+        solver.add_binary(lit![6], !lit![7]);
+        solver.add_binary(lit![7], !lit![8]);
+        solver.add_binary(lit![8], !lit![9]);
         solver.add_unit(lit![9]);
         solver.add_unit(!lit![0]);
 
diff --git a/src/types.rs b/src/types.rs
index 8deae49b..c1ab25d8 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -2,9 +2,12 @@
 //!
 //! Common types used throughout the library to guarantee type safety.
 
-use core::{ffi::c_int, ops::Not};
+use core::ffi::c_int;
 use std::{fmt, ops};
 
+pub mod constraints;
+pub use constraints::Clause;
+
 /// Type representing boolean variables in a SAT problem. Variables indexing in
 /// RustSAT starts from 0 and the maximum index is `(usize::MAX - 1) / 2`. This is
 /// because literals are represented as a single `usize` as well. The memory
@@ -100,6 +103,28 @@ impl Var {
     }
 }
 
+/// Incrementing variables
+impl ops::Add<usize> for Var {
+    type Output = Var;
+
+    fn add(self, rhs: usize) -> Self::Output {
+        Var {
+            idx: self.idx + rhs,
+        }
+    }
+}
+
+/// Decrementing variables
+impl ops::Sub<usize> for Var {
+    type Output = Var;
+
+    fn sub(self, rhs: usize) -> Self::Output {
+        Var {
+            idx: self.idx - rhs,
+        }
+    }
+}
+
 /// Variables can be printed with the [`Display`](std::fmt::Display) trait
 impl fmt::Display for Var {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
@@ -303,7 +328,7 @@ impl Lit {
 }
 
 /// Trait implementation allowing for negating literals with the `!` operator.
-impl Not for Lit {
+impl ops::Not for Lit {
     type Output = Lit;
 
     #[inline]
@@ -314,6 +339,40 @@ impl Not for Lit {
     }
 }
 
+/// Trait implementation allowing for negating literals with the unary `-` operator.
+impl ops::Neg for Lit {
+    type Output = Lit;
+
+    #[inline]
+    fn neg(self) -> Lit {
+        Lit {
+            lidx: self.lidx ^ 1usize,
+        }
+    }
+}
+
+/// Incrementing literals. This preserves the sign of the literal.
+impl ops::Add<usize> for Lit {
+    type Output = Lit;
+
+    fn add(self, rhs: usize) -> Self::Output {
+        Lit {
+            lidx: self.lidx + 2 * rhs,
+        }
+    }
+}
+
+/// Decrementing literals. This preserves the sign of the literal.
+impl ops::Sub<usize> for Lit {
+    type Output = Lit;
+
+    fn sub(self, rhs: usize) -> Self::Output {
+        Lit {
+            lidx: self.lidx - 2 * rhs,
+        }
+    }
+}
+
 /// Literals can be printed with the [`Display`](std::fmt::Display) trait
 impl fmt::Display for Lit {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
@@ -359,164 +418,6 @@ macro_rules! ipasir_lit {
     };
 }
 
-/// 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.
-#[derive(Hash, Eq, PartialEq, Clone)]
-pub struct Clause {
-    lits: Vec<Lit>,
-}
-
-impl Clause {
-    /// Creates a new empty clause
-    pub fn new() -> Clause {
-        Clause { lits: Vec::new() }
-    }
-
-    /// Create a new clause from an iterator
-    pub fn from<I>(lits: I) -> Clause
-    where
-        I: Iterator<Item = Lit>,
-    {
-        Clause {
-            lits: lits.collect(),
-        }
-    }
-
-    /// Gets the length of the clause
-    #[inline]
-    pub fn len(&self) -> usize {
-        self.lits.len()
-    }
-
-    /// Adds a literal to the clause
-    pub fn add(&mut self, lit: Lit) {
-        self.lits.push(lit)
-    }
-
-    /// Removes the first occurrence of a literal from the clause
-    /// Returns true if an occurrence was found
-    pub fn remove(&mut self, lit: &Lit) -> bool {
-        for (i, l) in self.lits.iter().enumerate() {
-            if l == lit {
-                self.lits.swap_remove(i);
-                return true;
-            }
-        }
-        false
-    }
-
-    /// Removes all occurrences of a literal from the clause
-    pub fn remove_thorough(&mut self, lit: &Lit) -> bool {
-        let mut idxs = Vec::new();
-        for (i, l) in self.lits.iter().enumerate() {
-            if l == lit {
-                idxs.push(i);
-            }
-        }
-        for i in idxs.iter().rev() {
-            self.lits.remove(*i);
-        }
-        !idxs.is_empty()
-    }
-
-    /// Gets an iterator over the clause
-    #[inline]
-    pub fn iter(&self) -> std::slice::Iter<'_, Lit> {
-        self.lits.iter()
-    }
-}
-
-impl ops::Index<usize> for Clause {
-    type Output = Lit;
-
-    #[inline]
-    fn index(&self, index: usize) -> &Self::Output {
-        &self.lits[index]
-    }
-}
-
-impl ops::IndexMut<usize> for Clause {
-    #[inline]
-    fn index_mut(&mut self, index: usize) -> &mut Self::Output {
-        &mut self.lits[index]
-    }
-}
-
-impl<'a> IntoIterator for &'a Clause {
-    type Item = &'a Lit;
-
-    type IntoIter = std::slice::Iter<'a, Lit>;
-
-    #[inline]
-    fn into_iter(self) -> Self::IntoIter {
-        (&self.lits).into_iter()
-    }
-}
-
-impl<'a> IntoIterator for &'a mut Clause {
-    type Item = &'a mut Lit;
-
-    type IntoIter = std::slice::IterMut<'a, Lit>;
-
-    #[inline]
-    fn into_iter(self) -> Self::IntoIter {
-        (&mut self.lits).into_iter()
-    }
-}
-
-impl IntoIterator for Clause {
-    type Item = Lit;
-
-    type IntoIter = std::vec::IntoIter<Lit>;
-
-    #[inline]
-    fn into_iter(self) -> Self::IntoIter {
-        self.lits.into_iter()
-    }
-}
-
-/// Clauses can be printed with the [`Display`](std::fmt::Display) trait
-impl fmt::Display for Clause {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "(")?;
-        for (i, lit) in self.iter().enumerate() {
-            if i != 0 {
-                write!(f, "|")?;
-            }
-            write!(f, "{}", lit)?
-        }
-        write!(f, ")")
-    }
-}
-
-/// Clauses can be printed with the [`Debug`](std::fmt::Debug) trait
-impl fmt::Debug for Clause {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "(")?;
-        for (i, lit) in self.iter().enumerate() {
-            if i != 0 {
-                write!(f, "|")?;
-            }
-            write!(f, "{}", lit)?
-        }
-        write!(f, ")")
-    }
-}
-
-#[macro_export]
-macro_rules! clause {
-    ( $($l:expr),* ) => {
-        {
-            let mut tmp_clause = Clause::new();
-            $(
-                tmp_clause.add($l);
-            )*
-            tmp_clause
-        }
-    };
-}
-
 /// Ternary value assigned to a literal or variable, including possible "don't care"
 #[derive(Clone, Copy, PartialEq)]
 #[repr(u8)]
diff --git a/src/types/constraints.rs b/src/types/constraints.rs
new file mode 100644
index 00000000..7ac3562d
--- /dev/null
+++ b/src/types/constraints.rs
@@ -0,0 +1,807 @@
+//! # Constraint Types
+//!
+//! Different types of constraints. The most important one is [`Clause`] but
+//! Rust SAT supports more complex constraints like [`PBConstraint`] or
+//! [`CardConstraint`].
+
+use std::{collections::HashMap, fmt, ops};
+
+use super::Lit;
+
+/// 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.
+#[derive(Hash, Eq, PartialEq, Clone)]
+pub struct Clause {
+    lits: Vec<Lit>,
+}
+
+impl Clause {
+    /// Creates a new empty clause
+    pub fn new() -> Clause {
+        Clause { lits: Vec::new() }
+    }
+
+    /// Create a new clause from an iterator
+    pub fn from<I>(lits: I) -> Clause
+    where
+        I: Iterator<Item = Lit>,
+    {
+        Clause {
+            lits: lits.collect(),
+        }
+    }
+
+    /// Gets the length of the clause
+    #[inline]
+    pub fn len(&self) -> usize {
+        self.lits.len()
+    }
+
+    /// Adds a literal to the clause
+    pub fn add(&mut self, lit: Lit) {
+        self.lits.push(lit)
+    }
+
+    /// Removes the first occurrence of a literal from the clause
+    /// Returns true if an occurrence was found
+    pub fn remove(&mut self, lit: &Lit) -> bool {
+        for (i, l) in self.lits.iter().enumerate() {
+            if l == lit {
+                self.lits.swap_remove(i);
+                return true;
+            }
+        }
+        false
+    }
+
+    /// Removes all occurrences of a literal from the clause
+    pub fn remove_thorough(&mut self, lit: &Lit) -> bool {
+        let mut idxs = Vec::new();
+        for (i, l) in self.lits.iter().enumerate() {
+            if l == lit {
+                idxs.push(i);
+            }
+        }
+        for i in idxs.iter().rev() {
+            self.lits.remove(*i);
+        }
+        !idxs.is_empty()
+    }
+
+    /// Gets an iterator over the clause
+    #[inline]
+    pub fn iter(&self) -> std::slice::Iter<'_, Lit> {
+        self.lits.iter()
+    }
+}
+
+impl ops::Index<usize> for Clause {
+    type Output = Lit;
+
+    #[inline]
+    fn index(&self, index: usize) -> &Self::Output {
+        &self.lits[index]
+    }
+}
+
+impl ops::IndexMut<usize> for Clause {
+    #[inline]
+    fn index_mut(&mut self, index: usize) -> &mut Self::Output {
+        &mut self.lits[index]
+    }
+}
+
+impl<'a> IntoIterator for &'a Clause {
+    type Item = &'a Lit;
+
+    type IntoIter = std::slice::Iter<'a, Lit>;
+
+    #[inline]
+    fn into_iter(self) -> Self::IntoIter {
+        (&self.lits).into_iter()
+    }
+}
+
+impl<'a> IntoIterator for &'a mut Clause {
+    type Item = &'a mut Lit;
+
+    type IntoIter = std::slice::IterMut<'a, Lit>;
+
+    #[inline]
+    fn into_iter(self) -> Self::IntoIter {
+        (&mut self.lits).into_iter()
+    }
+}
+
+impl IntoIterator for Clause {
+    type Item = Lit;
+
+    type IntoIter = std::vec::IntoIter<Lit>;
+
+    #[inline]
+    fn into_iter(self) -> Self::IntoIter {
+        self.lits.into_iter()
+    }
+}
+
+/// Clauses can be printed with the [`Display`](std::fmt::Display) trait
+impl fmt::Display for Clause {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "(")?;
+        for (i, lit) in self.iter().enumerate() {
+            if i != 0 {
+                write!(f, "|")?;
+            }
+            write!(f, "{}", lit)?
+        }
+        write!(f, ")")
+    }
+}
+
+/// Clauses can be printed with the [`Debug`](std::fmt::Debug) trait
+impl fmt::Debug for Clause {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "(")?;
+        for (i, lit) in self.iter().enumerate() {
+            if i != 0 {
+                write!(f, "|")?;
+            }
+            write!(f, "{}", lit)?
+        }
+        write!(f, ")")
+    }
+}
+
+#[macro_export]
+macro_rules! clause {
+    ( $($l:expr),* ) => {
+        {
+            let mut tmp_clause = Clause::new();
+            $(
+                tmp_clause.add($l);
+            )*
+            tmp_clause
+        }
+    };
+}
+
+/// Type representing a cardinality constraint.
+#[derive(Hash, Eq, PartialEq, Clone, Debug)]
+pub enum CardConstraint {
+    /// An upper bound cardinality constraint
+    UB(CardUBConstr),
+    /// A lower bound cardinality constraint
+    LB(CardLBConstr),
+    /// An equality cardinality constraint
+    EQ(CardEQConstr),
+}
+
+impl CardConstraint {
+    /// Constructs a new upper bound cardinality constraint (`sum of lits <= b`)
+    pub fn new_ub(lits: Vec<Lit>, b: usize) -> Self {
+        CardConstraint::UB(CardUBConstr { lits, b })
+    }
+
+    /// Constructs a new lower bound cardinality constraint (`sum of lits >= b`)
+    pub fn new_lb(lits: Vec<Lit>, b: usize) -> Self {
+        CardConstraint::LB(CardLBConstr { lits, b })
+    }
+
+    /// Constructs a new equality cardinality constraint (`sum of lits = b`)
+    pub fn new_eq(lits: Vec<Lit>, b: usize) -> Self {
+        CardConstraint::EQ(CardEQConstr { lits, b })
+    }
+
+    /// Adds literals to the cardinality constraint
+    pub fn add(&mut self, lits: Vec<Lit>) {
+        match self {
+            CardConstraint::UB(constr) => constr.lits.extend(lits),
+            CardConstraint::LB(constr) => constr.lits.extend(lits),
+            CardConstraint::EQ(constr) => constr.lits.extend(lits),
+        }
+    }
+
+    /// Changes the bound on the constraint
+    pub fn change_bound(&mut self, b: usize) {
+        match self {
+            CardConstraint::UB(constr) => constr.b = b,
+            CardConstraint::LB(constr) => constr.b = b,
+            CardConstraint::EQ(constr) => constr.b = b,
+        }
+    }
+
+    /// Checks if the constraint is always satisfied
+    pub fn is_tautology(&self) -> bool {
+        match self {
+            CardConstraint::UB(constr) => constr.is_tautology(),
+            CardConstraint::LB(constr) => constr.is_tautology(),
+            CardConstraint::EQ(_) => false,
+        }
+    }
+
+    /// Checks if the constraint is unsatisfiable
+    pub fn is_unsat(&self) -> bool {
+        match self {
+            CardConstraint::UB(_) => false,
+            CardConstraint::LB(constr) => constr.is_unsat(),
+            CardConstraint::EQ(constr) => constr.is_unsat(),
+        }
+    }
+
+    /// Checks if the constraint is an assignment
+    pub fn is_assignment(&self) -> bool {
+        match self {
+            CardConstraint::UB(_) => false,
+            CardConstraint::LB(constr) => constr.is_assignment(),
+            CardConstraint::EQ(constr) => constr.is_assignment(),
+        }
+    }
+
+    /// Checks if the constraint is a clause
+    pub fn is_clause(&self) -> bool {
+        match self {
+            CardConstraint::UB(_) => false,
+            CardConstraint::LB(constr) => constr.is_clause(),
+            CardConstraint::EQ(_) => false,
+        }
+    }
+
+    /// Gets the literals that are in the constraint
+    pub fn into_lits(self) -> Vec<Lit> {
+        match self {
+            CardConstraint::UB(constr) => constr.lits,
+            CardConstraint::LB(constr) => constr.lits,
+            CardConstraint::EQ(constr) => constr.lits,
+        }
+    }
+
+    /// Gets an iterator over the literals in the constraint
+    #[inline]
+    pub fn iter(&self) -> std::slice::Iter<'_, Lit> {
+        match self {
+            CardConstraint::UB(constr) => constr.lits.iter(),
+            CardConstraint::LB(constr) => constr.lits.iter(),
+            CardConstraint::EQ(constr) => constr.lits.iter(),
+        }
+    }
+}
+
+/// An upper bound cardinality constraint (`sum of lits <= b`)
+#[derive(Hash, Eq, PartialEq, Clone, Debug)]
+pub struct CardUBConstr {
+    lits: Vec<Lit>,
+    b: usize,
+}
+
+impl CardUBConstr {
+    /// Decomposes the constraint to a set of input literals and an upper bound
+    pub fn decompose(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()
+    }
+}
+
+/// A lower bound cardinality constraint (`sum of lits >= b`)
+#[derive(Hash, Eq, PartialEq, Clone, Debug)]
+pub struct CardLBConstr {
+    lits: Vec<Lit>,
+    b: usize,
+}
+
+impl CardLBConstr {
+    /// Decomposes the constraint to a set of input literals and a lower bound
+    pub fn decompose(self) -> (Vec<Lit>, usize) {
+        (self.lits, self.b)
+    }
+
+    /// Checks if the constraint is always satisfied
+    pub fn is_tautology(&self) -> bool {
+        self.b <= 0
+    }
+
+    /// Checks if the constraint is unsatisfiable
+    pub fn is_unsat(&self) -> bool {
+        self.b > self.lits.len()
+    }
+
+    /// Checks if the constraint is an assignment
+    pub fn is_assignment(&self) -> bool {
+        self.b == self.lits.len()
+    }
+
+    /// Checks if the constraint is a clause
+    pub fn is_clause(&self) -> bool {
+        self.b == 1
+    }
+}
+
+/// An equality cardinality constraint (`sum of lits = b`)
+#[derive(Hash, Eq, PartialEq, Clone, Debug)]
+pub struct CardEQConstr {
+    lits: Vec<Lit>,
+    b: usize,
+}
+
+impl CardEQConstr {
+    /// Decomposes the constraint to a set of input literals and an equality bound
+    pub fn decompose(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()
+    }
+
+    /// Checks if the constraint is an assignment
+    pub fn is_assignment(&self) -> bool {
+        self.b == self.lits.len()
+    }
+}
+
+/// Errors when converting pseudo-boolean to cardinality constraints
+#[derive(Debug)]
+pub enum PBToCardError {
+    /// the pseudo-boolean constraint is not a cardinality constraint
+    NotACard,
+    /// the pseudo-boolean constraint is unsatisfiable
+    Unsat,
+    /// the pseudo-boolean constraint is a tautology
+    Tautology,
+}
+
+/// Type representing a pseudo-boolean constraint. When literals are added to a
+/// constraint, the constraint is transformed so that all coefficients are
+/// positive.
+#[derive(Eq, PartialEq, Clone, Debug)]
+pub enum PBConstraint {
+    /// An upper bound pseudo-boolean constraint
+    UB(PBUBConstr),
+    /// A lower bound pseudo-boolean constraint
+    LB(PBLBConstr),
+    /// An equality pseudo-boolean constraint
+    EQ(PBEQConstr),
+}
+
+impl PBConstraint {
+    /// Converts input literals to non-negative weights, also returns the weight sum and the sum to add to the bound
+    fn convert_input_lits(lits: HashMap<Lit, isize>) -> (HashMap<Lit, usize>, usize, isize) {
+        let mut b_add = 0;
+        let mut weight_sum = 0;
+        let lits = lits
+            .into_iter()
+            .map(|(l, w)| {
+                if w >= 0 {
+                    weight_sum += w as usize;
+                    (l, w as usize)
+                } else {
+                    b_add -= w;
+                    weight_sum += -w as usize;
+                    (!l, -w as usize)
+                }
+            })
+            .collect();
+        (lits, weight_sum, b_add)
+    }
+    /// Constructs a new upper bound pseudo-boolean constraint (`weighted sum of lits <= b`)
+    pub fn new_ub(lits: HashMap<Lit, isize>, b: isize) -> Self {
+        let (lits, weight_sum, b_add) = PBConstraint::convert_input_lits(lits);
+        PBConstraint::UB(PBUBConstr {
+            lits,
+            weight_sum,
+            b: b + b_add,
+        })
+    }
+
+    /// Constructs a new lower bound pseudo-boolean constraint (`weighted sum of lits >= b`)
+    pub fn new_lb(lits: HashMap<Lit, isize>, b: isize) -> Self {
+        let (lits, weight_sum, b_add) = PBConstraint::convert_input_lits(lits);
+        PBConstraint::LB(PBLBConstr {
+            lits,
+            weight_sum,
+            b: b + b_add,
+        })
+    }
+
+    /// Constructs a new equality pseudo-boolean constraint (`weighted sum of lits = b`)
+    pub fn new_eq(lits: HashMap<Lit, isize>, b: isize) -> Self {
+        let (lits, weight_sum, b_add) = PBConstraint::convert_input_lits(lits);
+        PBConstraint::EQ(PBEQConstr {
+            lits,
+            weight_sum,
+            b: b + b_add,
+        })
+    }
+
+    /// Gets mutable references to the underlying data
+    fn get_data(&mut self) -> (&mut HashMap<Lit, usize>, &mut usize, &mut isize) {
+        match self {
+            PBConstraint::UB(constr) => (&mut constr.lits, &mut constr.weight_sum, &mut constr.b),
+            PBConstraint::LB(constr) => (&mut constr.lits, &mut constr.weight_sum, &mut constr.b),
+            PBConstraint::EQ(constr) => (&mut constr.lits, &mut constr.weight_sum, &mut constr.b),
+        }
+    }
+
+    /// Adds literals to the cardinality constraint
+    pub fn add(&mut self, lits: HashMap<Lit, isize>) {
+        let (lits, add_weight_sum, b_add) = PBConstraint::convert_input_lits(lits);
+        let (data_lits, weight_sum, b) = self.get_data();
+        lits.iter().for_each(|(l, w)| {
+            match data_lits.get(l) {
+                Some(old_w) => data_lits.insert(*l, *old_w + *w),
+                None => data_lits.insert(*l, *w),
+            };
+        });
+        *weight_sum += add_weight_sum;
+        *b += b_add;
+    }
+
+    /// Checks if the constraint is always satisfied
+    pub fn is_tautology(&self) -> bool {
+        match self {
+            PBConstraint::UB(constr) => constr.is_tautology(),
+            PBConstraint::LB(constr) => constr.is_tautology(),
+            PBConstraint::EQ(_) => false,
+        }
+    }
+
+    /// Checks if the constraint is unsatisfiable
+    pub fn is_unsat(&self) -> bool {
+        match self {
+            PBConstraint::UB(constr) => constr.is_unsat(),
+            PBConstraint::LB(constr) => constr.is_unsat(),
+            PBConstraint::EQ(constr) => constr.is_unsat(),
+        }
+    }
+
+    /// Checks if the constraint is an assignment
+    pub fn is_assignment(&self) -> bool {
+        match self {
+            PBConstraint::UB(_) => false,
+            PBConstraint::LB(constr) => constr.is_assignment(),
+            PBConstraint::EQ(constr) => constr.is_assignment(),
+        }
+    }
+
+    /// Checks if the constraint is a cardinality constraint
+    pub fn is_card(&self) -> bool {
+        match self {
+            PBConstraint::UB(constr) => constr.get_unit_weight().is_some(),
+            PBConstraint::LB(constr) => constr.get_unit_weight().is_some(),
+            PBConstraint::EQ(constr) => constr.get_unit_weight().is_some(),
+        }
+    }
+
+    /// Converts the pseudo-boolean constraint into a cardinality constraint, if possible
+    pub fn as_card_constr(self) -> Result<CardConstraint, PBToCardError> {
+        if self.is_tautology() {
+            return Err(PBToCardError::Tautology);
+        }
+        if self.is_unsat() {
+            return Err(PBToCardError::Unsat);
+        }
+        Ok(match self {
+            PBConstraint::UB(constr) => {
+                let unit_weight = constr.get_unit_weight();
+                match unit_weight {
+                    None => return Err(PBToCardError::NotACard),
+                    Some(unit_weight) => {
+                        let lits = constr.lits.into_iter().map(|(l, _)| l).collect();
+                        CardConstraint::new_ub(lits, constr.b as usize / unit_weight)
+                    }
+                }
+            }
+            PBConstraint::LB(constr) => {
+                let unit_weight = constr.get_unit_weight();
+                match unit_weight {
+                    None => return Err(PBToCardError::NotACard),
+                    Some(unit_weight) => {
+                        let lits = constr.lits.into_iter().map(|(l, _)| l).collect();
+                        CardConstraint::new_lb(lits, constr.b as usize / unit_weight + 1)
+                    }
+                }
+            }
+            PBConstraint::EQ(constr) => {
+                let unit_weight = constr.get_unit_weight();
+                match unit_weight {
+                    None => return Err(PBToCardError::NotACard),
+                    Some(unit_weight) => {
+                        if constr.b as usize % unit_weight != 0 {
+                            return Err(PBToCardError::Unsat);
+                        }
+                        let lits = constr.lits.into_iter().map(|(l, _)| l).collect();
+                        CardConstraint::new_ub(lits, constr.b as usize / unit_weight)
+                    }
+                }
+            }
+        })
+    }
+
+    /// Gets the (positively) weighted literals that are in the constraint
+    pub fn into_lits(self) -> HashMap<Lit, usize> {
+        match self {
+            PBConstraint::UB(constr) => constr.lits,
+            PBConstraint::LB(constr) => constr.lits,
+            PBConstraint::EQ(constr) => constr.lits,
+        }
+    }
+
+    /// Gets an iterator over the literals in the constraint
+    #[inline]
+    pub fn iter(&self) -> std::collections::hash_map::Iter<'_, Lit, usize> {
+        match self {
+            PBConstraint::UB(constr) => constr.lits.iter(),
+            PBConstraint::LB(constr) => constr.lits.iter(),
+            PBConstraint::EQ(constr) => constr.lits.iter(),
+        }
+    }
+}
+
+/// An upper bound pseudo-boolean constraint (`weighted sum of lits <= b`)
+#[derive(Eq, PartialEq, Clone, Debug)]
+pub struct PBUBConstr {
+    lits: HashMap<Lit, usize>,
+    weight_sum: usize,
+    b: isize,
+}
+
+impl PBUBConstr {
+    /// Decomposes the constraint to a set of input literals and an upper bound
+    pub fn decompose(self) -> (HashMap<Lit, usize>, isize) {
+        (self.lits, self.b)
+    }
+
+    /// Checks if the constraint is always satisfied
+    pub fn is_tautology(&self) -> bool {
+        if self.b < 0 {
+            false
+        } else {
+            self.b as usize >= self.weight_sum
+        }
+    }
+
+    /// Checks if the constraint is unsatisfiable
+    pub fn is_unsat(&self) -> bool {
+        self.b < 0
+    }
+
+    /// Gets the unit weight of the constraint, if it exists
+    pub fn get_unit_weight(&self) -> Option<usize> {
+        let mut unit_weight = None;
+        for (_, &w) in self.lits.iter() {
+            if let Some(uw) = unit_weight {
+                if uw != w {
+                    return None;
+                }
+            } else {
+                unit_weight = Some(w)
+            }
+        }
+        unit_weight
+    }
+}
+
+/// A lower bound pseudo-boolean constraint (`weighted sum of lits >= b`)
+#[derive(Eq, PartialEq, Clone, Debug)]
+pub struct PBLBConstr {
+    lits: HashMap<Lit, usize>,
+    weight_sum: usize,
+    b: isize,
+}
+
+impl PBLBConstr {
+    /// Decomposes the constraint to a set of input literals and a lower bound
+    pub fn decompose(self) -> (HashMap<Lit, usize>, isize) {
+        (self.lits, self.b)
+    }
+
+    /// Checks if the constraint is always satisfied
+    pub fn is_tautology(&self) -> bool {
+        self.b <= 0
+    }
+
+    /// Checks if the constraint is unsatisfiable
+    pub fn is_unsat(&self) -> bool {
+        if self.b < 0 {
+            false
+        } else {
+            self.b as usize > self.weight_sum
+        }
+    }
+
+    /// Checks if the constraint is an assignment
+    pub fn is_assignment(&self) -> bool {
+        if self.b < 0 {
+            false
+        } else {
+            self.b as usize == self.weight_sum
+        }
+    }
+
+    /// Gets the unit weight of the constraint, if it exists
+    pub fn get_unit_weight(&self) -> Option<usize> {
+        let mut unit_weight = None;
+        for (_, &w) in self.lits.iter() {
+            if let Some(uw) = unit_weight {
+                if uw != w {
+                    return None;
+                }
+            } else {
+                unit_weight = Some(w)
+            }
+        }
+        unit_weight
+    }
+}
+
+/// An equality pseudo-boolean constraint (`weighted sum of lits = b`)
+#[derive(Eq, PartialEq, Clone, Debug)]
+pub struct PBEQConstr {
+    lits: HashMap<Lit, usize>,
+    weight_sum: usize,
+    b: isize,
+}
+
+impl PBEQConstr {
+    /// Decomposes the constraint to a set of input literals and an equality bound
+    pub fn decompose(self) -> (HashMap<Lit, usize>, isize) {
+        (self.lits, self.b)
+    }
+
+    /// Checks if the constraint is unsatisfiable
+    pub fn is_unsat(&self) -> bool {
+        if self.b < 0 {
+            true
+        } else {
+            self.b as usize > self.weight_sum
+        }
+    }
+
+    /// Checks if the constraint is an assignment
+    pub fn is_assignment(&self) -> bool {
+        if self.b < 0 {
+            false
+        } else {
+            self.b as usize == self.weight_sum
+        }
+    }
+
+    /// Gets the unit weight of the constraint, if it exists
+    pub fn get_unit_weight(&self) -> Option<usize> {
+        let mut unit_weight = None;
+        for (_, &w) in self.lits.iter() {
+            if let Some(uw) = unit_weight {
+                if uw != w {
+                    return None;
+                }
+            } else {
+                unit_weight = Some(w)
+            }
+        }
+        unit_weight
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::{CardConstraint, Clause, PBConstraint};
+    use crate::{lit, types::Lit};
+    use std::collections::HashMap;
+
+    #[test]
+    fn clause_remove() {
+        let mut cl = clause![lit![0], lit![1], lit![2], lit![1]];
+        assert!(!cl.remove(&lit![3]));
+        assert!(cl.remove(&lit![1]));
+        assert_eq!(cl.len(), 3);
+    }
+
+    #[test]
+    fn clause_remove_thorough() {
+        let mut cl = clause![lit![0], lit![1], lit![2], lit![1]];
+        assert!(!cl.remove_thorough(&lit![3]));
+        assert!(cl.remove_thorough(&lit![1]));
+        assert_eq!(cl.len(), 2);
+    }
+
+    #[test]
+    fn card_is_tautology() {
+        let lits = vec![lit![0], lit![1], lit![2]];
+        assert!(CardConstraint::new_ub(lits.clone(), 3).is_tautology());
+        assert!(!CardConstraint::new_ub(lits.clone(), 2).is_tautology());
+        assert!(CardConstraint::new_lb(lits.clone(), 0).is_tautology());
+        assert!(!CardConstraint::new_lb(lits.clone(), 1).is_tautology());
+        assert!(!CardConstraint::new_eq(lits.clone(), 2).is_tautology());
+    }
+
+    #[test]
+    fn card_is_unsat() {
+        let lits = vec![lit![0], lit![1], lit![2]];
+        assert!(!CardConstraint::new_ub(lits.clone(), 1).is_unsat());
+        assert!(!CardConstraint::new_lb(lits.clone(), 3).is_unsat());
+        assert!(CardConstraint::new_lb(lits.clone(), 4).is_unsat());
+        assert!(!CardConstraint::new_eq(lits.clone(), 2).is_unsat());
+        assert!(CardConstraint::new_eq(lits.clone(), 4).is_unsat());
+    }
+
+    #[test]
+    fn card_is_assignment() {
+        let lits = vec![lit![0], lit![1], lit![2]];
+        assert!(!CardConstraint::new_ub(lits.clone(), 1).is_assignment());
+        assert!(CardConstraint::new_lb(lits.clone(), 3).is_assignment());
+        assert!(!CardConstraint::new_lb(lits.clone(), 2).is_assignment());
+        assert!(CardConstraint::new_eq(lits.clone(), 3).is_assignment());
+        assert!(!CardConstraint::new_eq(lits.clone(), 2).is_assignment());
+    }
+
+    #[test]
+    fn card_is_clause() {
+        let lits = vec![lit![0], lit![1], lit![2]];
+        assert!(!CardConstraint::new_ub(lits.clone(), 1).is_clause());
+        assert!(!CardConstraint::new_lb(lits.clone(), 3).is_clause());
+        assert!(CardConstraint::new_lb(lits.clone(), 1).is_clause());
+        assert!(!CardConstraint::new_eq(lits.clone(), 2).is_clause());
+    }
+
+    #[test]
+    fn pb_is_tautology() {
+        let mut lits = HashMap::new();
+        lits.insert(lit![0], 1);
+        lits.insert(lit![1], 2);
+        lits.insert(lit![2], 3);
+        assert!(PBConstraint::new_ub(lits.clone(), 6).is_tautology());
+        assert!(!PBConstraint::new_ub(lits.clone(), 5).is_tautology());
+        assert!(PBConstraint::new_lb(lits.clone(), 0).is_tautology());
+        assert!(!PBConstraint::new_lb(lits.clone(), 1).is_tautology());
+        assert!(!PBConstraint::new_eq(lits.clone(), 2).is_tautology());
+    }
+
+    #[test]
+    fn pb_is_unsat() {
+        let mut lits = HashMap::new();
+        lits.insert(lit![0], 1);
+        lits.insert(lit![1], 2);
+        lits.insert(lit![2], 3);
+        assert!(!PBConstraint::new_ub(lits.clone(), 1).is_unsat());
+        assert!(!PBConstraint::new_lb(lits.clone(), 6).is_unsat());
+        assert!(PBConstraint::new_lb(lits.clone(), 7).is_unsat());
+        assert!(!PBConstraint::new_eq(lits.clone(), 2).is_unsat());
+        assert!(PBConstraint::new_eq(lits.clone(), 7).is_unsat());
+    }
+
+    #[test]
+    fn pb_is_assignment() {
+        let mut lits = HashMap::new();
+        lits.insert(lit![0], 1);
+        lits.insert(lit![1], 2);
+        lits.insert(lit![2], 3);
+        assert!(!PBConstraint::new_ub(lits.clone(), 1).is_assignment());
+        assert!(PBConstraint::new_lb(lits.clone(), 6).is_assignment());
+        assert!(!PBConstraint::new_lb(lits.clone(), 2).is_assignment());
+        assert!(PBConstraint::new_eq(lits.clone(), 6).is_assignment());
+        assert!(!PBConstraint::new_eq(lits.clone(), 2).is_assignment());
+    }
+
+    #[test]
+    fn pb_is_card() {
+        let mut lits = HashMap::new();
+        lits.insert(lit![0], 2);
+        lits.insert(lit![1], 2);
+        lits.insert(lit![2], 2);
+        assert!(PBConstraint::new_ub(lits.clone(), 1).is_card());
+        assert!(PBConstraint::new_lb(lits.clone(), 3).is_card());
+        assert!(PBConstraint::new_eq(lits.clone(), 2).is_card());
+        let mut lits = HashMap::new();
+        lits.insert(lit![0], 2);
+        lits.insert(lit![1], 1);
+        lits.insert(lit![2], 2);
+        assert!(!PBConstraint::new_ub(lits.clone(), 1).is_card());
+        assert!(!PBConstraint::new_lb(lits.clone(), 3).is_card());
+        assert!(!PBConstraint::new_eq(lits.clone(), 2).is_card());
+    }
+}


Test patch:
diff --git a/tests/constraints.rs b/tests/constraints.rs
new file mode 100644
index 00000000..56abccf7
--- /dev/null
+++ b/tests/constraints.rs
@@ -0,0 +1,173 @@
+use std::collections::HashMap;
+
+use rustsat::{
+    instances::SatInstance,
+    lit, solvers,
+    solvers::SolverResult,
+    types::{
+        constraints::{CardConstraint, PBConstraint},
+        Lit,
+    },
+};
+
+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();
+        println!("{:?}", cnf);
+        let mut solver = solvers::new_default_inc_solver();
+        solver.add_cnf(cnf);
+        assert_eq!(
+            solver.solve_assumps($sat_assump).unwrap(),
+            SolverResult::SAT
+        );
+        assert_eq!(
+            solver.solve_assumps($unsat_assump).unwrap(),
+            SolverResult::UNSAT
+        );
+    }};
+}
+
+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();
+        println!("{:?}", cnf);
+        let mut solver = solvers::new_default_inc_solver();
+        solver.add_cnf(cnf);
+        assert_eq!(
+            solver.solve_assumps($sat_assump).unwrap(),
+            SolverResult::SAT
+        );
+        assert_eq!(
+            solver.solve_assumps($unsat_assump).unwrap(),
+            SolverResult::UNSAT
+        );
+    }};
+}
+
+#[test]
+fn card_ub() {
+    let lits = vec![lit![0], lit![1], lit![2]];
+    test_card!(
+        CardConstraint::new_ub(lits.clone(), 1),
+        vec![!lit![0], lit![1], !lit![2]],
+        vec![lit![0], lit![1], !lit![2]]
+    );
+    test_card!(
+        CardConstraint::new_ub(lits.clone(), 2),
+        vec![lit![0], lit![1], !lit![2]],
+        vec![lit![0], lit![1], lit![2]]
+    );
+}
+
+#[test]
+fn card_lb() {
+    let lits = vec![lit![0], lit![1], lit![2]];
+    test_card!(
+        CardConstraint::new_lb(lits.clone(), 1),
+        vec![lit![0], lit![1], !lit![2]],
+        vec![!lit![0], !lit![1], !lit![2]]
+    );
+    test_card!(
+        CardConstraint::new_lb(lits.clone(), 2),
+        vec![lit![0], lit![1], !lit![2]],
+        vec![!lit![0], !lit![1], !lit![2]]
+    );
+    test_card!(
+        CardConstraint::new_lb(lits.clone(), 3),
+        vec![lit![0], lit![1], lit![2]],
+        vec![!lit![0], lit![1], !lit![2]]
+    );
+}
+
+#[test]
+fn card_eq() {
+    let lits = vec![lit![0], lit![1], lit![2]];
+    test_card!(
+        CardConstraint::new_eq(lits.clone(), 1),
+        vec![lit![0], !lit![1], !lit![2]],
+        vec![!lit![0], lit![1], lit![2]]
+    );
+    test_card!(
+        CardConstraint::new_eq(lits.clone(), 2),
+        vec![lit![0], lit![1], !lit![2]],
+        vec![!lit![0], !lit![1], !lit![2]]
+    );
+    test_card!(
+        CardConstraint::new_eq(lits.clone(), 3),
+        vec![lit![0], lit![1], lit![2]],
+        vec![!lit![0], lit![1], !lit![2]]
+    );
+}
+
+#[test]
+fn pb_ub() {
+    let mut lits = HashMap::new();
+    lits.insert(lit![0], 1);
+    lits.insert(lit![1], 2);
+    lits.insert(lit![2], 3);
+    test_pb!(
+        PBConstraint::new_eq(lits.clone(), 1),
+        vec![lit![0], !lit![1], !lit![2]],
+        vec![!lit![0], lit![1], !lit![2]]
+    );
+    test_pb!(
+        PBConstraint::new_eq(lits.clone(), 2),
+        vec![!lit![0], lit![1], !lit![2]],
+        vec![!lit![0], !lit![1], lit![2]]
+    );
+    test_pb!(
+        PBConstraint::new_eq(lits.clone(), 3),
+        vec![!lit![0], !lit![1], lit![2]],
+        vec![lit![0], !lit![1], lit![2]]
+    );
+}
+
+#[test]
+fn pb_lb() {
+    let mut lits = HashMap::new();
+    lits.insert(lit![0], 1);
+    lits.insert(lit![1], 2);
+    lits.insert(lit![2], 3);
+    test_pb!(
+        PBConstraint::new_lb(lits.clone(), 1),
+        vec![lit![0], lit![1], !lit![2]],
+        vec![!lit![0], !lit![1], !lit![2]]
+    );
+    test_pb!(
+        PBConstraint::new_lb(lits.clone(), 2),
+        vec![lit![0], lit![1], !lit![2]],
+        vec![lit![0], !lit![1], !lit![2]]
+    );
+    test_pb!(
+        PBConstraint::new_lb(lits.clone(), 3),
+        vec![!lit![0], !lit![1], lit![2]],
+        vec![!lit![0], lit![1], !lit![2]]
+    );
+}
+
+#[test]
+fn pb_eq() {
+    let mut lits = HashMap::new();
+    lits.insert(lit![0], 1);
+    lits.insert(lit![1], 2);
+    lits.insert(lit![2], 3);
+    test_pb!(
+        PBConstraint::new_eq(lits.clone(), 1),
+        vec![lit![0], !lit![1], !lit![2]],
+        vec![!lit![0], lit![1], lit![2]]
+    );
+    test_pb!(
+        PBConstraint::new_eq(lits.clone(), 2),
+        vec![!lit![0], lit![1], !lit![2]],
+        vec![!lit![0], !lit![1], !lit![2]]
+    );
+    test_pb!(
+        PBConstraint::new_eq(lits.clone(), 3),
+        vec![!lit![0], !lit![1], lit![2]],
+        vec![!lit![0], lit![1], !lit![2]]
+    );
+}
diff --git a/tests/opb.rs b/tests/opb.rs
new file mode 100644
index 00000000..2777eeb7
--- /dev/null
+++ b/tests/opb.rs
@@ -0,0 +1,84 @@
+use rustsat::{
+    instances::SatInstance,
+    lit, solvers,
+    solvers::SolverResult,
+    types::{constraints::PBConstraint, Lit},
+};
+use std::{collections::HashMap, path::Path};
+
+#[cfg(feature = "multiopt")]
+use rustsat::instances::MultiOptInstance;
+#[cfg(feature = "optimization")]
+use rustsat::instances::{Objective, OptInstance};
+
+macro_rules! opb_test {
+    ($path:expr, $expect:expr) => {{
+        let inst: SatInstance = SatInstance::from_opb_path(Path::new($path)).unwrap();
+        let (cnf, _) = inst.as_cnf();
+        println!("{:?}", cnf);
+        let mut solver = solvers::new_default_solver();
+        solver.add_cnf(cnf);
+        assert_eq!(solver.solve().unwrap(), $expect);
+    }};
+}
+
+#[test]
+fn opb_tiny_sat() {
+    opb_test!("./data/tiny-sat.opb", SolverResult::SAT);
+}
+
+#[test]
+fn opb_tiny_unsat() {
+    opb_test!("./data/tiny-unsat.opb", SolverResult::UNSAT);
+}
+
+#[cfg(feature = "optimization")]
+#[test]
+fn opb_opt() {
+    let inst: OptInstance = OptInstance::from_opb_path(Path::new("./data/tiny-opt.opb")).unwrap();
+    let mut true_constr = SatInstance::new();
+    let mut lits = HashMap::new();
+    lits.insert(lit![0], 5);
+    lits.insert(lit![1], -3);
+    true_constr.add_pb_constr(PBConstraint::new_lb(lits, 4));
+    let mut lits = HashMap::new();
+    lits.insert(lit![2], 5);
+    lits.insert(lit![3], -3);
+    true_constr.add_pb_constr(PBConstraint::new_lb(lits, 2));
+    let mut lits = HashMap::new();
+    lits.insert(!lit![3], 5);
+    true_constr.add_pb_constr(PBConstraint::new_lb(lits, 4));
+    let mut true_obj = Objective::new();
+    true_obj.add_soft_lit_int(1, lit![0]);
+    true_obj.add_soft_lit_int(2, lit![1]);
+    assert_eq!(inst, OptInstance::compose(true_constr, true_obj));
+}
+
+#[cfg(feature = "multiopt")]
+#[test]
+fn opb_multi_opt() {
+    let inst: MultiOptInstance =
+        MultiOptInstance::from_opb_path(Path::new("./data/tiny-opt.opb")).unwrap();
+    let mut true_constr = SatInstance::new();
+    let mut lits = HashMap::new();
+    lits.insert(lit![0], 5);
+    lits.insert(lit![1], -3);
+    true_constr.add_pb_constr(PBConstraint::new_lb(lits, 4));
+    let mut lits = HashMap::new();
+    lits.insert(lit![2], 5);
+    lits.insert(lit![3], -3);
+    true_constr.add_pb_constr(PBConstraint::new_lb(lits, 2));
+    let mut lits = HashMap::new();
+    lits.insert(!lit![3], 5);
+    true_constr.add_pb_constr(PBConstraint::new_lb(lits, 4));
+    let mut true_obj_1 = Objective::new();
+    true_obj_1.add_soft_lit_int(1, lit![0]);
+    true_obj_1.add_soft_lit_int(2, lit![1]);
+    let mut true_obj_2 = Objective::new();
+    true_obj_2.add_soft_lit_int(2, lit![2]);
+    true_obj_2.add_soft_lit_int(-3, !lit![3]);
+    assert_eq!(
+        inst,
+        MultiOptInstance::compose(true_constr, vec![true_obj_1, true_obj_2])
+    );
+}