sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-05-11T12:15:13Zhttps://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/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/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/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/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/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/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/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);
}
https://gitlab.ow2.org/sat4j/sat4j/-/issues/72Print the statistics of all solvers in manycore2018-04-13T11:56:15ZDaniel Le BerrePrint the statistics of all solvers in manycoreCurrently, only the statistics of the winner are displayed. We should display the statistics of all solvers.Currently, only the statistics of the winner are displayed. We should display the statistics of all solvers.https://gitlab.ow2.org/sat4j/sat4j/-/issues/90Better management of forgotten variables for undo-based constraints2018-04-13T11:56:17ZDaniel Le BerreBetter management of forgotten variables for undo-based constraintsSat4j allows to forget some variables during prime implicant computation.
It performs that operation by falsifying both the positive and negative literal associated with a variable.
It works fine for clauses and cardinality constraints.
...Sat4j allows to forget some variables during prime implicant computation.
It performs that operation by falsifying both the positive and negative literal associated with a variable.
It works fine for clauses and cardinality constraints.
However, there is an issue for constraints requiring a call to undo when backtracking.
The constraints to be considered when undoing an assignment is stored for a variable, not a literal. As such, when forgetting a variable, both the constraints where the positive and negative literal appears are part of that constraint. So a call to undo() on a constraint that does contains the literal will occur.
Worst, it is necessary to perform the undo both on the literal and its oppositve in that case, to properly undo all constraints.
In our testcases, the PB constraints are encoding the objective function and are deleted after each PI computation, so the current fix is simply to avoid a NPE that occurs when the undo() method is applied on a constraint not associated by such literal.
We are currently working on a new PI computation scheme, so that code with forget will eventually be removed. The current fix allows the solver to be correct, and prevents NPE to occur.https://gitlab.ow2.org/sat4j/sat4j/-/issues/93Find a way to factorize the various settings for the solvers2018-07-07T05:11:52ZDaniel Le BerreFind a way to factorize the various settings for the solversThe PB, MAXSAT and SAT launchers have their own code for configuring the solvers.
As such, it is quite tedious to update all the launchers when a new feature is added to the library (e.g. internal optimization).
The PB launcher does not...The PB, MAXSAT and SAT launchers have their own code for configuring the solvers.
As such, it is quite tedious to update all the launchers when a new feature is added to the library (e.g. internal optimization).
The PB launcher does not have any dependency to commons CLI, so is a bit different from the two others.
However, we need to find a central class to perform the configuration of solvers: note that in sat package, the configuration of the solvers is done twice, one in DetailedCommandPanel and one in Launcher.
https://gitlab.ow2.org/sat4j/sat4j/-/issues/97Allow Sat4j statistics to be visible using JMX2018-07-07T05:11:52ZDaniel Le BerreAllow Sat4j statistics to be visible using JMXJava allows external programs to access some objects values using JMX. Standard tools such as JConsole or VisualVM can then be used to monitor those values.
Will it is not clear yet if such approach could be used for the dashboard, we c...Java allows external programs to access some objects values using JMX. Standard tools such as JConsole or VisualVM can then be used to monitor those values.
Will it is not clear yet if such approach could be used for the dashboard, we could at least use it for providing an access to the solver statistics while the solver is running.https://gitlab.ow2.org/sat4j/sat4j/-/issues/102API for using an OPB string spec2018-07-07T05:11:52ZMihai BarbuceanuAPI for using an OPB string specHi Daniel,
Is there any API available that would allow me to read an OPB spec as a string (which I have stored previously in a database, for example) and run the PB solvers to get a solution? I would like to do this without going throug...Hi Daniel,
Is there any API available that would allow me to read an OPB spec as a string (which I have stored previously in a database, for example) and run the PB solvers to get a solution? I would like to do this without going through the command line.
Many Thanks,
Mihai