Release Notes
Version 1.7.3 (Sep 27, 2021)
Version 1.7.2 (Aug 11, 2020)
- Extended OptiMathSAT API: opt.priority can now be set after the creation of the environment.
Version 1.7.1 (Jun 4, 2020)
- FlatZinc: support for half-reified predicates
- Other minor fixes
[HotFix] 1.7.0.1 (May 13, 2020)
- Fixed Bug in Java API (thanks to Karlheinz Friedberger)
Version 1.7.0 (May 10, 2020)
This is a major release due to important changes to OptiMathSAT's input/output.
Initial lower/upper bounds are no longer necessary and have thus been removed from
the input interfaces and the API.
Other changes:
- Synch with MathSAT 5.6.2 (see MathSAT 5 release notes)
- OMT(NIRA): improved effectiveness of search cuts
- Boxed(OMT): new incremental engines
- Boxed(OMT): DPLL engine can now use binary and adaptive search
- FlatZinc: can now print models with finite precision
- FlatZinc: can now dump internal mapping between SMT-LIB
and FlatZinc variables
- Other minor fixes
Version 1.6.4 (Feb 25, 2020)
- Synch with MathSAT 5.6.0 (see MathSAT 5 release notes)
- OMT(LIRA): initial bounds are no longer neccessary for using the binary and adaptive search strategies
- OMT(NIRA): experimental support (note: requires option -preprocessor.toplevel_propagation=False)
- FlatZinc: it is no longer necessary to sort
bool2int and int2float
constraints to appear at the beginning of the constraints section
- FlatZinc: improved handling of Pseudo-Boolean constraints
- Python API: MathSAT and OptiMathSAT can now be loaded within the same environment side by side
- Other minor fixes
Version 1.6.3 (May 13, 2019)
- FlatZinc: fixed regression with the option -opt.fzn.all_solutions=True
- Examples: added OMT(FP) to OMT(BV) reduction example
- Other minor fixes
Version 1.6.2 (Mar 18, 2019)
- Python API fixed regression, major cleanup and simplification
- Binary search with OMT(BV) no longer requires an initial lower/upper bound
- FlatZinc: added missing float_div/float_times constraints
Version 1.6.1 (Mar 04, 2019)
- Synch with MathSAT 5.5.4 (see MathSAT 5 release notes)
- Updated FP Optimization engines to comply with the stable definition of OMT(FP) optimization
- Binary search with OMT(FP) no longer requires an initial lower/upper bound
- Several Minor Fixes
Version 1.6.0 (Nov 26, 2018)
This is a major release due to important changes to OptiMathSAT's input/api.
These changes were mandated by the ongoing process of integration with MathSAT5.
- Synch with MathSAT 5.5.3 (see MathSAT 5 release notes)
- Added explicit option for using the OBV-WA engine
- Added OFPBS engine for Floating-Point optimization
- Improvements to the Pareto Engine
- The SmtLibv2 Extension set-model is now load-objective-model
- Several Fixes
The following changes affect OptiMathSAT interface for FlatZinc:
- Optional BV-encoding of Int expressions
Version 1.5.1 (Mar 01, 2018)
The set of SmtLibv2 optimization extensions has been updated,
please refer to the docs.
- BitVector Optimization: OBV-BS engine
- OMT-based Floating Point Optimization
- non-incremental allsat is now supported in single-objective and lexicographic optimization
- various minor improvements and bug fixes
The following changes affect OptiMathSAT interface for FlatZinc:
- It is now possible to print all solutions
- It is now possible to print sub-optimal solutions when optimizing
Version 1.5.0 (Jan 15, 2018)
This is a major release due to important changes to OptiMathSAT's input/output.
In order to use OptiMathSAT with the old output format, enable the following options:
-opt.print_objectives=True
-opt.output_format=old
Other changes:
- Synch with MathSAT 5.5.1 (see MathSAT 5 release notes)
- Pareto Optimization is now supported
- Signed/Unsigned BitVector Optimization is now supported
Add the following option to a BV objective declaration to mark it as signed::signed true
- The SmtLibv2 extension (get-objectives) is now supported.
- Fixed timeout in boxed optimization
- Fixed tolerance/interval thresholds behaviour
- Other minor improvements
The following changes affect OptiMathSAT interface for FlatZinc:
- Pareto optimization is now supported
- Fixed various bugs
- Hugely extended the list of supported constraints
- Other minor improvements
Version 1.4.5 (Aug 21, 2017)
- OptiMathSAT now pre-loads optimum model in the environment in the following cases:
- single-objective optimization
- lexicographic optimization
The following changes affect OptiMathSAT interface for FlatZinc:
- Multi-objective optimization is now supported
- Option opt.fzn.var_substitution removed: enhancement is now permanent
- Fixed bug in constraints (at_most, at_least, int_div, int_mod)
- Fixed bug in model printing
- Improved encoding of constraints (float_abs, float_min, float_max, int_abs,
int_min, int_max, int_div, int_mod, bool2int, set_card,
set_make_min_sym_diff, at_least_set, at_most_set, exactly_set, among,
count_leq, count_eq, count_gt, count_geq, count_lt, count_neq,
distribute, at_most_1)
- Improved early unsat detection
- Improved handling of ITE encoding
- Improved auto-detection of PB terms
- Other minor improvements
Version 1.4.4 (Jul 25, 2017)
- Fixed bug in LAZ optimization
- Fixed sig-sev due to (get-value) being called on an empty model
- Extended Api Tracer to handle optional id: attribute introduced with OptiMathSAT 1.4.2
The following changes affect OptiMathSAT interface for FlatZinc:
- FlatZinc attributes ::output_var and ::output_array() are now supported
- New option -opt.fzn.use_ite_encoding: if true, 0-1 variables are replaced with corresponding ITE terms whenever possible.
Note: for best performance, 'bool2int' constraints should appear as early as possible in the input model.
- New option opt.fzn.var_substitution: if true, aliases for existing variables are removed from the formula
- FlatZinc constraints: OptiMathSAT now tries to prevent non-linear moltiplication among variables in the encoding
- Fixed bug caused by incorrect handling of some variables with fragmented domain
- Fixed bug caused by incorrect handling of some boolean arrays
- Fixed bug in all-different handling
- Fixed auto-detection of PB terms in FlatZinc constraints
Version 1.4.3 (May 15, 2017)
Version 1.4.2 (May 08, 2017)
- Synch with MathSAT 5.4.0 (see MathSAT 5 release notes)
- Added Difference Logic T-Solver with ad-hoc learning of T-Lemmas based on conflict-interpolation (used by wcet_omt)
- Added :id attribute to extended SmtLibv2 format to simplify combination of objectives
- Changed options, now shorter and cleaner (old options are deprecated but still available)
- Minor fixes to External MaxSAT engine handling based on Lemma Lifting approach
- Fixed bug when using OptiMathSAT incrementally via C API
- Minor fixes
Version 1.4.1 (Sep 29, 2016)
- Synch with MathSAT 5.3.13 (see MathSAT 5 release notes)
- Added Maximum Resolution MaxSAT engine for dealing with Partial Weighted MaxSMT problems
- Added Lemma Lifting with external MaxSAT engine for dealing with Partial Weighted MaxSMT problems
- Added optional automatic encoding of Pseudo-Boolean terms in FlatZinc formulas into assert-soft statements
- API Tracer: optional expansion of soft-clauses into smt-based encoding
- Minor improvements
Version 1.4.0 (May 04, 2016)
This is a major release due to important changes to OptiMathSAT interface:
- Synch with MathSAT 5.3.11 (see MathSAT 5 release notes)
- Introduced new experimental support for (a subset of) the FlatZinc 1.6 input format
- assert-soft: weight and dweight annotations are now interchangeable
- Fixed minor bugs
Version 1.3.10 (Jan 08, 2016)
- Synch with MathSAT 5.3.10 (see MathSAT 5 release notes)
- Fixed bug caused by an attempt of popping the environment without a previous push (submitted by George Karpenkov)
- Lexicographic Optimization + Soft Timeout: optimum model is now pre-loaded in the environment
- assert-soft: 0-valued weights are now allowed
- assert-soft: negative-valued weights are now allowed
- Minor improvements
Version 1.3.9 (Dec 29, 2015)
- Synch with MathSAT 5.3.9 (see MathSAT 5 release notes)
- Optional Soft Timeout: during the optimization search, the timeout is delayed if no sub-optimal solution has not been found yet
NOTE: when using this option, the timeout value should be large enough (> few seconds) to give the solver a chance to start the optimization search.
- Optional auto-detection of MaxSMT bounds is now disabled by default
- Minor Fixes
Version 1.3.8 (Nov 13, 2015)
- Performance Improvement: from now on, the circuit_limit option affects the sequential counter encoding only
- Fixed regression impeding auto-detection of maxsmt objective bounds
- Fixed regression causing incorrect lexicographic optimization results
- Fixed the sequential counter circuit encoding value propagation
- Fixed crash when Theory Combination was disabled
Version 1.3.7 (Oct 11, 2015)
- Extended the MathSAT 5 API Tracer to work with optimization problems
- Extended the MathSAT 5 support for the SmtLib v. 2.5 Standard to include optimization problems
- C API: now a handler is returned upon creation of an objective instance
- Fixed regression causing optimization with timeout not printing any output
- Fixed other minor bugs
- Updated OptiMathSAT default configuration for solving MaxSMT problems
Version 1.3.6 (Oct 03, 2015)
- Synch with MathSAT 5.3.8 (see MathSAT 5 release notes)
- Better integration with Model-Based Theory Combination
- Fixed minor bugs
Version 1.3.5 (Aug 11, 2015)
- Reduced memory usage of the automatic advanced MaxSMT/Pseudo-Boolean encoding (see option '-optimization.circuit_limit')
- Improved performance when solving MaxSMT/Pseudo-Boolean problems
- Fixed bug causing crash on OMT(LA) problems with ghost_filtering and pure_literal_filtering enabled
- Fixed minor bug
Version 1.3.4 (Aug 04, 2015)
- Synch with MathSAT 5.3.7 (see MathSAT 5 release notes)
- Introduced automatic advanced MaxSMT/Pseudo-Boolean problems encoding through soft-clauses, option: -optimization.card_constr_encoding=INT
- 0 : basic encoding
- 1 : sequential counter circuit encoding, complexity O(n*n)
- 2 : sorting network circuit encoding, complexity O(n*log(n)*log(n))
Simple MaxSMT Objectives are automatically assigned upper and lower bounds for binary/adaptive search
- Private variables are no longer shown when (get-model) is invoked
- Now soft-clauses can be used to encode Pseudo-Boolean problems even when no objective is on stack
- Fixed bug that caused non-optimal model being printed for trivial problems
- Fixed other minor bugs
Version 1.3.3 (Jul 03, 2015)
- Synch with MathSAT 5.3.6 (see MathSAT 5 release notes)
- Fixed bug that caused incorrect model being printed in some cases
- Fixed bug when using timed optimization through API
Version 1.3.2 (Mar 23, 2015)
Version 1.3.1 (Feb 16, 2015)
- Introduced native support to maximization
- Improved optimization routines
- Fixed minor bug
Version 1.3.0 (Feb 11, 2015)
This is a major release due to important changes to OptiMathSAT interface:
- Introduced new SmtLibv2 extensions for interacting with OptiMathSAT
- Introduced new C API bindings for interacting with OptiMathsat
- Fixed minor bugs
Version 1.2.3 (Jan 29, 2015)
- Fixed bug of LAR model generation in MO boxed optimization mode
- Fixed bug of search status in MO boxed optimization mode
Version 1.2.2 (Jan 15, 2015)
- Fixed incorrect handling of unbounded Lexicographic problems
Version 1.2.1 (Dec 17, 2014)
- Added lexicographic optimization of multiple objectives
- Fixed bug in LAR minimizer with MILP problems
- Fixed bug in LAZ minimizer with ILP problems
Version 1.2.0 (Nov 12, 2014)
This is a major release, with several new features:
- Added support to optimizing integral cost functions
- Added support for incremental optimization
- Added support to multi-objective optimization
- Added C++ OptiMathSAT API (temporary version)
- Added support to SMT-LIBv2 language extensions for optimization
- Fixed several bugs
