sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-05-11T12:15:13Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/1Use a specific data structure for binary clauses compatible with reason simpl...2018-05-11T12:15:13ZDaniel Le BerreUse a specific data structure for binary clauses compatible with reason simplificationThe support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because th...The support for binary clauses as proposed by Lawrence Ryan in his thesis was removed because not compatible with reason simplification.
There are many cases where the amount of memory is huge and the unit propagation is slow because the instance is mainly composed of binary clauses.
We should add back such data structure in order to reduce the memory footprint of the solver on such problems. It will only happen if we find a nice solution compatible with reason simplification.https://gitlab.ow2.org/sat4j/sat4j/-/issues/4Provide a representation of pseudo boolean constraints with primitive type lo...2018-05-11T12:15:13ZDaniel Le BerreProvide a representation of pseudo boolean constraints with primitive type long instead of BigIntegerPseudo boolean constraints are currently using BigInteger for representing coefficients and degrees.
If this is the only option for cutting planes based inference, it would be cheaper to use when possible primitive types for those const...Pseudo boolean constraints are currently using BigInteger for representing coefficients and degrees.
If this is the only option for cutting planes based inference, it would be cheaper to use when possible primitive types for those constraints, to efficiently propagate truth values.
One could choose either int or long for that.
long is probably a good tradeoff between the space required to store the information and the number of cases in which it will apply. Since we are going to 64 bits arch, long should be handled natively by the JVMs at some point.2.3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/11Allow creation of ManyCore solver from a list/array of existing solvers inste...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of ManyCore solver from a list/array of existing solvers instead of their name in a factoryIt is currently impossible to create a new multi solver using existing solvers. One need to use a solver factory and a list of name instead.
It would be simpler to also allow the multi solver to reuse existing solvers.It is currently impossible to create a new multi solver using existing solvers. One need to use a solver factory and a list of name instead.
It would be simpler to also allow the multi solver to reuse existing solvers.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/12Use List instead of IVec in DependencyHelper.getSolution()2018-05-11T12:15:13ZDaniel Le BerreUse List instead of IVec in DependencyHelper.getSolution()Currently, the DependencyHelper class returns an IVec object, i.e. a Sat4j specific data structure.
Since the DependencyHelper is supposed to be embedded in Java software, it is probably wise to use only Java classical data structure to...Currently, the DependencyHelper class returns an IVec object, i.e. a Sat4j specific data structure.
Since the DependencyHelper is supposed to be embedded in Java software, it is probably wise to use only Java classical data structure to interact with that class.
We could use for instance a java.util.List object instead of an IVec.
The main issue here is that it would break the API: the DependencyHelper class exists since Sat4j 2.1.
2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/15Allow to reset the DependencyHelper2018-05-11T12:15:13ZDaniel Le BerreAllow to reset the DependencyHelperThere is currently no way to reset a DependencyHelper. In some cases, it might be useful to reset it, i.e. to clear its mapping, objective function and solver.There is currently no way to reset a DependencyHelper. In some cases, it might be useful to reset it, i.e. to clear its mapping, objective function and solver.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/19Allow creation of clauses, cardinality and pseudo boolean constraints using a...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of clauses, cardinality and pseudo boolean constraints using arrays of primitive typeWhen creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.When creating test cases, it is painful for many users to create feed VecInt to create new clauses.
It would be much simpler to simply use arrays of integers in addClause for instance.https://gitlab.ow2.org/sat4j/sat4j/-/issues/24Add statistics about SAT/UNSAT calls2018-05-11T12:15:13ZDaniel Le BerreAdd statistics about SAT/UNSAT callsWhen doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.When doing optimization, it is sometimes useful to be able to get some statistics about the number of calls to the SAT solver, and how much time is spent for SAT and UNSAT.https://gitlab.ow2.org/sat4j/sat4j/-/issues/25Allow input string to be read properly using InputStream or Reader2018-05-11T12:15:13ZDaniel Le BerreAllow input string to be read properly using InputStream or ReaderFor the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is ...For the moment, if the user does not want to use a file to feed the solver, the only possibility it is use an InputStream.
That method is however not supported in the generic InstanceReader class, and the possibility to use a Reader is not supported in some readers.
Not a big deal to fix, but need to be done properly.https://gitlab.ow2.org/sat4j/sat4j/-/issues/28Allow easy explanation for OPB file2022-04-09T17:42:39ZDaniel Le BerreAllow easy explanation for OPB fileCurrently, using ExplainPB on an opb file does not provide an explanation of inconsistency with the explain method because there are no "names" associated with the constraints.
One should allow to use constraint numbers in that case, to...Currently, using ExplainPB on an opb file does not provide an explanation of inconsistency with the explain method because there are no "names" associated with the constraints.
One should allow to use constraint numbers in that case, to easily display the unsat core in terms of constraints number (might not be that good because an equality constraint is splitted into 2 constraints).https://gitlab.ow2.org/sat4j/sat4j/-/issues/33Improve project documentation (including web site)2018-07-07T05:11:52ZDaniel Le BerreImprove project documentation (including web site)Sat4j is mainly a research project, used to try our ideas around SAT. We start to receive more and more calls for help in the forums, which is nice because it shows that Sat4j is used, but it is also a sign that the documentation is not ...Sat4j is mainly a research project, used to try our ideas around SAT. We start to receive more and more calls for help in the forums, which is nice because it shows that Sat4j is used, but it is also a sign that the documentation is not good enough.
The tools we are using have evolved recently. Jira for instance should appear prominently on the web site while it does not, so we need to redirect users there.
We are going to design a new web site for next year (2012). Please use this bug report to tell us what you would like to see there.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/34Make sure that all solvers return a unit clause in addClause2018-07-07T05:11:52ZDaniel Le BerreMake sure that all solvers return a unit clause in addClauseIn many cases, to allow the end user to easily remove unit clauses or constraints that propagate literals, we retour UnitClause or UnitClauses objects in the addXxxx() methods.
However, especially in the simple SAT case, that behavior i...In many cases, to allow the end user to easily remove unit clauses or constraints that propagate literals, we retour UnitClause or UnitClauses objects in the addXxxx() methods.
However, especially in the simple SAT case, that behavior is not enforced for all DataStructureFactory.
We thus need to make sure that all DSF do return a UnitClause object instead of null when a unit clause is detected.
2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/36Allow pretty printing of solutions2018-07-07T05:11:53ZDaniel Le BerreAllow pretty printing of solutionsWe currently generate very long lines with the solution of the problem (SAT, PB or MAXSAT).
We have OutOfMemory problems when displaying a solution after a OOM exception has ben launched.
It would probably not happen is the output stre...We currently generate very long lines with the solution of the problem (SAT, PB or MAXSAT).
We have OutOfMemory problems when displaying a solution after a OOM exception has ben launched.
It would probably not happen is the output stream is flushed regularly, i.e. after a limited amount of literals in the solution line.
It would therefore be nice to have a way to pretty print the solution line.
The only issue is that it may break scripts that simply do a grep to retrieve the solution.https://gitlab.ow2.org/sat4j/sat4j/-/issues/38Investigate usage of plain CNF rather than custom cardinality of PB constraints2018-07-07T05:11:53ZDaniel Le BerreInvestigate usage of plain CNF rather than custom cardinality of PB constraintsSat4j uses by default a custom constraint for cardinality and PB constraints.
The main advantage is to reduce the memory needed to represent the constraints. However, it requires ad hoc propagation and analysis procedure.
Many solvers fo...Sat4j uses by default a custom constraint for cardinality and PB constraints.
The main advantage is to reduce the memory needed to represent the constraints. However, it requires ad hoc propagation and analysis procedure.
Many solvers for solving MaxSat problems rely on cardinality of PB translation into SAT.
It would be nice to be able to easily try in sat4j the effect of pure clausal encodings against current solution.2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/39Add the possibility to create a constraint k among n in IProblem2018-07-07T05:11:53ZDaniel Le BerreAdd the possibility to create a constraint k among n in IProblemIn the pseudo boolean competition, and in many situations, it is important to be able to create a constraint that satisfies exactly k variables among n.
The current way to proceed in Sat4j is to create both a <= and a >= constraints.
T...In the pseudo boolean competition, and in many situations, it is important to be able to create a constraint that satisfies exactly k variables among n.
The current way to proceed in Sat4j is to create both a <= and a >= constraints.
That's fine. However, there are possibilities to encode directly such kind of constraints in the solver.
As such, it would be great to provide a new method for that in the API, even if the current implementation remains unchanged.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/41Use a specific data structure to locate efficiently the weight associated to ...2018-07-07T05:11:53ZDaniel Le BerreUse a specific data structure to locate efficiently the weight associated to a literal in a counter based constraintAfter checking the reason for inefficiency of Sat4j on specific benchmarks, it turns out that large counter based constraints have a bottleneck:
// finding the index for p in the array of literals
int indiceP = 0;
while ((lits[ind...After checking the reason for inefficiency of Sat4j on specific benchmarks, it turns out that large counter based constraints have a bottleneck:
// finding the index for p in the array of literals
int indiceP = 0;
while ((lits[indiceP] ^ 1) != p)
indiceP++;
Using an auxiliary array or map to store the location of the literals instead of going through that loop will probably make the propagation and undo much faster.
(hint: use an array when the size of the constraint contains at least half of the variables, else use a map).2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/42Allow Sat4j to use bunzip2 to uncompress on the fly bz2 (and possibly others)...2018-07-07T05:11:53ZDaniel Le BerreAllow Sat4j to use bunzip2 to uncompress on the fly bz2 (and possibly others) compressed filesBenchmarks take more and more space, so they are usually stored in a compressed form.
Java has a built in support for zip file, but not for bz2 files.
One pragmatic way to add support for bz2 (and maybe 7z compressed files), is to use p...Benchmarks take more and more space, so they are usually stored in a compressed form.
Java has a built in support for zip file, but not for bz2 files.
One pragmatic way to add support for bz2 (and maybe 7z compressed files), is to use platform specific decoders, e.g. bunzip2 on unix platform.
This is how abscon is managing bz2 files, and it works fine for both Linux and Mac Os X.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/43Allow the solver to be aware of the user defined max var id2018-07-07T05:11:53ZDaniel Le BerreAllow the solver to be aware of the user defined max var idWhen using SAT encodings, it is often necessary to create new variables on the fly.
This is true for instance in the translation from MaxSAT to PBO, from Card to SAT, etc.
In that context, it is important to make a difference between th...When using SAT encodings, it is often necessary to create new variables on the fly.
This is true for instance in the translation from MaxSAT to PBO, from Card to SAT, etc.
In that context, it is important to make a difference between the original max var id
and the maxvarid after adding the new variables.
It is assumed in most cases in Sat4j that the user defined maxvarid is defined using the method
ISolver.newVar(int maxvarid)
Then new variables can be retrieved using nextFreeVarId().
We could for instance fix the value set using newVar() and add a method to retrieve it.
That way, the model iterator for instance could use that value instead of the current nVar().2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/45Separate MS and PWMS decorator from the optimization method2018-07-07T05:11:53ZDaniel Le BerreSeparate MS and PWMS decorator from the optimization methodSince we now have two methods for optimizing, lower bounding and upper bounding, we need to have the decorators used in MaxSat independent of the optimization method.
This basically means that the decorator should not optimize the probl...Since we now have two methods for optimizing, lower bounding and upper bounding, we need to have the decorators used in MaxSat independent of the optimization method.
This basically means that the decorator should not optimize the problem, it should delegate that to a PseudoOptDecorator or a ConstraintRelaxingPseudoOptDecorator.
Since we use here new variables, it means updating the current pseudo-opt decorators to deal with additional variables.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/59Use package-info.java instead of package.html for package JavaDoc2019-01-03T09:55:37ZDaniel Le BerreUse package-info.java instead of package.html for package JavaDocThere are some package documentation missing.
The preferred way to document packages since Java 5 is to use a package-info.java file instead of a package.html file in the package.
When working on improving the Javadoc, we should move t...There are some package documentation missing.
The preferred way to document packages since Java 5 is to use a package-info.java file instead of a package.html file in the package.
When working on improving the Javadoc, we should move the current package documentation inside package-info.java files.
See http://docs.oracle.com/javase/6/docs/technotes/tools/solaris/javadoc.html#packagecomment for details.
2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/62Expose solver stats and info programatically2018-05-11T12:15:13ZPablo AbadExpose solver stats and info programaticallyCurrently, the Solver class exposes several methods that can be used to get insight into different solver metrics:
void printStat(PrintWriter out, String prefix)
void printStat(PrintStream out, String prefix)
int nVars()
void printLearnt...Currently, the Solver class exposes several methods that can be used to get insight into different solver metrics:
void printStat(PrintWriter out, String prefix)
void printStat(PrintStream out, String prefix)
int nVars()
void printLearntClausesInfos(PrintWriter out, String prefix)
void printInfos(PrintWriter out, String prefix)
Map<String, Number> getStat()
long getTimeoutMs()
int realNumberOfVariables()
int nConstraints()
While some of these methods may be used while building constraints, most of them return information about the problem being represented and status of the solving process.
Furthermore, some of this information can't be accessed programatically, but printed to a Stream or Writer.
The proposal would be to create an interface that provides methods for retrieving all these information and add a method in Solver that returns an implementation of this interface. Ideally, all the printXXX methods could be moved from Solver into another class that would receive this interface.
Here is a possible draft of this interface:
public interface SolverStats {
int numberOfVars();
int realNumberOfVars();
int nContraints();
void observeStats(StatObserver observer);
void observeConstraintTypes(ConstraintTypeObserver observer);
void observeLearnedConstraintTypes(ConstraintTypeObserver observer);
}
public interface StatObserver {
public void observe(String stat, Number value);
// or a method per value type
}
public interface ConstraintTypeObserver {
public void observe(String type, int count);
}