<p>I have to list the solutions to the following hypergraph problem:</p>
<p>There is a set of nodes, linked by edges that are 2-to-1 and bidirectional. The possible directions are either <em>direct</em>: 2 sources and 1 target, or <em>reverse</em>: 1 source and 2 targets. A node cannot appear on both sides, but the 2 sources (resp. targets) can be 2 occurences of the same node.</p>
<p>A <strong>nice cycle</strong> in such a hypergraph is a subset <span class="math-container">$N$</span> of nodes and a subset <span class="math-container">$E$</span> of edges together with a choice of direction <span class="math-container">$d:E\to\{\mathit{direct},\mathit{reverse}\}$</span> for each edge of <span class="math-container">$E$</span>, such that:</p>
<ul>
<li><span class="math-container">$|N|=|E|$</span></li>
<li>each node of <span class="math-container">$N$</span> is a source of exactly 1 edge from <span class="math-container">$E$</span>. (This induces a bijection <span class="math-container">$N\to E$</span>)</li>
<li>each node of <span class="math-container">$N$</span> appears as the target of at least 1 edge from <span class="math-container">$E$</span>.</li>
<li>there is a node of <span class="math-container">$N$</span> appearing twice as target of an edge of <span class="math-container">$E$</span> (possibly of the same edge).</li>
</ul>
<p>A nice cycle <span class="math-container">$C=(N,E,d)$</span> is <strong>included</strong> in <span class="math-container">$C'=(N',E',d')$</span> if  <span class="math-container">$N\subseteq N'$</span>, <span class="math-container">$E\subseteq E'$</span>, and <span class="math-container">$d$</span> is the restriction of <span class="math-container">$d'$</span> to <span class="math-container">$E$</span>. A nice cycle is <strong>minimal</strong> if no other nice cycle is included in it.</p>
<p>All of this can also be modelled with linear algebra, where a (minimal) nice cycle is an invertible square submatrix with additional conditions, but I leave out the details of this here to keep the question short and to the point.</p>
<p>Given a hypergraph, I want to list its minimal nice cycles for a practical application. I already proved that the problem of finding a nice cycle containing some nodes is NP-complete, so my first reflex was to use a SAT-solver. But when I started to work on implementation details, I realized that other kinds of solvers could be more efficient for this problem, for instance SMT solvers or Linear Programming.</p>
<p>So if you have some experience with such solvers, what do you think is best for this problem ? I am also interested in recommendations for specific solvers (like Z3) and/or implementation choices if you have some tricks of the trade.</p>

CC BY-SA 4.0
2023-03-17T14:27:33.837Z
My two cents: 
For SAT solvers, the current best one is clearly Kissat. Glucose 4.1 is also efficient. But both require à CNF formula as input.
I don't recommand Z3. It's really slow. It's mostly used for higher order logic (which neither Kissat nor Glucose tackle). But it doesn't require a CNF input. 
Surprisigly, I never found any quick and simple software that converts a SAT formula into CNF. I always do it "by hand".
For (I)LP solvers, I tried a lot open source softwares, but none of them was as efficient as CPLEX and Gurobi. I think that you can get the former as an academic.
Lamine
CC BY-SA 4.0
2023-03-17T14:38:51.340Z
@Lamine Thanks, I didn't know Kissat, do you know how it compares to Minisat ? (the one I currently use)
Denis
CC BY-SA 4.0
2023-03-17T14:46:40.393Z
It is much faster. Glucose is an "overlay" of Minisat, which is outdated for more than a decade. You can see the results of the 2020 SAT competition: http://fmv.jku.at/kissat/
Lamine
CC BY-SA 4.0
2023-03-17T16:44:16.653Z
@Lamine, you can also get a free academic license for Gurobi.  https://www.gurobi.com/academia/academic-program-and-licenses/
Neal Young
CC BY-SA 4.0
2023-03-17T23:00:21.213Z
@Lamine I'm trying to use kissat, but there are no instructions on how to install it and use it, do you have a pointer for this ? I can clone it and do ./configure && make test, it seems happy, but then I'm kind of stuck.
Denis
CC BY-SA 4.0
2023-03-19T22:24:50.293Z
I finally found the kissat executable and the "kissat --help" command explaining how it works, let's see what it can do :)
Denis
<sat><linear-programming><np-complete><hypergraphs>
What kind of solver should I use for this hypergraph problem?
Denis
# What kind of solver should I use for this hypergraph problem?

(Asked by: username_0 on 2023-03-17)

I have to list the solutions to the following hypergraph problem:

There is a set of nodes, linked by edges that are 2-to-1 and bidirectional. The possible directions are either *direct*: 2 sources and 1 target, or *reverse*: 1 source and 2 targets. A node cannot appear on both sides, but the 2 sources (resp. targets) can be 2 occurences of the same node.

A **nice cycle** in such a hypergraph is a subset $N$ of nodes and a subset $E$ of edges together with a choice of direction $d:E\to\{\mathit{direct},\mathit{reverse}\}$ for each edge of $E$, such that:

* $|N|=|E|$
* each node of $N$ is a source of exactly 1 edge from $E$. (This induces a bijection $N\to E$)
* each node of $N$ appears as the target of at least 1 edge from $E$.
* there is a node of $N$ appearing twice as target of an edge of $E$ (possibly of the same edge).

A nice cycle $C=(N,E,d)$ is **included** in $C'=(N',E',d')$ if $N\subseteq N'$, $E\subseteq E'$, and $d$ is the restriction of $d'$ to $E$. A nice cycle is **minimal** if no other nice cycle is included in it.

All of this can also be modelled with linear algebra, where a (minimal) nice cycle is an invertible square submatrix with additional conditions, but I leave out the details of this here to keep the question short and to the point.

Given a hypergraph, I want to list its minimal nice cycles for a practical application. I already proved that the problem of finding a nice cycle containing some nodes is NP-complete, so my first reflex was to use a SAT-solver. But when I started to work on implementation details, I realized that other kinds of solvers could be more efficient for this problem, for instance SMT solvers or Linear Programming.

So if you have some experience with such solvers, what do you think is best for this problem ? I am also interested in recommendations for specific solvers (like Z3) and/or implementation choices if you have some tricks of the trade.

**Tags:** sat, linear-programming, np-complete, hypergraphs
> **Comments:**
> **username_1**: My two cents:  For SAT solvers, the current best one is clearly Kissat. Glucose 4.1 is also efficient. But both require à CNF formula as input. I don't recommand Z3. It's really slow. It's mostly used for higher order logic (which neither Kissat nor Glucose tackle). But it doesn't require a CNF input.  Surprisigly, I never found any quick and simple software that converts a SAT formula into CNF. I always do it "by hand". For (I)LP solvers, I tried a lot open source softwares, but none of them was as efficient as CPLEX and Gurobi. I think that you can get the former as an academic.  
> **username_0**: @Lamine Thanks, I didn't know Kissat, do you know how it compares to Minisat ? (the one I currently use)  
> **username_1**: It is much faster. Glucose is an "overlay" of Minisat, which is outdated for more than a decade. You can see the results of the 2020 SAT competition: http://fmv.jku.at/kissat/  
> **username_2**: @Lamine, you can also get a free academic license for Gurobi.  https://www.gurobi.com/academia/academic-program-and-licenses/  
> **username_0**: @Lamine I'm trying to use kissat, but there are no instructions on how to install it and use it, do you have a pointer for this ? I can clone it and do ./configure && make test, it seems happy, but then I'm kind of stuck.  
> **username_0**: I finally found the kissat executable and the "kissat --help" command explaining how it works, let's see what it can do :)  

---

## 0 answers

