Question: abc's solver configuration for HWMCC'20?

[wu-haoze]

Hi there,

I'm writing to ask whether it is possible to share the commands of abc used in HWMCC'20?

Thanks in advance!

[sirandreww]

Did you get an answer to this?

[wu-haoze]

No :(

…

________________________________ From: Andrew Luka ***@***.***> Sent: Wednesday, February 7, 2024 3:49 AM To: berkeley-abc/abc ***@***.***> Cc: Andrew (Haoze) Wu ***@***.***>; Author ***@***.***> Subject: Re: [berkeley-abc/abc] Question: abc's solver configuration for HWMCC'20? (Issue #216) Did you get an answer to this? — Reply to this email directly, view it on GitHub<#216 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/ACRZF2Y6KJTKQBO4C4EGBV3YSNS4PAVCNFSM6AAAAAAXOHAGUGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMZRHA3TONZUGY>. You are receiving this because you authored the thread.Message ID: ***@***.***>

[sirandreww]

Do you have a guess as to how it was run?

[sterin]

The complete configuration for HWMCC 2020 can be found at

https://github.com/sterin/super-prove-build

It's a wrapper project that collects all the relevant tools and build scripts. Checkout tag hwmcc20-2 for the exact version used in the competition. There's a README.md file that describes how to build and run. It builds and runs on Ubuntu 18.04, later version might need some work, mainly because of the Python 2 to 3 transition.

[sirandreww]

Thank you for the reference! From my understanding multiple engines were run at once for ABC results, as indicated by this:

engines = [
        ( 'pdr', ['abc', '-b', '-c', '&st; &put; pdr ; send_status'] ),
        ( 'bmc3', ['abc', '-b', '-c', '&st; &put; bmc3 -a'] ),
        ( ',bmc', ['bip', ',bmc', '-no-logo', '@@'] ),
        ( ',treb', ['bip', '-no-logo', ',treb', '@@'] ),
        ( ',treb -abs', ['bip', '-no-logo', ',treb', '-abs', '@@'] ),
    ]

[GPJ-ZFF]

how to use bmc2 for an aig