mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 22:33:40 +00:00
Code Activity

add MUS/MCS plan

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-28 21:18:17 -07:00
parent 16e0ad14aa
commit bd8875bf5f
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/opt/maxres.cpp
View file

@ -272,18 +272,23 @@ public:
Plan: Plan:
- Get maximal set of disjoint cores. - Get maximal set of disjoint cores.
- Update the lower bound using the cores. - Update the lower bound using the cores.
- As a side-effect find a satisfying assignment that - As a side-effect find a satisfying assignment that has maximal weight.
has maximal weight.
(during core minimization several queries are bound to be SAT, (during core minimization several queries are bound to be SAT,
those can be used to boot-strap the MCS search). those can be used to boot-strap the MCS search).
- Use the best satisfying assignment to find an MCS of least weight. - Use the best satisfying assignment from the MUS search to find an MCS of least weight.
- Update the upper bound using the MCS. - Update the upper bound using the MCS.
- Update the soft constraints using first the cores. - Update the soft constraints using first the cores.
- Then update the resulting soft constraints using the evaluation of the MCS/MSS - Then update the resulting soft constraints using the evaluation of the MCS/MSS
- Add a cardinality constraint to force new satisfying assignments to improve - Add a cardinality constraint to force new satisfying assignments to improve
the new upper bound. the new upper bound.
- In every iteration, the lower bound is improved using the cores. - In every iteration, the lower bound is improved using the cores.
- In every iteration, the upper bound is improved using the MCS - In every iteration, the upper bound is improved using the MCS.
- Optionally: add a cardinality constraint to prune the upper bound.
What are the corner cases:
- suppose that cost of cores adds up to current upper bound.
-> it means that each core is a unit (?)
*/ */
lbool mus_mss2_solver() { lbool mus_mss2_solver() {
init(); init();