Optimization #439

mikand · 2017-09-14T14:03:23Z

Added initial support for Optimization Modulo Theory.

Currently, the only "real" optimizing solver we have is Z3, but the extension is designed to be general and extensible, on the same line as the solver factory.

Moreover, this PR introduces two mixins that can use any solver with an incremental or "solving under assumption" interface to perform a simple optimization loop on the SAT side. The technique is not complete and can diverge in general, but it is simple and also effective in some cases.

marcogario · 2017-09-27T02:18:28Z

Is this ready for review?

mikand · 2017-09-27T07:19:19Z

Not really, I would like to add some more tests and features, but if you have time for an early review it is most welcome! 😄

pysmt/factory.py

pysmt/solvers/optimizer.py

pysmt/solvers/z3.py

pysmt/test/__init__.py

pysmt/test/test_optimization.py

mikand · 2019-01-22T12:47:41Z

Interestingly, the tests trigger a deterministic segmentation fault on z3 with python3.6 for windows. I will try to reproduce locally.

marcogario · 2020-03-30T10:47:11Z

👋 Thanks for pushing this through! I will re-review this in the next few days. Since the PR description is almost 2yr old 👴 , could you make sure that the PR description captures the changes that were made?

mikand · 2020-03-31T07:14:41Z

@marcogario wait before merging this. With @arrighi79 and @PatrickTrentin88 we are working on a more comprehensive and adherent refactoring of the optimization. I will use this branch as "master" for a series of PRs and then we'll merge this afterwards.

marcogario

This looks very promising! 🎉

The PR is doing quite a bunch of things and I think it would better to split it in more manageable chunks.

The optimization interface using "dumb" SMT solvers
Integration with OptiMathsat
Other changes (e.g., bug fixes in configuration, Z3 interpolants)

I am not particularly convinced that the dynamic loading of OptiMathsat is the best way to proceed. This adds a layer of indirection that needs to be resolved for basically every solver call. I wonder if this introduces a performance regression. Could you update the description of the PR explaining the rationale for this approach and alternatives that were considered?

pysmt/cmd/check_version.py

pysmt/cmd/install.py

pysmt/shortcuts.py

pysmt/solvers/dynmsat.py

marcogario · 2020-05-23T13:19:48Z

pysmt/solvers/msat.py

+        # Check if we are working on a version MathSAT supporting quantifier elimination
+        self._msat_lib = MSATLibLoader(self.__class__.__lib_name__)
+        if not hasattr(self._msat_lib, "MSAT_EXIST_ELIM_ALLSMT_FM"):
+            raise NotImplementedError


Do you think we still need this?

marcogario · 2020-05-23T13:22:12Z

pysmt/solvers/optimizer.py

+    Interface for the optimization
+    """
+
+    def optimize(self, cost_function, **kwargs):


Why isn't this called minimize? optimize does not make it clear in which direction we are working (min/max).

marcogario · 2020-05-23T13:24:09Z

pysmt/solvers/optimizer.py

+    def _setup(self):
+        raise NotImplementedError
+
+    def _cleanup(self, client_data):
+        raise NotImplementedError
+
+    def _pareto_setup(self, client_data):
+        raise NotImplementedError
+
+    def _pareto_cleanup(self, client_data):
+        raise NotImplementedError
+
+    def _pareto_check_progress(self, client_data, cost_functions,
+                               costs_so_far, lts, les):
+        raise NotImplementedError
+
+    def _pareto_block_model(self, client_data, cost_functions, last_model, lts, les):
+        raise NotImplementedError
+
+    def _optimization_check_progress(self, client_data, cost_function,
+                                     cost_so_far, lt, le, strategy):
+        raise NotImplementedError


Don't we need to document what an implementation of these methods would do?

marcogario · 2020-05-23T13:24:35Z

pysmt/solvers/optimizer.py

+                 feasible_solution_callback=None,
+                 step_size=1, **kwargs):
+        """This function performs the optimization as described in
+        `Optimizer.optimize()`. However. two additional parameters are


Suggested change

`Optimizer.optimize()`. However. two additional parameters are

`Optimizer.optimize()`. However. three additional parameters are

marcogario · 2020-05-23T13:25:13Z

pysmt/solvers/optimizer.py

+        the satisfiable models.
+
+        `feasible_solution_callback` is a function with a single
+        argument or None. If specified, the function will be called


The argument can be None? If so

Suggested change

argument or None. If specified, the function will be called

argument (possibly None). If specified, the function will be called

For now, we support only Z3 native minimization and a very naive optimization loop using solving under assumptions

…imization

For now, we support only Z3 native minimization and a very naive optimization loop using solving under assumptions

… factorization of out-of-solver optimizers

… optizimers, add test for MaxSMT, add warning for real optimization objectives in the algorithms

Add optimization tests

mikand · 2025-05-12T11:56:07Z

Ciao @marcogario,

while @Framba-Luca fixes the tests and re-aligns the code with master, can you have a quick look and tell us if something is missing? I would like to merge this soon!

marcogario

I've taken a very superficial look as I do not have much context on the change and this is quite a large PR.

It seems the test coverage is quite good, so I don't see a reason to delay merging these changes.

Maybe 2 things that we might add (as a follow-up is fine) are some words about this feature in the README and a dedicated example in the examples/ folder.

You have tests and you have quite a fair amount of explanation in optimizer.py about the various types of optimization problems. The goal of examples/ is to have that information in a format that is more "didactic", so people can quickly grasp the capabilities of pysmt and understand how to do something.

marcogario · 2025-05-13T11:47:19Z

pysmt/optimization/goal.py

+# check if gmpy2 is installed or not and decide which numeric classes are supported
+accepted_integer_numbers_class = (int, )
+accepted_real_numbers_class = (float, Fraction)
+try:
+    import gmpy2
+    accepted_integer_numbers_class += (gmpy2.mpz, )
+    accepted_real_numbers_class += (gmpy2.mpq, gmpy2.mpfr)
+except ImportError:
+    pass
+accepted_numbers_class = accepted_integer_numbers_class + accepted_real_numbers_class


It is a bit odd that you are running this half-way through the file. Pushing this to the top or having dedicated files per goal type would make this more obvious.

marcogario · 2025-05-13T11:47:57Z

pysmt/cmd/shell.py

 from warnings import warn

-from pysmt import git_version
+from pysmt import __version__


Nit. This change could probably be its own PR.

marcogario · 2025-05-13T11:48:36Z

pysmt/fnode.py

-                             STR_LENGTH, STR_CONCAT, STR_CONTAINS,
-                             STR_INDEXOF, STR_REPLACE, STR_SUBSTR,
-                             STR_PREFIXOF, STR_SUFFIXOF,
-                             STR_TO_INT, INT_TO_STR,
-                             STR_CHARAT,


I assume these were unused, otherwise CI would go 💥 , right?

We checked, this is just a cleanup of the imports, the FNodel class only uses the STR_OPERATORS set

marcogario · 2025-05-13T11:51:35Z

pysmt/optimization/goal.py

+        self.id = MaxSMTGoal._instance_id
+        MaxSMTGoal._instance_id = MaxSMTGoal._instance_id + 1


👀 Why do you need this?

marcogario · 2025-05-13T11:52:28Z

pysmt/optimization/optimizer.py

+        """Returns a pair `(model, cost)` where `model` is an object
+        that obtained according to `goal` while satisfying all
+        the formulae asserted in the optimizer, while `cost` is the
+        objective function value for the model.


Suggested change

"""Returns a pair `(model, cost)` where `model` is an object

that obtained according to `goal` while satisfying all

the formulae asserted in the optimizer, while `cost` is the

objective function value for the model.

"""Returns a pair `(model, cost)` where `model` is an object

obtained according to `goal` while satisfying all

the formulae asserted in the optimizer, while `cost` is the

objective function value for the model.

marcogario · 2025-05-13T11:57:06Z

pysmt/optimization/optimizer.py

+        self.client_data = client_data
+
+    def linear_search_cut(self):
+        """must be called always"""


This comment is not really clear. Maybe the assumptions on how to use this object should be part of the class doctstring.

marcogario · 2025-05-13T11:57:38Z

pysmt/optimization/optimsat.py

+# TODO:
+# - check msat does not instantiate any MSAT class directly (use virtual override)
+# - is it possible to reintroduce file-level try-except for library import?
+# - the "Not in Python's Path" message is wrong for MathSAT when only OptiMAthSAT
+#   is installed.. the current implementation must be revised.


marcogario · 2025-05-13T11:57:55Z

pysmt/optimization/optimsat.py

+        # TODO: support FP
+        # TODO: support signed/unsigned BV optimization


marcogario · 2025-05-13T12:06:34Z

pysmt/test/smtlib/parser_utils.py

            warnings.warn("Test (%s, %s) skipped because Boolector can't handle QF_UF." % (logic, smtfile))
            return
        log = script.evaluate(solver)
+        print(log)


marcogario · 2025-05-13T12:07:09Z

pysmt/test/smtlib/parser_utils.py

+    (QF_LIA, "smtlib2_load_objective_model.smt2", SAT, {
+        OptimizationTypes.BOXED: [Int(3), Int(30)],
+        OptimizationTypes.PARETO: [ # TODO weird. if pareto is tested before boxed in optimsat it works, otherwise it fails
+            (Int(x), Int(2*x + 20)) for x in range(3, 6)
+        ],
+        OptimizationTypes.LEXICOGRAPHIC: [Int(3), Int(26)],


Do you need to create a follow-up issue for this?

…nges

…xes to binary search

mikand · 2025-05-16T07:16:20Z

pysmt/optimization/optimizer.py

+        if not goal.is_maxsmt_goal():
+            term_type = goal.term().get_type()
+            # For bit-vectors, start lower and upper bounds to their width limit
+            if term_type.is_bv_type():
+                # add 1 top upper bound because it is excluded
+                if goal.signed:
+                    lower = -(2**(term_type.width-1))
+                    upper = (2**(term_type.width-1))
+                else:
+                    lower = 0
+                    upper = (2**term_type.width) + 1


Why put this here and not in the constructor of OptSearchInterval?

Note after sync: being that minimization has [lower, upper) and maximization has (lower, upper], here we have to check if we are minimizing or maximizing to understand if we have to add 1 to the upper (when maximizing) or remove 1 to the lower (when minimizing)

mikand · 2025-05-16T07:18:28Z

pysmt/optimization/optimizer.py

+            if formula is not None:
+                self.add_assertion(formula)
+            rt = self.solve()
+            # TODO for example in z3 the get_model must be called before the pop.


I think this is a design bug: after the pop() we are NOT guaranteed to have access to the model, so it would be better to get it before the pop() and return it to the caller (also in the pareto case)

mikand · 2025-05-16T07:35:29Z

pysmt/optimization/optimizer.py

+        add = 1 if self._obj.is_minimization_goal() else 0
+        return (l + u + add) // 2


using a +1 is OK-ish for QF_LIA and QF_BV objectives, but not for QF_LRA (where we can simply use / 2 instead of '// 2')

I think the general rule is: if I am minimizing, then at each step an optimal solution s is s.t. lower < s <= upper. Instead, for maximization, lower <= s < upper. We have to document this. However, this means that if I have lower=-10 and upper=-9 in the case of maximization I would get a pivot=-9 which would make the algorithm loop. I think a simpler approach would be to compute the pivot as (l+u) // 2 and then adjust it with a +1 or -1 if it is outside of the ranges above.

…ome edge cases. maxsmt on real with binary strategy could diverge

…on diverging for unbounded cases and use that method in tests that use the Real logic, avoiding non-endin tests in CI

mikand · 2025-05-19T12:21:13Z

pysmt/optimization/goal.py

+# check if gmpy2 is installed or not and decide which numeric classes are supported
+accepted_integer_numbers_class = (int, )
+accepted_real_numbers_class = (float, Fraction)
+try:
+    import gmpy2
+    accepted_integer_numbers_class += (gmpy2.mpz, )
+    accepted_real_numbers_class += (gmpy2.mpq, gmpy2.mpfr)
+except ImportError:
+    pass
+accepted_numbers_class = accepted_integer_numbers_class + accepted_real_numbers_class


This code could be removed, as we now ude the Real or Int constructors

mikand · 2025-05-19T12:26:19Z

pysmt/fnode.py

-                             STR_LENGTH, STR_CONCAT, STR_CONTAINS,
-                             STR_INDEXOF, STR_REPLACE, STR_SUBSTR,
-                             STR_PREFIXOF, STR_SUFFIXOF,
-                             STR_TO_INT, INT_TO_STR,
-                             STR_CHARAT,


We checked, this is just a cleanup of the imports, the FNodel class only uses the STR_OPERATORS set

mikand · 2025-05-19T12:36:07Z

pysmt/optimization/optimsat.py

+
+    @clear_pending_pop
+    def optimize(self, goal, **kwargs):
+        msat_obj = self._assert_msat_goal(goal, 0)


Check that this works if called multiple times. (Add tests)

…s and add a way to destroy already asserted objectives, but it does not work

… Int and Real that already do the check in a unified way

…the incapability of removing an asserted goal. Also add some tests to check subsequent optimizations

marcogario added this to the 0.7.5 milestone Sep 16, 2017

marcogario requested changes Nov 19, 2017

View reviewed changes

marcogario modified the milestones: 0.7.5, 0.8.0 May 20, 2018

mikand requested a review from marcogario January 21, 2019 16:02

mikand assigned marcogario Jan 21, 2019

marcogario modified the milestones: 0.9.0, Backlog Apr 18, 2020

mikand force-pushed the optimization branch from 3826daa to 4885edd Compare May 5, 2020 07:47

marcogario previously requested changes May 23, 2020

View reviewed changes

marcogario modified the milestones: Backlog, 1.0.0 May 23, 2020

yxliang01 mentioned this pull request Oct 26, 2020

Soft Constraints #664

Closed

mikand assigned mikand and unassigned marcogario Dec 22, 2020

mikand added 10 commits December 22, 2020 14:06

Added initial implementation of optimization support in pysmt.

56ea649

For now, we support only Z3 native minimization and a very naive optimization loop using solving under assumptions

Added initial support for infintes and infinitesimals in z3-based opt…

a96927e

…imization

Added initial implementation of optimization support in pysmt.

a6a3b52

For now, we support only Z3 native minimization and a very naive optimization loop using solving under assumptions

Added support for pareto computation in SUA optimizer

53d4125

Added incremental implementation of a basic optimizer

db3a983

Added installer for OptiMsat

409f06a

Initial implementation of OptiMathSAT support

276605f

Addressed most of PR comments

19a07a6

Added OptiMathSAT to CI tests, fixed problem in installer and started…

79c7486

… factorization of out-of-solver optimizers

Finished factorization of out-of-solver optimizers

80c097b

Framba-Luca and others added 6 commits April 18, 2025 18:20

minor fix

9dcce18

minor fix

99dd0f5

chore: removed some commented code

2b13c03

feat(Internal Optimizers): add support to real logics in SUA and INCR…

c02ef08

… optizimers, add test for MaxSMT, add warning for real optimization objectives in the algorithms

fix: implemented requested changes

f028cc4

Merge pull request #793 from pysmt/optimization-add-tests

a7d7377

Add optimization tests

mikand requested a review from marcogario May 12, 2025 11:56

Framba-Luca added 3 commits May 12, 2025 15:10

Minor improvement

e093b57

Merge branch 'master' into optimization

09b1ec2

Merge branch 'master' into optimization

a9a90a1

marcogario approved these changes May 13, 2025

View reviewed changes

Framba-Luca added 2 commits May 13, 2025 18:01

chore(optimization): cleanup PR code; implementing some requested cha…

7a081d9

…nges

Fix: Implemented requested changes; add test on binary search; add fi…

e03edd7

…xes to binary search

mikand commented May 16, 2025

View reviewed changes

Framba-Luca added 2 commits May 16, 2025 18:19

fix(binary optimization strategy): moved some code around and fixed s…

ebc15cf

…ome edge cases. maxsmt on real with binary strategy could diverge

fix(omt-test): add a method that returns only solver names that are n…

0306e0c

…on diverging for unbounded cases and use that method in tests that use the Real logic, avoiding non-endin tests in CI

mikand commented May 19, 2025

View reviewed changes

Framba-Luca force-pushed the optimization branch from 7924464 to 0306e0c Compare May 19, 2025 16:11

Framba-Luca added 9 commits May 20, 2025 16:48

Backup commit: add some optimization tests on subsequent optimization…

91214ac

…s and add a way to destroy already asserted objectives, but it does not work

backup commit

7bc414a

fix(goal): removed gpmpy2 check in max_smt goal since now it is using…

1dd1138

… Int and Real that already do the check in a unified way

fix(optimsat): optimsat raises an exception when it is reused due to …

965bde6

…the incapability of removing an asserted goal. Also add some tests to check subsequent optimizations

Merge branch 'master' into optimization

8b3ea2f

fix(test): skip optimsat in cnf test (and not only msat)

29e8353

fix(optimsat): fixed optimsat on subsequent optimizations

93f3302

Add last tests and cleanup

d190366

minor fix

1c56620

mikand merged commit d1a1a25 into master May 27, 2025
42 of 49 checks passed

mikand deleted the optimization branch May 27, 2025 12:05

	`Optimizer.optimize()`. However. two additional parameters are
	`Optimizer.optimize()`. However. three additional parameters are

	argument or None. If specified, the function will be called
	argument (possibly None). If specified, the function will be called

		self.id = MaxSMTGoal._instance_id
		MaxSMTGoal._instance_id = MaxSMTGoal._instance_id + 1

		# TODO: support FP
		# TODO: support signed/unsigned BV optimization

		add = 1 if self._obj.is_minimization_goal() else 0
		return (l + u + add) // 2

Optimization #439

Optimization #439

Uh oh!

Conversation

mikand commented Sep 14, 2017

Uh oh!

marcogario commented Sep 27, 2017

Uh oh!

mikand commented Sep 27, 2017

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mikand commented Jan 22, 2019

Uh oh!

marcogario commented Mar 30, 2020

Uh oh!

mikand commented Mar 31, 2020

Uh oh!

marcogario left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mikand commented May 12, 2025

Uh oh!

marcogario left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment