diff --git a/CMakeLists.txt b/CMakeLists.txt
index b2c37c4..9fb6ecc 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -28,7 +28,7 @@ if(${HEURISTIC_TYPE_INDEX} EQUAL -1)
 endif()
 message(STATUS "Heuristic type: ${HEURISTIC_TYPE}")
 
-add_library(oRatioLib src/solver.cpp src/graph.cpp src/flaw.cpp src/resolver.cpp src/smart_type.cpp src/flaws/atom_flaw.cpp src/flaws/bool_flaw.cpp src/flaws/disj_flaw.cpp src/flaws/disjunction_flaw.cpp src/flaws/enum_flaw.cpp)
+add_library(oRatioLib src/solver.cpp src/graph.cpp src/flaw.cpp src/resolver.cpp src/smart_type.cpp src/flaws/atom_flaw.cpp src/flaws/bool_flaw.cpp src/flaws/disj_flaw.cpp src/flaws/exact_one_flaw.cpp src/flaws/disjunction_flaw.cpp src/flaws/enum_flaw.cpp)
 target_link_libraries(oRatioLib PUBLIC RiDDLe SeMiTONE)
 target_include_directories(oRatioLib PUBLIC $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include> $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include/flaws> $<BUILD_INTERFACE:${CMAKE_CURRENT_BINARY_DIR}>)
 
diff --git a/include/flaws/disjunction_flaw.hpp b/include/flaws/disjunction_flaw.hpp
index d585583..d95b88e 100644
--- a/include/flaws/disjunction_flaw.hpp
+++ b/include/flaws/disjunction_flaw.hpp
@@ -8,14 +8,14 @@ namespace ratio
   class disjunction_flaw : public flaw
   {
   public:
-    disjunction_flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, std::vector<std::reference_wrapper<riddle::conjunction>> &&xprs) noexcept;
+    disjunction_flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, std::vector<std::unique_ptr<riddle::conjunction>> &&xprs) noexcept;
 
-    [[nodiscard]] const std::vector<std::reference_wrapper<riddle::conjunction>> &get_conjunctions() const noexcept { return xprs; }
+    [[nodiscard]] const std::vector<std::unique_ptr<riddle::conjunction>> &get_conjunctions() const noexcept { return xprs; }
 
   private:
     void compute_resolvers() override;
 
   private:
-    std::vector<std::reference_wrapper<riddle::conjunction>> xprs;
+    std::vector<std::unique_ptr<riddle::conjunction>> xprs;
   };
 } // namespace ratio
diff --git a/include/flaws/exact_one_flaw.hpp b/include/flaws/exact_one_flaw.hpp
new file mode 100644
index 0000000..ce68471
--- /dev/null
+++ b/include/flaws/exact_one_flaw.hpp
@@ -0,0 +1,20 @@
+#pragma once
+
+#include "flaw.hpp"
+
+namespace ratio
+{
+  class exact_one_flaw : public flaw
+  {
+  public:
+    exact_one_flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, std::vector<utils::lit> &&lits) noexcept;
+
+    [[nodiscard]] const std::vector<utils::lit> &get_lits() const noexcept { return lits; }
+
+  private:
+    void compute_resolvers() override;
+
+  private:
+    std::vector<utils::lit> lits;
+  };
+} // namespace ratio
diff --git a/src/flaws/disjunction_flaw.cpp b/src/flaws/disjunction_flaw.cpp
index a4bc4c1..c4a8eae 100644
--- a/src/flaws/disjunction_flaw.cpp
+++ b/src/flaws/disjunction_flaw.cpp
@@ -4,7 +4,7 @@
 
 namespace ratio
 {
-    disjunction_flaw::disjunction_flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, std::vector<std::reference_wrapper<riddle::conjunction>> &&xprs) noexcept : flaw(s, std::move(causes)), xprs(std::move(xprs))
+    disjunction_flaw::disjunction_flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, std::vector<std::unique_ptr<riddle::conjunction>> &&xprs) noexcept : flaw(s, std::move(causes)), xprs(std::move(xprs))
     {
         assert(!xprs.empty());
     }
diff --git a/src/flaws/exact_one_flaw.cpp b/src/flaws/exact_one_flaw.cpp
new file mode 100644
index 0000000..e2ecff6
--- /dev/null
+++ b/src/flaws/exact_one_flaw.cpp
@@ -0,0 +1,16 @@
+#include <cassert>
+#include "exact_one_flaw.hpp"
+#include "solver.hpp"
+
+namespace ratio
+{
+    exact_one_flaw::exact_one_flaw(solver &s, std::vector<std::reference_wrapper<resolver>> &&causes, std::vector<utils::lit> &&lits) noexcept : flaw(s, std::move(causes)), lits(lits)
+    {
+        assert(!lits.empty());
+    }
+
+    void exact_one_flaw::compute_resolvers()
+    {
+        throw std::runtime_error("Not implemented yet");
+    }
+} // namespace ratio
diff --git a/src/solver.cpp b/src/solver.cpp
index 88de99a..3f8713a 100644
--- a/src/solver.cpp
+++ b/src/solver.cpp
@@ -6,6 +6,9 @@
 #include "smart_type.hpp"
 #include "atom_flaw.hpp"
 #include "bool_flaw.hpp"
+#include "disj_flaw.hpp"
+#include "exact_one_flaw.hpp"
+#include "disjunction_flaw.hpp"
 #include "logging.hpp"
 
 namespace ratio
@@ -19,6 +22,9 @@ namespace ratio
         LOG_DEBUG("[" << name << "] Initializing solver");
         // we read the init string..
         read(INIT_STRING);
+
+        if (!sat.propagate())
+            throw riddle::unsolvable_exception();
     }
 
     void solver::read(const std::string &script)
@@ -271,7 +277,7 @@ namespace ratio
         lits.reserve(exprs.size());
         for (const auto &xpr : exprs)
             lits.push_back(xpr->get_value());
-        return std::make_shared<riddle::bool_item>(get_bool_type(), sat.new_disj(std::move(lits)));
+        return std::make_shared<riddle::bool_item>(get_bool_type(), gr.new_flaw<disj_flaw>(*this, std::vector<std::reference_wrapper<resolver>>(), std::move(lits)).get_phi());
     }
     std::shared_ptr<riddle::bool_item> solver::exct_one(const std::vector<std::shared_ptr<riddle::bool_item>> &exprs)
     {
@@ -279,7 +285,7 @@ namespace ratio
         lits.reserve(exprs.size());
         for (const auto &xpr : exprs)
             lits.push_back(xpr->get_value());
-        throw std::runtime_error("Not implemented yet");
+        return std::make_shared<riddle::bool_item>(get_bool_type(), gr.new_flaw<exact_one_flaw>(*this, std::vector<std::reference_wrapper<resolver>>(), std::move(lits)).get_phi());
     }
     std::shared_ptr<riddle::bool_item> solver::negate(const std::shared_ptr<riddle::bool_item> &expr) { return std::make_shared<riddle::bool_item>(get_bool_type(), !expr->get_value()); }
 
@@ -289,10 +295,7 @@ namespace ratio
             throw riddle::unsolvable_exception();
     }
 
-    void solver::new_disjunction(std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts) noexcept
-    {
-        throw std::runtime_error("Not implemented yet");
-    }
+    void solver::new_disjunction(std::vector<std::unique_ptr<riddle::conjunction>> &&disjuncts) noexcept { gr.new_flaw<disjunction_flaw>(*this, std::vector<std::reference_wrapper<resolver>>(), std::move(disjuncts)); }
 
     std::shared_ptr<riddle::atom> solver::new_atom(bool is_fact, riddle::predicate &pred, std::map<std::string, std::shared_ptr<riddle::item>> &&arguments) noexcept
     {